/*
  Protocol: ESPKE

  Hand-Specified. The bundle program goes into an infinite-loop when div/mul are used
  (even though they're in the CAPSL specification).
*/
strand(roleA,Passwd,Ba,Na,Mb,[
  send(div(exp(alpha,Na),exp(beta,Passwd))),
  recv([Ba,Mb]),
  send(sha([1,[exp(Ba,Na),Passwd]]))
]).

strand(roleB,Passwd,Ab,Nb,Ma,[
  recv(Ab),
  send([exp(alpha,Nb),sha([0,[exp(mul(Ab,exp(beta,Passwd)),Nb),Passwd]])]),
  recv(Ma)
]).

strand(test,X,[
  recv(X),
  send(stop)
]).

espke0([Sa,Sb,St]) :-
    strand(roleA, passwd, Ba, na, Mb, Sa),
    strand(roleB, passwd, Ab, nb, Ma, Sb),
    strand(test, na, St).