% NSPK modified by Lowe (NSL) with headers % Binary concatenation strand(roleA,A,B,Na,Nb,[ recv([e,A,B]), send([A,B,[A,Na]*pk(B)]), % Lowe's version has [Na,A]*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([e,e,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).