% NSPK modified by Lowe (NSL) with headers
% n-ary cat version, no attacks found

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

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

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

% Normal bundle

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

% Instantiated normal bundle

nsi([Sa,Sb]) :-
  strand(roleA,a,b,na,nb,Sa),
  strand(roleB,a,b,na,nb,Sb).

% Bundle with A and B (no compromise)

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

% Two B's (was type flaw compromise!)

ns02([Sb,Sb2,St]) :-
  strand(roleB,a,b,Na,nb,Sb),
  strand(roleB,B,A,Na2,nb2,Sb2),
  strand(test,nb,St).

% Two B's, one A (no)

ns12([Sa,Sb,Sb2,St]) :-
  strand(roleA,A,B,na,Nb,Sa),
  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 (no)

ns22([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).