Cryptographic Choreographies

TL;DR

CryptoChoreo introduces a high-level choreography language for cryptographic protocols, enabling intuitive specification and analysis of complex behaviors with non-determinism and memory, supported by a practical implementation.

Contribution

It extends Alice-and-Bob notation with non-deterministic choice, branching, and memory, providing a formal semantics and a practical tool connected to ProVerif for protocol analysis.

Findings

Semantic translation to process calculus enables protocol understanding.

Implementation demonstrates practical feasibility on case studies.

Supports algebraic theories and non-deterministic choices in protocol analysis.

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.