diff -r 41fa62c229c3 -r bb8ff763c93d src/HOL/Auth/Recur.thy --- 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"