diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Recur.thy	Fri Jan 17 12:49:31 1997 +0100
@@ -8,56 +8,47 @@
 
 Recur = Shared +
 
-syntax
-  newK2    :: "nat*nat => key"
-
-translations
-  "newK2 x"  == "newK(nPair x)"
-
 (*Two session keys are distributed to each agent except for the initiator,
-	who receives one.
+        who receives one.
   Perhaps the two session keys could be bundled into a single message.
 *)
-consts     respond :: "nat => (nat*msg*msg)set"
-inductive "respond i"	(*Server's response to the nested message*)
+consts     respond :: "event list => (msg*msg*key)set"
+inductive "respond evs" (*Server's response to the nested message*)
   intrs
     (*The message "Agent Server" marks the end of a list.*)
 
-    One  "A ~= Server
-          ==> (j, HPair (Key(shrK A)) 
+    One  "[| A ~= Server;  Key KAB ~: used evs |]
+          ==> (Hash[Key(shrK A)] 
                         {|Agent A, Agent B, Nonce NA, Agent Server|}, 
-                  {|Agent A, 
-                    Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|}, 
-                    Agent Server|})
-              : respond i"
+               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
+               KAB)   : respond evs"
 
     (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
-    Cons "[| (Suc j, PA, RA) : respond i;
-             PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|};
+    Cons "[| (PA, RA, KAB) : respond evs;  
+             Key KBC ~: used evs;  Key KBC ~: parts {RA};
+             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
              B ~= Server |]
-          ==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|}, 
-                  {|Agent B, 
-                    Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
-                    Agent B, 
-                    Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, 
-                    RA|})
-              : respond i"
+          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
+               {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+                 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+                 RA|},
+               KBC)
+              : respond evs"
 
 
 (*Induction over "respond" can be difficult due to the complexity of the
   subgoals.  The "responses" relation formalizes the general form of its
   third component.
 *)
-consts     responses :: nat => msg set
-inductive "responses i" 	
+consts     responses :: event list => msg set
+inductive "responses evs"       
   intrs
     (*Server terminates lists*)
-    Nil  "Agent Server : responses i"
+    Nil  "Agent Server : responses evs"
 
-    Cons "RA : responses i
-          ==> {|Agent B, 
-                Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|},
-                RA|}  : responses i"
+    Cons "[| RA : responses evs;  Key KAB ~: used evs |]
+          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+                RA|}  : responses evs"
 
 
 consts     recur   :: agent set => event list set
@@ -75,40 +66,36 @@
 
          (*Alice initiates a protocol run.
            "Agent Server" is just a placeholder, to terminate the nesting.*)
-    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server |]
+    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
           ==> Says A B 
-                (HPair (Key(shrK A)) 
-                 {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|})
+                (Hash[Key(shrK A)] 
+                 {|Agent A, Agent B, Nonce NA, Agent Server|})
               # evs : recur lost"
 
          (*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.
+                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.*)
-    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
+                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;  
              PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
-          ==> Says B C 
-                (HPair (Key(shrK B))
-                 {|Agent B, Agent C, Nonce (newN(length evs)), PA|})
+          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs : recur lost"
 
          (*The Server receives and decodes Bob's message.  Then he generates
            a new session key and a response.*)
     RA3  "[| evs: recur lost;  B ~= Server;
              Says B' Server PB : set_of_list evs;
-             (0,PB,RB) : respond (length evs) |]
+             (PB,RB,K) : respond evs |]
           ==> Says Server B RB # evs : recur lost"
 
          (*Bob receives the returned message and compares the Nonces with
-	   those in the message he previously sent the Server.*)
+           those in the message he previously sent the Server.*)
     RA4  "[| evs: recur lost;  A ~= B;  
-             Says C' B {|Agent B, 
-                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         Agent B, 
-                         Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
+             Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
+                         Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
                : set_of_list evs;
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
                          XA, Agent A, Agent B, Nonce NA, P|}