/*
  Protocol: ESPKE
*/
strand(roleAlice,Alice,Bob,Na,P,Nb,[
  send(Na+P),
  recv([Nb,sha([zero,[[Na,Nb],P]])]),
  send(sha([one,[[Na,Nb],P]]))
]).

strand(roleBob,Bob,Alice,Nb,P,Na,[
  recv(Na+P),
  send([Nb,sha([zero,[[Na,Nb],P]])]),
  recv(sha([one,[[Na,Nb],P]]))
]).

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

espke0([Sa,Sb,Se]) :-
  strand(roleAlice, alice, bob,   na, p, Nb, Sa),
  strand(roleBob,   bob,   alice, nb, p, Na, Sb),
  strand(test, na, Se).