diff -r 77bf175f5145 -r f20fbb141673 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Recur.thy	Fri Sep 26 10:34:28 2003 +0200
@@ -2,11 +2,11 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
-
-Inductive relation "recur" for the Recursive Authentication protocol.
 *)
 
-theory Recur = Shared:
+header{*The Otway-Bull Recursive Authentication Protocol*}
+
+theory Recur = Public:
 
 text{*End marker for message bundles*}
 syntax        END :: "msg"
@@ -63,26 +63,26 @@
 
          (*Alice initiates a protocol run.
            END is a placeholder to terminate the nesting.*)
-   RA1:  "[| evs1: recur;  Nonce NA \<notin> used evs1 |]
+   RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
           ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
               # evs1 \<in> recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
            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;  Nonce NB \<notin> used evs2;
+   RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
              Says A' B PA \<in> set evs2 |]
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs2 \<in> recur"
 
          (*The Server receives Bob's message and prepares a response.*)
-   RA3:  "[| evs3: recur;  Says B' Server PB \<in> set evs3;
+   RA3:  "[| evs3 \<in> recur;  Says B' Server PB \<in> set evs3;
              (PB,RB,K) \<in> respond evs3 |]
           ==> Says Server B RB # evs3 \<in> recur"
 
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
-   RA4:  "[| evs4: recur;
+   RA4:  "[| evs4 \<in> recur;
              Says B  C {|XH, Agent B, Agent C, Nonce NB,
                          XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
@@ -98,7 +98,7 @@
      the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
      etc.
 
-   Oops:  "[| evso: recur;  Says Server B RB \<in> set evso;
+   Oops:  "[| evso \<in> recur;  Says Server B RB \<in> set evso;
 	      RB \<in> responses evs';  Key K \<in> parts {RB} |]
            ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
   *)
@@ -129,28 +129,30 @@
 
 
 text{*Case two: Alice, Bob and the server*}
-lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K' |]
-       ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
+lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
+          Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
+       ==> \<exists>NA. \<exists>evs \<in> recur.
         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                    END|}  \<in> set evs"
-apply (cut_tac Nonce_supply2, clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
-          recur.Nil [THEN recur.RA1, 
-                     THEN recur.RA2,
-                     THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
-                     THEN recur.RA4])
-apply possibility
+          recur.Nil
+           [THEN recur.RA1 [of _ NA], 
+	    THEN recur.RA2 [of _ NB],
+	    THEN recur.RA3 [OF _ _ respond.One 
+                                     [THEN respond.Cons [of _ _ K _ K']]],
+	    THEN recur.RA4], possibility)
 apply (auto simp add: used_Cons)
 done
 
 (*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
 lemma "[| Key K \<notin> used []; Key K' \<notin> used [];  
-                       Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'' |]
+          Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'';
+          Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 
+          NA < NB; NB < NC |]
        ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
              Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                         END|}  \<in> set evs"
-apply (cut_tac Nonce_supply3, clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
@@ -163,7 +165,6 @@
 apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
 done
 
-(**** Inductive proofs about recur ****)
 
 lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
 by (erule respond.induct, simp_all)
@@ -236,12 +237,13 @@
      ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
                    (Key K \<in> analz (insert RB (Key`KK Un H))) =
                    (K \<in> KK | Key K \<in> analz (insert RB H))"
-by (erule responses.induct,
-    simp_all del: image_insert
-	     add: analz_image_freshK_simps)
+apply (erule responses.induct)
+apply (simp_all del: image_insert
+	        add: analz_image_freshK_simps, auto)
+done 
 
 
-text{*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*}
+text{*Version for the protocol.  Proof is easy, thanks to the lemma.*}
 lemma raw_analz_image_freshK:
  "evs \<in> recur ==>
    \<forall>K KK. KK \<subseteq> - (range shrK) -->
@@ -320,9 +322,10 @@
 lemma shrK_in_analz_respond [simp]:
      "[| RB \<in> responses evs;  evs \<in> recur |]
   ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
-by (erule responses.induct,
-    simp_all del: image_insert
-             add: analz_image_freshK_simps resp_analz_image_freshK)
+apply (erule responses.induct)
+apply (simp_all del: image_insert
+                add: analz_image_freshK_simps resp_analz_image_freshK, auto) 
+done
 
 
 lemma resp_analz_insert_lemma:
@@ -452,8 +455,6 @@
        drule_tac [6] RA4_parts_spies,
        drule_tac [4] RA2_parts_spies,
        simp_all)
-txt{*Nil*}
-apply force
 txt{*Fake, RA3*}
 apply (blast dest: Hash_in_parts_respond)+
 done