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.

翻译：我们提出CryptoChoreo——一种用于规范密码学协议的编排语言。编排可视为Alice-Bob表示法的扩展，为协议整体提供直观的高层视角（而非孤立地规定每个协议角色）。我们在标准Alice-Bob表示法基础上扩展的功能包括：非确定性选择、条件分支和可变长期记忆。我们通过将CryptoChoreo翻译为进程演算来定义其语义。该语义蕴含对协议的理解：在任意代数理论存在且其他参与者作出非确定性选择的情况下，它决定了智能体如何解析验证传入消息及构造传出消息。虽然该语义会引致通常不可判定的代数问题，但我们针对典型理论给出了具体实现方案。我们将此翻译方法与ProVerif工具进行关联，并通过系列案例研究表明该方案具有实际可行性。