In this example, we execute a handshake between clientA and serverB.
However, the handshake has a person-in-the-middle attack, which ProVerif automatically detects.
Switch back to the simple example?
First, we define the cryptographic primitives we need to model the protocol.
Here, we define function symbols to perform symmetric and asymmetric (de)encryption,
as well as creation and validation of signatures.
We use the reduc keyword to define the equational theory between the function symbols.
We define the secret s as a private symbol (excluding it from the initial attacker knowledge),
and the attacker target to learn this secret s.
ProVerif will now try to find a way to derive this secret for the attacker,
by executing the processes we model further below,
and transforming terms it learns thereby (e.g. by applying the equational theory).
Given the primitives, we now model the handshake protocol.
We create a processus for both the client and the server using let,
and then specify what messages they receive, how these are transformed, and what is finally sent back out.
Lastly, we define the main process, which initializes the keys and boots up the client and the server processus.
ProVerif will then be able to fulfil the adversary query, i.e. find an attack.
type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.
type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.
free s:bitstring [private].
query attacker(s).
free c:channel.
let clientA(pkA:pkey,skA:skey,pkB:spkey) =
out(c,pkA);
in(c,x:bitstring);
let y = adec(x,skA) in
let (=pkB,k:key) = checksign(y,pkB) in
out(c,senc(s,k)).
let serverB(pkB:spkey,skB:sskey) =
in(c,pkX:pkey);
new k:key;
out(c,aenc(sign((pkB,k),skB),pkX));
in(c,x:bitstring);
let z = sdec(x,k) in
0.
process
new skA:skey;
new skB:sskey;
let pkA = pk(skA) in out(c,pkA);
let pkB = spk(skB) in out(c,pkB);
( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB)) )
