The Private Authentication Protocol

The Private Authentication Protocol was introduced by Martin Abadi and Cédric Fournet in Private authentication. Theoretical Computer Science (2004). We want to ensure the anonymity of the participant “Alice” for one session of the protocol.

free c.

### Description of the role of Alice

let process_Alice k_a k_b =
  new N_a;
  out(c,aenc((N_a,pk(k_a)),pk(k_b))); 
  in(c,x).

### Description of the role of Bob

let process_Bob k_a k_b =
  in(c,x); 
  let (na,pka) = adec(x,k_b) in	
  if pka = pk(k_a)
  then new N_b; out(c,aenc((na,N_b,pk(k_b)),pk(k_a)))
  else new N; out(c,aenc(N,pk(k_a))).

This input describes the two roles Alice and Bob. Note that the functions pk, aenc, adec are declared by default.
In fact the following functions are already declared :

• aenc(x,y) : Asymmetric encryption of x by the public key y
• adec(x,y) : Asymmetric decryption of x by the private key y
• pk(x) : Public key of the private key x
• senc(x,y) : Symmetric encryption of x by the key y
• sdec(x,y) : Symmetric decryption of x by the key y
• sign(x,y) : Digital signature of x by the private key y
• check(x,y) : Digital check of the signature x with the public key y
• vk(x) : Verification key of the signing key x
• hash(x) : Hash of x
• (x_1,…,x_n) : Tuple

Any other one way function can be declared by the following command where n is the arity of the function myfunction.

fun myfunction/n.

Then to prove the anonymity of the role of Alice, we add to the previous input:

### Main

let instance1 =
  new k_a ; new k_b ; new k_c ; out(c,pk(k_a)) ; out(c,pk(k_b)) ; 
  out(c,pk(k_c)); 
  ( process_Alice k_a k_b | process_Bob k_a k_b ).

let instance2 =
  new k_a ; new k_b ; new k_c ; out(c,pk(k_a)) ; out(c,pk(k_b)) ;
  out(c,pk(k_c)); 
  ( process_Alice k_c k_b | process_Bob k_c k_b ).

equivalence instance1 and instance2.

Trace equivalence w.r.t. length

Since the version 0.2alpha, APTE is able to decide the trace equivalence w.r.t. length. By default, APTE assign some length coefficients to the cryptographic primitives. Hence you could check the anonymity of the Private Authentication protocol considering the length of messages by using the following command in the input file.

equivalence length instance1 and instance2.

However, if you want to specify the coefficients, you can use the following syntax.

length senc [constant=9 ; arguments = 0, 0].
length tuple(2) [ constant = 0. ; arguments = 1.1 ,1.2].

The length functions of senc and the tuple of 2 elements are now

• l_senc(x,y) = 9
• l_tuple(x,y) = 1.1 * x + 1.2 * y

Here is a full example:

free c.

length senc [constant=9 ; arguments = 0, 0].
length tuple(2) [ constant = 0. ; arguments = 1.1 ,1.2].

let P_1 = new n; new k; out(c,senc(((n,n),n),k)).

let P_2 = new n; new k; out(c,senc(n,k)).

let P_3 = new n; new k; out(c,senc((n,(n,n)),k)).

equivalence length P_1 and P_2.

equivalence P_1 and P_2.

equivalence length P_1 and P_3.

equivalence P_1 and P_3.