% NSPK modified by Lowe (NSL)

strand(roleA,A,B,Na,Nb,[ 
  recv([A,B]),
  send([A,Na]*pk(B)),  % Lowe's version has [Na,A]*pk(B)
  recv([Na,[Nb,B]]*pk(A)),
  send(Nb*pk(B))
]).

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

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

% Normal bundle

nsl0([Sa,Sb]) :-
  strand(roleA,A,B,na,Nb,Sa),
  strand(roleB,a,b,Na,nb,Sb).

% Bundle with A and B (no compromise)

nsl11([Sa,Sb,St]) :- 
  strand(roleA,A,B,na,Nb,Sa),
  strand(roleB,a,b,Na,nb,Sb),
  strand(test,nb,St).

% Two B's (compromise)

nsl02([Sb,Sb2,St]) :-
  strand(roleB,a,b,Na,nb,Sb),
  strand(roleB,Ab2,Bb2,Na2,nb2,Sb2),
  strand(test,nb,St).

% Two A's and two B's (compromise)

nsl22([Sa,Sb,Sa2,Sb2,St]) :-
  strand(roleA,A,B,na,Nb,Sa),
  strand(roleB,a,b,Na,nb,Sb),
  strand(roleA,A2,B2,na2,Nb2,Sa2),
  strand(roleB,Ab2,Bb2,Na2,nb2,Sb2),
  strand(test,nb,St).