Name
Title | ||
|---|---|---|
Abstraction and resolution modulo AC: How to verify Diffie–Hellman-like protocols automatically |
Abstract | ||
|---|---|---|
We show how cryptographic protocols using Diffie–Hellman primitives, i.e., modular exponentiation on a fixed generator, can be encoded in Horn clauses modulo associativity and commutativity. In order to obtain a sufficient criterion of security, we design a complete (but not sound in general) resolution procedure for a class of flattened clauses modulo simple equational theories, including associativity–commutativity. We report on a practical implementation of this algorithm in the MOP modular platform for automated proving; in particular, we obtain the first fully automated proof of security of the IKA.1 initial key agreement protocol in the so-called pure eavesdropper model. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.jlap.2004.09.004 | The Journal of Logic and Algebraic Programming |
Keywords | Field | DocType |
Cryptographic protocols,Diffie–Hellman,Resolution,Clause,Associativity,Commutativity,Completeness,Abstraction,Abstract interpretation,Verification,Key exchange | Discrete mathematics,Horn clause,Cryptographic protocol,Key exchange,Modulo,Theoretical computer science,Cryptographic primitive,Key-agreement protocol,Mathematics,Diffie–Hellman key exchange,Modular exponentiation | Journal |
Volume | Issue | ISSN |
64 | 2 | 1567-8326 |
Citations | PageRank | References |
28 | 1.30 | 30 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean Goubault-Larrecq | 1 | 582 | 40.90 |
| Muriel Roger | 2 | 185 | 9.35 |
| Kumar Neeraj Verma | 3 | 171 | 8.87 |