src/HOL/Auth/Recur.thy
 changeset 3465 e85c24717cad parent 2550 8d8344bcf98a child 3466 30791e5a69c4
```--- a/src/HOL/Auth/Recur.thy	Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Recur.thy	Thu Jun 26 13:20:50 1997 +0200
@@ -75,14 +75,14 @@
NOTE: existing proofs don't need PA and are complicated by its
presence!  See parts_Fake_tac.*)
RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B PA : set_of_list evs;
+             Says A' B PA : set evs;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs : recur lost"

(*The Server receives Bob's message and prepares a response.*)
RA3  "[| evs: recur lost;  B ~= Server;
-             Says B' Server PB : set_of_list evs;
+             Says B' Server PB : set evs;
(PB,RB,K) : respond evs |]
==> Says Server B RB # evs : recur lost"

@@ -91,11 +91,11 @@
RA4  "[| evs: recur lost;  A ~= B;
Says B  C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|}
-               : set_of_list evs;
+               : set evs;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|}
-               : set_of_list evs |]
+               : set evs |]
==> Says B A RA # evs : recur lost"

(**No "oops" message can readily be expressed, since each session key is```