Computer Science – Cryptography and Security
Scientific paper
2012-02-10
Computer Science
Cryptography and Security
Scientific paper
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.
Dougherty Daniel J.
Guttman Joshua D.
No associations
LandOfFree
Symbolic Protocol Analysis for Diffie-Hellman does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Symbolic Protocol Analysis for Diffie-Hellman, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Symbolic Protocol Analysis for Diffie-Hellman will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-274400