I am new to ProVerif and trying to verify a simple DHKE protocol. The attacker is assumed as passive. The specifications are:
- The attacker cannot obtains the mutual key.
- Both participants obtain the same key.
This is what I have created.
type G. (* The generator *) type exponent. free c, sc: channel. free c02, c12: channel [private]. const g: G [data]. free msg, sameKey: bitstring [private]. fun exp(G, exponent): G. fun enc(bitstring, G): bitstring. reduc forall m: bitstring, k: G; dec(enc(m,k),k) = m. equation forall x: exponent, y: exponent; exp(exp(g,x),y) = exp(exp(g,y),x). set attacker = passive. query attacker(msg). query attacker(sameKey). let par1 = new a1: exponent; out(c, exp(g,a1)); (* g^a1 *) in(c, v2: G); let key1 = exp(v2,a1) in out(c, enc(msg,key1)); out(c02, key1). let par2 = new a2: exponent; out(c, exp(g,a2)); (* g^a2 *) in(c, v1: G); let key2 = exp(v1,a2) in out(c12, key2). let px3 = in(c02, k1: bitstring); in(c12, k2: bitstring); if k1 = k2 then 0 else out(sc, sameKey). process par1 | par2 | px3
- Is it enough to verify the first specification?
- Logically, the attacker cannot obtain the value of sameKey if the mutual key is identical. But, proverif returns the following output along with some traces. Are there any mistakes in this approach?
The proverif output:
RESULT not attacker(sameKey) cannot be proved.
[Update] I managed to solve this problem by using different channel for P1 and P2, denoted by $\verb|c01|$ and $\verb|c10|$ respectively.