Formal Verification of DHKE protocol using ProVerif 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


My questions:


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.
I think it's because par1 and par2 start "out".
As you know, a client will start to send message to the server first. And after do thart, the server will receive the message.
It seems that it's probably possible to fine if your code in one of them code is fixed like below.

let par1 = out(..); 
                  in(..);

let par2 = in(..); 
                  out(..);