changeset 32960 | 69916a850301 |
parent 23746 | a455e69c31cc |
child 37936 | 1e4c5015a72e |
--- a/src/HOL/Auth/Yahalom2.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/Auth/Yahalom2.thy Sat Oct 17 14:43:18 2009 +0200 @@ -51,7 +51,7 @@ Both agents are quoted in the 2nd certificate to prevent attacks!*) | YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; Gets Server {|Agent B, Nonce NB, - Crypt (shrK B) {|Agent A, Nonce NA|}|} + Crypt (shrK B) {|Agent A, Nonce NA|}|} \<in> set evs3 |] ==> Says Server A {|Nonce NB,