changeset 2105 | 782772e744dc |
parent 2064 | 5a5e508e2a2b |
child 2135 | 80477862ab33 |
--- a/src/HOL/Auth/OtwayRees.thy Fri Oct 18 11:38:17 1996 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Fri Oct 18 11:39:10 1996 +0200 @@ -36,7 +36,7 @@ (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field. - We modify the published protocol by NOT encrypting NB.*) + Note that NB is encrypted.*) OR2 "[| evs: otway lost; B ~= Server; Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] ==> Says B Server