% NSPK

strand(roleA,A,B,Na,Nb,[ 
  recv([A,B]),
  send([A,Na]*pk(B)),
  recv([Na,Nb]*pk(A)),
  send(Nb*pk(B)),
  send(roleA(A,B,Na,Nb)) % for Auth
]).

strand(roleB,A,B,Na,Nb,[
  recv([A,Na]*pk(B)),
  send([Na,Nb]*pk(A)),
  recv(Nb*pk(B)),
  send(doneB)
]).

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


nspk0([Sa,Sb,St]) :- 
  strand(roleA,_A,_B,na,_Nb,Sa),
  strand(roleB,a,b,_Na,nb,Sb),
  strand(test,nb,St).  % compromise nb

% Auth test: nspk1(Bundle, Auth)

nspk1([Sa,Sb,St],roleA(a,b,_,nb)) :-
  strand(roleA,_A,_B,na,_Nb,Sa),
  strand(roleB,a,b,_Na,nb,Sb),
  strand(test,doneB,St). % B is done