**** Protocol: Needham-Schroeder ****

**** Unsafe States ****
unsafe([step3(pk(A),tuple(nonce(B),nonce(_),pk(C))),mem(nonce(B))],{A>0,C>0})
unsafe([step3(pk(A),tuple(nonce(_),nonce(D),pk(C))),mem(nonce(D))],{A>0,C>0})
unsafe([step4(pk(C),tuple(nonce(B),nonce(_),pk(A))),mem(nonce(B))],{A>0,C>0})
unsafe([step4(pk(C),tuple(nonce(_),nonce(D),pk(A))),mem(nonce(D))],{A>0,C>0})

**** Potential Attacks ****

Constrained configuration: 
[fresh(_)]:{}.

Rule: intercept_first
rule([fresh(A)], [fresh(B),step1(pk(C),tuple(nonce(D),pk(0))),mem(nonce(D))], {C>0,B>D,D>A}).

Constrained configuration: 
[fresh(_),mem(nonce(A)),step1(pk(B),tuple(nonce(A),pk(0)))]:{B>0.0}.

Rule: trudy_cheats_and_impersonate
rule([fresh(A),mem(nonce(B))], [fresh(C),step2(pk(D),tuple(nonce(B),nonce(E),pk(F))),enc(pk(F),tuple(nonce(B),nonce(E)))], {F>0,D>0,C>E,E>A}).

Constrained configuration: 
[step1(pk(A),tuple(nonce(B),pk(0))),enc(pk(A),tuple(nonce(B),nonce(C))),step2(pk(D),tuple(nonce(_),nonce(C),pk(E)))]:{E>0.0,D>0.0,A>0.0}.

Rule: alice_is_cheated
rule([step1(pk(A),tuple(nonce(B),pk(0))),enc(pk(A),tuple(nonce(B),nonce(C)))], [step3(pk(A),tuple(nonce(B),nonce(C),pk(0))),mem(nonce(B)),mem(nonce(C))], {A>0}).

Constrained configuration: 
[step2(pk(A),tuple(nonce(_),nonce(B),pk(C))),mem(nonce(B))]:{C>0.0,A>0.0}.


Rule: fourth_rule_with_trudy
rule([step2(pk(A),tuple(nonce(B),nonce(C),pk(D))),mem(nonce(C))], [step4(pk(A),tuple(nonce(B),nonce(C),pk(D))),mem(nonce(C))], {A>0}).


Unsafe state: 
[step4(pk(A),tuple(nonce(_),nonce(B),pk(C))),mem(nonce(B))]:{C>0,A>0}.