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


**** Potential Attacks ****

**** Unsafe States ****

unsafe([step3(A,tuple(B,_,C)),mem(B)],{A>0,C>0}),
unsafe([step3(A,tuple(_,D,C)),mem(D)],{A>0,C>0}),
unsafe([step4(C,tuple(B,_,A)),mem(B)],{A>0,C>0}),
unsafe([step4(C,tuple(_,D,A)),mem(D)],{A>0,C>0})].

**** Trace 1 **** (Type Flaw)

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

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


Constrained configuration: 
[fresh(A),step1(B,tuple(C,D)),enc(B,tuple(C,E))]:{B>0.0,D>0.0,E-A>0.0}.


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


Constrained configuration: 
[step1(A,tuple(B,C)),enc(A,tuple(B,D)),mem(D)]:{A>0.0,C>0.0}.


Rule: third
rule([step1(A,tuple(B,C)),enc(A,tuple(B,D))], [step3(A,tuple(B,D,C)),enc(C,tuple(D))], {A>0,C>0}).


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

****** End of trace *****

**** Trace 2 **** (Type Flaw)

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

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


Constrained configuration: 
[step1(A,tuple(B,C)),enc(A,tuple(B,D)),mem(D)]:{A>0.0,C>0.0}.

Rule: third
rule([step1(A,tuple(B,C)),enc(A,tuple(B,D))], [step3(A,tuple(B,D,C)),enc(C,tuple(D))], {A>0,C>0}).


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

****** End of trace *****



**** Unsafe States ****

unsafe([step4(A,tuple(B,_,C)),mem(B)],{C>0,A>0})
unsafe([step4(A,tuple(_,D,C)),mem(D)],{C>0,A>0})

**** Trace 1 **** (Lowe's attack)

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


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


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

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


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


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


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


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


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

****** End of trace *****