Back to Search
Start Over
Abstraction and resolution modulo AC: How to verify Diffie–Hellman-like protocols automatically
- Source :
-
Journal of Logic & Algebraic Programming . Aug2005, Vol. 64 Issue 2, p219-251. 33p. - Publication Year :
- 2005
-
Abstract
- 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. [Copyright &y& Elsevier]
Details
- Language :
- English
- ISSN :
- 15678326
- Volume :
- 64
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- Journal of Logic & Algebraic Programming
- Publication Type :
- Academic Journal
- Accession number :
- 17915748
- Full Text :
- https://doi.org/10.1016/j.jlap.2004.09.004