Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

• URL: http://arxiv.org/abs/2601.21910v1
• Date: Thu, 29 Jan 2026 16:00:56 GMT
• Title: Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)
• Authors: Sofia Giampietro, Ralf Sasse, David Basin,
• Abstract summary: 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.
• Score: 2.264276964593832
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Diffie-Hellman groups are commonly used in cryptographic protocols. While most state-of-the-art, symbolic protocol verifiers support them to some degree, they do not support all mathematical operations possible in these groups. In particular, they lack support for exponent addition, as these tools reason about terms using unification, which is undecidable in the theory describing all Diffie-Hellman operators. In this paper we approximate such a theory and propose a semi-decision procedure to determine whether a protocol, which may use all operations in such groups, satisfies user-defined properties. We implement this approach by extending the Tamarin prover to support the full Diffie-Hellman theory, including group element multiplication and hence addition of exponents. This is the first time a state-of-the-art tool can model and reason about such protocols. We illustrate our approach's effectiveness with different case studies: ElGamal encryption and MQV. Using Tamarin, we prove security properties of ElGamal, and we rediscover known attacks on MQV.

Related papers

• Cryptographic Choreographies [37.66265825228905]
  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.
  arXiv  Detail & Related papers  (2026-02-13T14:35:19Z)
• Side Channel Analysis in Homomorphic Encryption [0.46040036610482665]
  Homomorphic encryption provides many opportunities for privacy-aware processing.<n>Existing cryptographic methods have been shown in the past to be susceptible to side channel attacks.<n>This paper aims to outline a range of weaknesses within FHE implementations as related to side channel analysis.
  arXiv  Detail & Related papers  (2025-05-16T09:56:03Z)
• Constructing a fully homomorphic encryption scheme with the Yoneda Lemma [0.0]
  The paper redefines the foundations of asymmetric cryptography's homomorphic cryptosystems through the application of the Yoneda Lemma.<n>It demonstrates that widely adopted systems, including ElGamal, RSA, Benaloh, Regev's LWE, and NTRUEncrypt, are directly derived from the principles of the Yoneda Lemma.<n>This synthesis leads to the creation of a holistic homomorphic encryption framework, the Yoneda Encryption Scheme.
  arXiv  Detail & Related papers  (2024-01-24T06:46:26Z)
• Uncovering Prototypical Knowledge for Weakly Open-Vocabulary Semantic Segmentation [59.37587762543934]
  This paper studies the problem of weakly open-vocabulary semantic segmentation (WOVSS) Existing methods suffer from a granularity inconsistency regarding the usage of group tokens. We propose the prototypical guidance network (PGSeg) that incorporates multi-modal regularization.
  arXiv  Detail & Related papers  (2023-10-29T13:18:00Z)
• Tracially embeddable strategies: Lifting MIP* tricks to MIPco [0.0]
  We show that any two-party correlation in the commuting operator model can be approximated using a tracially embeddable strategy.<n>We also extend the state-dependent norm variant of the Gowers-Hatami theorem to finite von Neumann algebras.
  arXiv  Detail & Related papers  (2023-04-04T16:41:30Z)
• Publicly-Verifiable Deletion via Target-Collapsing Functions [81.13800728941818]
  We show that targetcollapsing enables publiclyverifiable deletion (PVD) We build on this framework to obtain a variety of primitives supporting publiclyverifiable deletion from weak cryptographic assumptions.
  arXiv  Detail & Related papers  (2023-03-15T15:00:20Z)
• Equivariant Transduction through Invariant Alignment [71.45263447328374]
  We introduce a novel group-equivariant architecture that incorporates a group-in hard alignment mechanism. We find that our network's structure allows it to develop stronger equivariant properties than existing group-equivariant approaches. We additionally find that it outperforms previous group-equivariant networks empirically on the SCAN task.
  arXiv  Detail & Related papers  (2022-09-22T11:19:45Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Unsupervised Disentanglement with Tensor Product Representations on the Torus [78.6315881294899]
  Current methods for learning representations with auto-encoders almost exclusively employ vectors as the latent representations. In this work, we propose to employ a tensor product structure for this purpose. In contrast to the conventional variations methods, which are targeted toward normally distributed features, the latent space in our representation is distributed uniformly over a set of unit circles.
  arXiv  Detail & Related papers  (2022-02-13T04:23:12Z)
• A Two-Stage Masked LM Method for Term Set Expansion [50.59278236410461]
  We tackle task of Term Set Expansion (TSE): given a small seed set of example terms from a semantic class, finding more members of that class. We propose a novel TSE algorithm, which combines the pattern-based and distributional approaches. Our method outperforms state-of-the-art TSE algorithms.
  arXiv  Detail & Related papers  (2020-05-03T12:06:06Z)
• Post-Quantum Cryptography(PQC): Generalized ElGamal Cipher over GL(8,F251) [0.0]
  Post-quantum cryptography (PQC) attempts to find cryptographic protocols resistant to attacks.<n>This paper focuses on an asymmetric cipher based on a generalized ElGamal non-arbitrated protocol.
  arXiv  Detail & Related papers  (2017-02-12T22:50:28Z)

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.