pred begin/1 block.
pred c/1 elimVar,decompData.
nounif c:x.

fun pk/1.
fun sign/2.
fun sA/0.
fun sB/0.
fun na/1.
fun nb/4.

query end:x.

reduc
(* Initialization *)

c:pk(sA());
c:pk(sB());

(* The attacker *)

c:x -> c:pk(x);
c:x & c:y -> c:sign(x,y);
c:sign(x,y) -> c:y;
ver:(sign(x,y),pk(x));

(* The protocol *)
(* first message *)

c:na(i);

c:n & c:pk(a) & c:pk(b) ->
  c:sign(b,(n,nb(i,pk(a),pk(b),n),pk(a)));

c:na(i) & c:sign(b,(na(i),n,pk(a))) & begin:(pk(a),pk(b)) ->
  c:sign(a,(n,na(i),pk(b)));

c:n & c:sign(sA(),(nb(i,pk(sA()),pk(sB()),n),n,pk(sB()))) ->
  end:(pk(sA()),pk(sB())).