**** Protocol: Needham-Schroeder ****
**** Unsafe States ****
[unsafe([step2(pk(A),tuple(pk(B),key(_),nonce(C))),mem(nonce(C))],{B>0,A>0})].

**** Potential Attacks ****

Constrained configuration: 
[mem(key(A)),fresh(_),mem(key(A))]:{}.




Rule: compromised_key
rule([mem(key(A))], [step1(pk(B),tuple(pk(C),key(A))),enc(sk(C),tuple(pk(B),key(A)))], {B>0,C>0}).


Constrained configuration: 
[fresh(_),enc(sk(A),tuple(pk(B),key(C))),mem(key(C))]:{B>0.0,A>0.0}.




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


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

****** End of trace *****
**** End Potential Attack ****
Constrained configuration: 
[fresh(A),mem(key(B))]:{B-A>0.0}.




Rule: first
rule([fresh(A)], [fresh(B),step1(pk(C),tuple(pk(D),key(E))),enc(sk(D),tuple(pk(C),key(E)))], {C>0,D>0,B>E,E>A}).


Constrained configuration: 
[fresh(_),enc(sk(A),tuple(pk(B),key(C))),mem(key(C))]:{B>0.0,A>0.0}.




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


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

****** End of trace *****
**** End Potential Attack ****
Constrained configuration: 
[fresh(_),mem(sk(A))]:{A>0.0}.




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


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

****** End of trace *****
**** End Potential Attack ***