Security Protocols as Choreographies

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


A choreography gives a description of how endpoints in a concurrent systems should exchange messages during its execution. In this paper, we informally introduce a choreographic language for describing security protocols and a property language for expressing non-trivial security properties of such protocols. We motivate this work using the envelope protocol [2] as an example, which ensures auditable transfers by means of a TPM, that guarantees that the issuer of a message always learns whether such message has been opened or not. We then take an implementation of the TPM formulated as an API and discuss how such implementation and the usage of the TPM in the protocol can be related. Finally, we illustrate how the protocol and property descriptions can be translated into multiset rewrite rules and metric first order logic respectively, in order to check if auditable transfer holds.
Original languageEnglish
Title of host publicationSecurity Protocols as Choreographies : Joshua Guttman's Festschrift
Number of pages111
Publication date2021
Publication statusPublished - 2021


  • Choreographic Language
  • Security Protocols
  • Auditable Transfers
  • Trusted Platform Module (TPM)
  • Multiset Rewrite Rules


Dive into the research topics of 'Security Protocols as Choreographies'. Together they form a unique fingerprint.

Cite this