Security Protocols as Choreographies

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstract

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.
OriginalsprogEngelsk
TitelSecurity Protocols as Choreographies : Joshua Guttman's Festschrift
Antal sider111
ForlagSpringer
Publikationsdato2021
Sider98
DOI
StatusUdgivet - 2021

Emneord

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

Fingeraftryk

Dyk ned i forskningsemnerne om 'Security Protocols as Choreographies'. Sammen danner de et unikt fingeraftryk.

Citationsformater