TY - GEN
T1 - Security Protocols as Choreographies
AU - Bruni, Alessandro
AU - Carbone, Marco
AU - Giustolisi, Rosario
AU - Mödersheim, Sebastian Alexander
AU - Schürmann, Carsten
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
KW - Choreographic Language
KW - Security Protocols
KW - Auditable Transfers
KW - Trusted Platform Module (TPM)
KW - Multiset Rewrite Rules
KW - Choreographic Language
KW - Security Protocols
KW - Auditable Transfers
KW - Trusted Platform Module (TPM)
KW - Multiset Rewrite Rules
U2 - https://backend.orbit.dtu.dk/ws/portalfiles/portal/265046987/Bruni2021_Chapter_SecurityProtocolsAsChoreograph.pdf
DO - https://backend.orbit.dtu.dk/ws/portalfiles/portal/265046987/Bruni2021_Chapter_SecurityProtocolsAsChoreograph.pdf
M3 - Article in proceedings
SP - 98
BT - Security Protocols as Choreographies
PB - Springer
ER -