Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically

DOI10.1016/j.jlap.2004.09.004zbMath1078.68032OpenAlexW2034753880MaRDI QIDQ2484410

Kumar Neeraj Verma, Jean Goubault-Larrecq, Muriel Roger

Publication date: 1 August 2005

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2004.09.004

zbMATH Keywords

AssociativityDiffie-HellmanCompletenessVerificationAbstractionKey exchangeResolutionAbstract interpretationCryptographic protocolsCommutativityClause

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Authentication, digital signatures and secret sharing (94A62)

Related Items (4)

Alternating two-way AC-tree automata ⋮ The Blossom of Finite Semantic Trees ⋮ Analysis of the Collision Resistance of RadioGatúnUsing Algebraic Techniques ⋮ Deciding \(\mathcal H_1\) by resolution

Uses Software

• VAMPIRE
• NRL

Cites Work

• An NP decision procedure for protocol insecurity with XOR
• An attack on the Needham-Schroeder public-key authentication protocol
• Haskell overloading is DEXPTIME-complete
• Alternating two-way AC-tree automata
• The NRL Protocol Analyzer: An Overview
• New directions in cryptography
• A Unification Algorithm for Associative-Commutative Functions
• On the security of public key protocols
• Abstract interpretation and application to logic programs
• Resolution Strategies as Decision Procedures
• Using encryption for authentication in large networks of computers
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically