Cryptographic Choreographies

TL;DR

The semantics of CryptoChoreo are defined by translation to a process calculus, and an implementation for a representative theory is given for the specification of cryptographic protocols.

Abstract

We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole (rather than specifying each protocol role in isolation). The extensions over standard Alice-and-Bob notation that we consider are non-deterministic choice, conditional branching, and mutable long-term memory. We define the semantics of CryptoChoreo by translation to a process calculus. This semantics entails an understanding of the protocol: it determines how agents parse and check incoming messages and how they construct outgoing messages, in the presence of an arbitrary algebraic theory and non-deterministic choices made by other agents. While this semantics entails algebraic problems that are in general undecidable, we give an implementation for a representative theory. We connect this translation to ProVerif and show on a number of case studies that the approach is practically feasible.

Figures (5)

• Figure 1: Example Choreography.
• Figure 2: Syntax of CryptoChoreo.
• Figure 3: Extension of the example from Fig. \ref{['fig:ex:choreo']}.
• Figure 4: Syntax of Local Behaviors.
• Figure 5: Semantics of Local Behaviors.

Theorems & Definitions (38)

• Definition 1
• Definition 2
• Definition 3
• Lemma 1
• proof
• Lemma 2
• proof
• Lemma 3
• proof
• Theorem 1