Cryptographic Choreographies

• URL: http://arxiv.org/abs/2602.12967v1
• Date: Fri, 13 Feb 2026 14:35:19 GMT
• Title: Cryptographic Choreographies
• Authors: Sebastian Mödersheim, Simon Lund, Alessandro Bruni, Marco Carbone, Rosario Giustolisi,
• Abstract summary: We present CryptoChoreo, a choreography language for the specification of cryptographic protocols.<n>We define the semantics of CryptoChoreo by translation to a process calculus.
• Score: 37.66265825228905
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version) [2.264276964593832]
  Diffie-Hellman groups are commonly used in cryptographic protocols.<n> symbolic protocol verifiers do not support all mathematical operations possible in these groups.<n>We propose a semi-decision procedure to determine whether a protocol satisfies user-defined properties.<n>This is the first time a state-of-the-art tool can model and reason about such protocols.
  arXiv  Detail & Related papers  (2026-01-29T16:00:56Z)
• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Molly compiles cryptographic protocol roles into straight-line programs. We define a denotational semantics for protocol roles based on an axiomatization of the runtime.
  arXiv  Detail & Related papers  (2023-11-22T21:04:07Z)
• LpiCT: A logic security analysis framework for protocols [1.4852249222037588]
  This paper introduces logic rules and proofs, binary tree and the KMP algorithm, and proposes a new extension the pi calculus theory, a logic security analysis framework and an algorithm. Empirical results show that the new extension theory, the logic security analysis framework and the algorithm can effectively analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol.
  arXiv  Detail & Related papers  (2023-11-01T12:06:47Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  This document presents the security protocol verifier CryptoVerif. It does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can work automatically, or the user can guide it with manual proof indications.
  arXiv  Detail & Related papers  (2023-10-23T07:53:38Z)
• Lexinvariant Language Models [84.2829117441298]
  Token embeddings, a mapping from discrete lexical symbols to continuous vectors, are at the heart of any language model (LM) We study textitlexinvariantlanguage models that are invariant to lexical symbols and therefore do not need fixed token embeddings in practice. We show that a lexinvariant LM can attain perplexity comparable to that of a standard language model, given a sufficiently long context.
  arXiv  Detail & Related papers  (2023-05-24T19:10:46Z)
• Rigidity of superdense coding [3.4113536110736766]
  Superdense coding is possible to communicate two bits of classical information by sending only one qubit and using a shared EPR pair. We show that the sender and receiver only use additional entanglement as a source of classical randomness. Unlike the $d=2$ case (i.e. sending a single qubit), there can be inequivalent superdense coding protocols for higher $d$.
  arXiv  Detail & Related papers  (2020-12-03T03:04:27Z)
• Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
  We formalize human language understanding as a structured prediction task where the output is a partially ordered set (poset) Current encoder-decoder architectures do not take the poset structure of semantics into account properly. We propose a novel hierarchical poset decoding paradigm for compositional generalization in language.
  arXiv  Detail & Related papers  (2020-10-15T14:34:26Z)
• A Transformer-based Approach for Source Code Summarization [86.08359401867577]
  We learn code representation for summarization by modeling the pairwise relationship between code tokens. We show that despite the approach is simple, it outperforms the state-of-the-art techniques by a significant margin.
  arXiv  Detail & Related papers  (2020-05-01T23:29:36Z)
• Emergence of Pragmatics from Referential Game between Theory of Mind Agents [64.25696237463397]
  We propose an algorithm, using which agents can spontaneously learn the ability to "read between lines" without any explicit hand-designed rules. We integrate the theory of mind (ToM) in a cooperative multi-agent pedagogical situation and propose an adaptive reinforcement learning (RL) algorithm to develop a communication protocol.
  arXiv  Detail & Related papers  (2020-01-21T19:37:33Z)
• Lexical Sememe Prediction using Dictionary Definitions by Capturing Local Semantic Correspondence [94.79912471702782]
  Sememes, defined as the minimum semantic units of human languages, have been proven useful in many NLP tasks. We propose a Sememe Correspondence Pooling (SCorP) model, which is able to capture this kind of matching to predict sememes. We evaluate our model and baseline methods on a famous sememe KB HowNet and find that our model achieves state-of-the-art performance.
  arXiv  Detail & Related papers  (2020-01-16T17:30:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.