Symbolic protocol analysis with an Abelian group operator or Diffie–Hellman exponentiation

Issue title: CSFW16

Article type: Research Article

Authors: Millen, Jonathan | Shmatikov, Vitaly^{; *}

Affiliations: Computer Science Laboratory, SRI International, USA. E-mail: millen@csl.sri.com, shmat@csl.sri.com

Note: [*] Partially supported by ONR Grants N00014-01-1-0837 and N00014-03-1-0961, and by DARPA contract N66001-00-C-8014.

Abstract: We demonstrate that for any well-defined cryptographic protocol, the symbolic trace reachability problem in the presence of an Abelian group operator (e.g., multiplication) can be reduced to solvability of a decidable system of quadratic Diophantine equations. This result enables complete, fully automated formal analysis of protocols that employ primitives such as Diffie–Hellman exponentiation, multiplication, and xor, with a bounded number of role instances, but without imposing any bounds on the size of terms created by the attacker.

DOI: 10.3233/JCS-2005-13306

Journal: Journal of Computer Security, vol. 13, no. 3, pp. 515-564, 2005