📎

ProVerif Examples

Example 1

The idea:

begin(A,B,m)begin(A,B,m)

A−{m}k→BA - \{m\}_k \rarr B(Symmetric keykk)

end(A,B,m)end(A,B,m)

Our Source-code in VerifPro:

Note:

idi - identity of initiator

idr - identity of receiver 

free c. (* channel *)
free A,B. (* identifiers *)
private free m.fun enc/2.
reduc dec(enc(x,y),y)=x.let responder =
in(d,(idi,idr)); (* start of process: idi, idr are A, B *)
event begin(idi,idr,m);
out(c,enc(m,k)). (* sending cipher *)let initiator =
in(d,(idi,idr)); (* start of process: idi, idr are A, B *)
in(c,y); (* receiving cipher *)
let x=dec(y,k) in	event end(idi,idr,x).
process
new k; (* symmetric key*)
new d; (* channel - used to start the process by setting initiator / responder to A / B*)
!out(d,(A,B)) | !out(d,(B,A)) | !responder | !initiator

Now we want to know:

  1. does the attacker have access to the message mm
  1. is a non-injective agreement guaranteed?

query attacker m.
query ev:end(x,y,z) ==> ev:begin(x,y,z)

The results:

  1. The message mm is kept a secret
  1. We habe a non-injective agreement
  1. A reflection attack is possible

Starting	query	not	attacker:m[]
RESULT	not	attacker:m[]	is	true.
Starting	query	ev:end(x_19,y_20,z_21)	==>	ev:begin(x_19,y_20,z_21)
goal reachable:	begin:begin(A[],B[],m[])	->	end:end(B[],A[],m[])
Goal of the attack : end:end(B[],A[],m[])event(begin(A,B,m))
out(c, enc(m,k_1))
in(c, enc(m,k_1))
event(end(B,A,m))An attack has been found.
RESULT	ev:end(x_19,y_20,z_21)	==>	ev:begin(x_19,y_20,z_21)	is	false.

Example 2

Now we try to fix this issue by adding an identifier to the sent message.

The idea:

begin(A,B,m)begin(A,B,m)

A−{B,m}k→BA - \{\textcolor{pink}B,m\}_k \rarr B(Symmetric keykk)

end(A,B,m)end(A,B,m)

Our Source-code in VerifPro:

Now the previous message m consists of (idi, m) . 

free c.
free A,B.
private free m.fun enc/2.
reduc dec(enc(x,y),y)=x.let responder =
in(d,(idi,idr));
event begin(idi,idr,m);
out(c,enc((idi,m),k)).let initiator =
in(d,(idi,idr));
in(c,y);
let (=idi,x) = dec(y,k) in	event end(idi,idr,x).
process
new k;
new d;
!out(d,(A,B)) | !out(d,(B,A)) | !responder | !initiator

Now we want to know:

  1. does the attacker have access to the message mm
  1. is a non-injective agreement guaranteed?
  1. is an injective agreement guaranteed?

query attacker:m.
query ev:end(x,y,z) ==> ev:begin(x,y,z).
query evinj:end(x,y,z) ==> evinj:begin(x,y,z).

The results:

  1. The message mm is kept a secret
  1. We habe a non-injective agreement
  1. A replay attack is possible

Starting	query	not	attacker:m[]
RESULT	not	attacker:m[]	is	true.
RESULT ev:end(x_13,y_14,z_15) ==> ev:begin(x_13,y_14,z_15) is true.
Starting query evinj:end(x_15,y_16,z_17) ==> evinj:begin(x_15,y_16,z_17)
....
event(begin(A,B,m_14_10)) at {10} in copy a_4, a_3, a_2
out(c, enc((A,m_14_10),k_6_12)) at {11} in copy a_4, a_3, a_2
in(c, enc((A,m_14_10),k_6_12)) at {6} in copy a_9, a_8, a_7, a_1
event(end(A,B,m_14_10)) at {8} in copy a_9, a_8, a_7, a_1
in(c, enc((A,m_14_10),k_6_12)) at {6} in copy sid_293_18, sid_294_17, sid_295_16,
sid_298_15
event(end(A,B,m_14_10)) at {8} in copy sid_293_18, sid_294_17, sid_295_16, sid_298_15
The event end(A,B,m_14_10) is executed in session sid_298_15 and in session a_1.

Example 3

Now we try to fix this issue by adding a nonce handshake to the sent message.

The idea:

begin(A,B,m)begin(A,B,m)

A←n−BA\larr \textcolor{pink}n - B

A−{B,m,n}k→BA - \{B,m,\textcolor{pink}n\}_k \rarr B

end(A,B,m)end(A,B,m)

free c.
free A,B.
private free m.fun enc/2.
reduc dec(enc(x,y),y)=x.let responder =
in(d,(idi,idr));
in(c,xn);
new m;
event begin(idi,idr,m);
out(c,enc((idi,m,xn),k)).let initiator =
in(d,(idi,idr));
new n; (* create new nonce *)
out(c,n);
in(c,y);
let (=idi,x,=n) = dec(y,k) in event end(idi,idr,x).
process
new k;
new d;
!out(d,(A,B)) | !out(d,(B,A)) | !responder | !initiator

Now we want to know:

  1. does the attacker have access to the message mm
  1. is an injective agreement guaranteed?

query attacker:m.
query evinj:end(x,y,z) ==> evinj:begin(x,y,z).

The results:

  1. The message mm is kept a secret
  1. We have a non-injective agreement

Starting query evinj:end(x_14,y_15,z_16) ==> evinj:begin(x_14,y_15,z_16)
...
RESULT evinj:end(x_14,y_15,z_16) ==> evinj:begin(x_14,y_15,z_16) is true.