--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Oct 18 11:41:04 1996 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Oct 18 11:41:41 1996 +0200
@@ -70,12 +70,12 @@
(*This message models possible leaks of session keys. Alice's Nonce
identifies the protocol run.*)
- Reveal "[| evs: otway; A ~= Spy;
- Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
- : set_of_list evs;
- Says A B {|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
- : set_of_list evs |]
- ==> Says A Spy {|Nonce NA, Key K|} # evs : otway"
+ Revl "[| evs: otway; A ~= Spy;
+ Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
+ : set_of_list evs;
+ Says A B {|Nonce NA, Agent A, Agent B,
+ Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+ : set_of_list evs |]
+ ==> Says A Spy {|Nonce NA, Key K|} # evs : otway"
end