**Sound Approximations to Diffie-Hellman using Rewrite Rules**Christopher Lynch Catherine Meadows Naval Research Lab**Cryptographic Protocol Analysis**• Formal Methods Approach usually ignores properties of algorithm • But Algebraic Properties of Algorithm can be modeled as Equational Theory**Example: DH Protocol**• A ! B: gnA • B ! A: gnB • A ! B: e(h(exp(g,nB¢ nA)),m) • B ! A: e(h(exp(g,nA¢ nB)),m’)**DH uses Commutativity (C)**• exp(g,nB¢ nA) = exp(g,nA¢ nB) • This can lead to attacks • Analysis using C-unification finds these attacks**C-Unification**• exp(g,X ¢ Y) = exp(g,nA¢ nB) has two solutions • Solution 1: [X nA, Y nB] • Solution 2: [X nB, Y nA]**C-unification is Exponential**• exp(g,X1 Xn) = exp(g,c1 cn) has 2n solutions • Let d1,,dn be a permutation of c1,,cn • 2n permutations exist • Then [X1 d1,,Xn dn] is a solution**Goal of Paper**• Find an efficient theory H to approximate C soundly • i.e., an attack modulo H is an attack modulo C • But what about vice versa (that’s the hard part)**Our Results**• We found an efficient theory H which approximates C soundly • We gave simple properties for a DH protocol to satisfy • We showed that if a protocol has these properties then a C-attack can be converted to an H-attack**Basic Properties**• symmetric keys of form h(exp(g,nA¢ nB)) • An honest principal can send exp(g,n) • h-terms appear nowhere else, exponent nonces appear nowhere else, exp-terms appear nowhere else**Properties preventing Role Confusion Attacks**• Messages encrypted with DH-key from Initiator and Responder must be of different form • Messages encrypted with DH-key must contain a unique strand id**Intruder**• As usual, the intruder can see all messages, and modify, delete and create messages • Of course, the intruder does not have to obey any of these rules**About the Properties**• Most DH-protocols for two principals satisfy these properties • They are syntactic, so it is easy to check if a protocol meets them**Who Cares?**• A Protocol Developer: A protocol with these properties will have no attack based on commutativity • A Protocol Analyzer: If a protocol has these properties, analyze it using efficient H-theory. Only if it does not, then use C.**Contents of Talk**• Representation of Protocol • Derivation Rules • Properties and Proof Techniques**Example of DH Protocol**• A ! B: [exp(g,nA), nonce] • B ! A: [exp(g,nB), e(h(exp(g,nB¢ nA)),exp(g,nA))] • A ! B: e(h(exp(g,nA¢ nB)),ok)**Specification of Protocol Rules**• A: ! [exp(g,nA), nonce] • B: [Y, nonce] ! [exp(g,nB), e(h(Y,nB),Y)] • A: [Z, e(h(exp(Z,nA),exp(g,nA))] ! e(h(exp(Z,nA),ok)**Instantiation of Specification**• A: ! [exp(g,nA), nonce] • B: [exp(g,nA), nonce] ! [exp(g,nB), e(h(exp(g,nA¢ nB)),exp(g,nA))] • A:[exp(g,nB), e(h(exp(g,nB¢ nA)),exp(g,nA))] ! e(h(exp(g,nB¢ nA),ok)**Equation needed in Protocol**• Need to know that: h(exp(g,nA¢ nB)) = h(exp(g,nB¢ nA)) • That’s where C is needed, but is there a more efficient H • h(exp(X,Y ¢ Z)) = h(exp(X,Z ¢ Y)) will work, but still not good enough**Modification of DH Protocol**• Assume inititiator uses function h1 and responder uses h2 • A ! B: [exp(g,nA), nonce] • B ! A: [exp(g,nB), e(h2(exp(g,nB¢ nA)),exp(g,nA))] • A ! B: e(h1(exp(g,nA¢ nB)),ok)**New Specification**• A: ! [exp(g,nA), nonce] • B: [Y, nonce] ! • [exp(g,nB), e(h2(Y,nB),Y)] • A: [Z, e(h1(exp(Z,nA),exp(g,nA))] ! e(h1(exp(Z,nA),ok)**New Instantiation**• A: ! [exp(g,nA), nonce] • B: [exp(g,nA), nonce] ! [exp(g,nB), e(h2(exp(g,nA¢ nB)),exp(g,nA))] • A:[exp(g,nB), e(h1(exp(g,nB¢ nA)),exp(g,nA))] ! e(h1(exp(g,nB¢ nA),ok)**Equation we now need**• h2(exp(x,nA¢ nB)) = h1(exp(x,nB¢ nA)) • So theory H will be h2(exp(X,Y ¢ Z)) = h1(exp(X,Z ¢ Y))**How Efficient is H**Using results from [LM01], we see that: • In H, all unifiable terms have a most general unifier • Complexity of H-unification is quadratic (usually linear in practice)**Completeness Theorem**• C theory is now exp(X,Y ¢ Z) = exp(X, Z ¢ Y) and h1(X) = h2(X) • Show that any attack modulo C can be converted to attack modulo H**Differences between H and C**• h1(exp(g, n1¢ n2)) equals h2(exp(g,n1¢ n2)) modulo H but not modulo C • h1(exp(g, n1¢ n2)) equals h1(exp(g, n2¢ n1)) modulo H but not modulo C • h1(exp(x, n1¢ n2¢ n3)) equals h2(exp(x, n3¢ n2¢ n1)) modulo H but not modulo C**Protocol Instance**A Protocol Instance has 2 parts • Protocol Rules • Derivation Rules to represent Intruder**Derivation Rules**• [X,Y] ` X • [X,Y] ` Y • X, Y ` [X,Y] • privkey(A), enc(pubkey(A), X) ` X • pubkey(A), enc(privkey(A), X) ` X**More Derivation Rules**• X, Y ` enc(X,Y) • X, Y ` e(X,Y) • X ` hi(X) • X, e(X,Y) ` Y • X,Y ` exp(X,Y)**Derivation modulo C**• Recall rule X, e(X,Y) ` Y • Derivation modulo C: • X1 e(X2,Y) `CH Y if X1 =C X2**Example**• h1(exp(x,nB¢ nI¢ nA)), e(h2(exp(x,nA¢ nI¢ nB)),m) `C m • But not h1(exp(x,nB¢ nI¢ nA)), e(h2(exp(x,nA¢ nI¢ nB)),m) `H m**How to convert from `C to `H**• Requires Certain Properties • Use Rewrite System R so that S `C m implies S+R`H m+R • R: exp(X,Y) ! X if Y is not an honest principal nonce**Properties of Protocol**• hashed symmetric keys are of the form h(exp(X ¢ n)), where X eventually unifies with a term exp(g,n’) • h-terms appear nowhere else, exponent nonces appear nowhere else, exp-terms appear nowhere else**More Interesting Properties**• A message encrypted with h1-term on RHS of protocol cannot unify with message encrypted with h2-term on LHS • Avoids role confusion attacks • Messages encrypted with hashed term must include a strand id in message • Avoids attacks involving different instances of same protocol or different protocols**Properties of Derivable Terms**• Honest Principals follow Protocol Rules • But Intruder can use derivation rules to create terms which disobey properties • Nevertheless, we show that there are certain properties that are preserved by derivation and protocol rules**Example Properties of Derivable Terms**• There is a set N (honest principal nonces) • Elements of N only appear as exponent • If a term exp(g,t1 tn) is derivable • t1 and tn are in N or are derivable • t2,,tn-1 are derivable • if term is not a key, then tn derivable**More Properties**• There are many more properties • Some quite complicated • And many lemmas and theorems to prove them**Properties Imply**• Every term will reduce by R to a term with at most two exponents (all exponents not in N are removed by rewrite rules) • This and other properties imply that if s and t C-unify then s+R and t+R H-unify**Summary**• Suppose a DH-protocol obeys simple (easy to check) properties • Then it’s possible to discover attacks based on commutativity, using an efficient equational theory**Related Work**• Properties so that attacks modeling cancellation of encryption/decryption rules are found with free algebra • Symmetric Key [Millen 03] • Public Key [LM 04]**Future Work**• Other DH work • Don’t assume base is known • What about inverses? • Group DH-protocols • Hierarchy of Protocol Models [Meadows 03]