--- a/src/HOL/Auth/Recur.thy Sat Jan 10 17:58:42 1998 +0100
+++ b/src/HOL/Auth/Recur.thy Sat Jan 10 17:59:32 1998 +0100
@@ -69,14 +69,10 @@
# evs1 : recur"
(*Bob's response to Alice's message. C might be the Server.
- XA should be the Hash of the remaining components with KA, but
- Bob cannot check that.
- P is the previous recur message from Alice's caller.
- NOTE: existing proofs don't need PA and are complicated by its
- presence! See parts_Fake_tac.*)
+ We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
+ it complicates proofs, so B may respond to any message at all!*)
RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2;
- Says A' B PA : set evs2;
- PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
+ Says A' B PA : set evs2 |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs2 : recur"