2012/02/10 by Daniel J. Dougherty, Dougherty, Daniel J., Joshua D. Guttman +1
Computer Science · #Advanced Authentication Protocols Security #Cryptographic Implementations and Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #User Authentication and Security Systems #cs.CR
paper · pdf · doi:10.48550/arxiv.1202.2168
arxiv created 2012/02/10 · openalex publication_date 2012/02/10 · arxiv updated 2012/02/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.