/*
Private Authentication Protocol
 1. A -> B: {Na, pub(A)}pub(B)
 2. B -> A: {Na, Nb,pub(B)}pub(A) if B wants to communicate with A
            {Nb}pub(B) otherwise
*/

fun aenc/2.
fun pk/1.

reduc adec(aenc(x,pk(y)),y) -> x.

free c.


let processA(ska,pkb) =
  new na;
(* complete here*)
  0.


let processB(skb,pka) =
  in(c,y);
  (* complete here*)
  0.



// Main

let P =new ska ; new skb ; new skc ; out(c,pk(ska)) ; out(c,pk(skb)) ; out(c,pk(skc));
(* complete scenario here *)
0.

let Q =
 new ska ; new skb ; new skc ; out(c,pk(ska)) ; out(c,pk(skb)) ; out(c,pk(skc));
 (* complete scenario here *)
0.

query trace_equiv(P,Q).