密码学编舞
Cryptographic Choreographies
AI总结：
CryptoChoreo是一种用于规范密码协议的编舞语言，通过扩展Alice和Bob记法，提供协议的整体高阶视图，并通过过程演算定义语义，实现协议的可验证性。
摘要：
我们提出了CryptoChoreo，一种用于规范密码协议的编舞语言。编舞可以被视为Alice和Bob记法的扩展，提供了一个整体协议的直观高级视图（而不是单独指定每个协议角色）。我们考虑的扩展包括非确定性选择、条件分支和可变的长期记忆。我们通过翻译到过程演算来定义CryptoChoreo的语义。这种语义使我们能够理解协议：它决定了在任意代数理论和其它代理的非确定性选择存在下，代理如何解析和检查传入消息以及如何构造传出消息。虽然这种语义导致了一般不可判定的代数问题，但我们为一个代表性理论提供了实现。我们将这种翻译连接到ProVerif，并在多个案例研究中展示了这种方法的实用性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
