**** Protocol: Needham-Schroeder **** **** Unsafe States **** [unsafe([step2(A,tuple(B,_,C)),mem(C)],{B>0,A>0})]. **** Potential Attacks **** Constrained configuration: [fresh(_)]:{}. Rule: alice_starts_a_session_with_trudy rule([fresh(A)], [fresh(B),step1(C,tuple(0,D)),mem(D)], {C>0,B>D,D>A}). Constrained configuration: [fresh(_),mem(A)]:{A>0.0}. Rule: trudy_starts_a_session_with_Bob rule([fresh(A),mem(B)], [fresh(C),step2(B,tuple(D,E,F)),mem(B),mem(E),mem(F)], {D>=0,B>0,C>E,E>F,F>A}). Unsafe state: [step2(A,tuple(B,_,C)),mem(C)]:{B>0,A>0}. ****** End of trace ***** **** End Potential Attack **** Constrained configuration: [mem(A),fresh(_),mem(A)]:{}. Rule: compromised_key rule([mem(A)], [step1(B,tuple(C,A)),enc(C,tuple(B,A))], {B>0,C>0}). Constrained configuration: [fresh(_),enc(A,tuple(B,C)),mem(C)]:{B>0.0,A>0.0}. Rule: trudy_knows_the_secret rule([fresh(A),enc(B,tuple(C,D)),mem(D)], [fresh(E),step2(B,tuple(C,D,F)),enc(D,tuple(F)),mem(D),mem(F)], {C>0,B>0,E>F,F>A}). Unsafe state: [step2(A,tuple(B,_,C)),mem(C)]:{B>0,A>0}. ****** End of trace ***** **** End Potential Attack **** Constrained configuration: [fresh(_),mem(A)]:{A>0.0}. Rule: trudy_starts_a_session_with_Bob rule([fresh(A),mem(B)], [fresh(C),step2(B,tuple(D,E,F)),mem(B),mem(E),mem(F)], {D>=0,B>0,C>E,E>F,F>A}). Unsafe state: [step2(A,tuple(B,_,C)),mem(C)]:{B>0,A>0}. ****** End of trace ***** **** End Potential Attack ****