src/HOL/Auth/Recur.thy

 (*Two session keys are distributed to each agent except for the initiator,
         who receives one.
   Perhaps the two session keys could be bundled into a single message.
 *)
 inductive_set (*Server's response to the nested message*)
-  respond :: "event list => (msg*msg*key)set"
+  respond :: "event list \<Rightarrow> (msg*msg*key)set"
   for evs :: "event list"
   where
    One:  "Key KAB \<notin> used evs
           ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>,
                \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>,

 (*Version for "responses" relation.  Handles case RA3 in the theorem below.
   Note that it holds for *any* set H (not just "spies evs")
   satisfying the inductive hypothesis.*)
 lemma resp_analz_image_freshK_lemma:
      "[| RB \<in> responses evs;
-         \<forall>K KK. KK \<subseteq> - (range shrK) -->
-                   (Key K \<in> analz (Key`KK Un H)) =
+         \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+                   (Key K \<in> analz (Key`KK \<union> H)) =
                    (K \<in> KK | Key K \<in> analz H) |]
-     ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
-                   (Key K \<in> analz (insert RB (Key`KK Un H))) =
+     ==> \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+                   (Key K \<in> analz (insert RB (Key`KK \<union> H))) =
                    (K \<in> KK | Key K \<in> analz (insert RB H))"
 apply (erule responses.induct)
 apply (simp_all del: image_insert
                 add: analz_image_freshK_simps, auto)
 done 
 
 
 text\<open>Version for the protocol.  Proof is easy, thanks to the lemma.\<close>
 lemma raw_analz_image_freshK:
  "evs \<in> recur ==>
-   \<forall>K KK. KK \<subseteq> - (range shrK) -->
-          (Key K \<in> analz (Key`KK Un (spies evs))) =
+   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+          (Key K \<in> analz (Key`KK \<union> (spies evs))) =
           (K \<in> KK | Key K \<in> analz (spies evs))"
 apply (erule recur.induct)
 apply (drule_tac [4] RA2_analz_spies,
        drule_tac [5] respond_imp_responses,
        drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)

 done
 
 
 (*Instance of the lemma with H replaced by (spies evs):
    [| RB \<in> responses evs;  evs \<in> recur; |]
-   ==> KK \<subseteq> - (range shrK) -->
-       Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
+   ==> KK \<subseteq> - (range shrK) \<longrightarrow>
+       Key K \<in> analz (insert RB (Key`KK \<union> spies evs)) =
        (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
 *)
 lemmas resp_analz_image_freshK =  
        resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
 

 
 lemma unique_NA:
   "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs);
       Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs);
       evs \<in> recur;  A \<notin> bad |]
-    ==> B=B' & P=P'"
+    ==> B=B' \<and> P=P'"
 apply (erule rev_mp, erule rev_mp)
 apply (erule recur.induct,
        drule_tac [5] respond_imp_responses)
 apply (force, simp_all)
 txt\<open>Fake\<close>

       (relations "respond" and "responses")
 ***)
 
 lemma shrK_in_analz_respond [simp]:
      "[| RB \<in> responses evs;  evs \<in> recur |]
-  ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
+  ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B\<in>bad)"
 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:
      "[| Key K \<in> analz (insert RB H);
-         \<forall>K KK. KK \<subseteq> - (range shrK) -->
-                   (Key K \<in> analz (Key`KK Un H)) =
+         \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+                   (Key K \<in> analz (Key`KK \<union> H)) =
                    (K \<in> KK | Key K \<in> analz H);
          RB \<in> responses evs |]
      ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
 apply (erule rev_mp, erule responses.induct)
 apply (simp_all del: image_insert parts_image

   possibilities.  Also, the presence of two different matching messages in
   the inductive step complicates the case analysis.  Unusually for such proofs,
   the quantifiers appear to be necessary.*)
 lemma unique_lemma [rule_format]:
      "(PB,RB,KXY) \<in> respond evs ==>
-      \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} -->
-      (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} -->
-      (A'=A & B'=B) | (A'=B & B'=A))"
+      \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} \<longrightarrow>
+      (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} \<longrightarrow>
+      (A'=A \<and> B'=B) | (A'=B \<and> B'=A))"
 apply (erule respond.induct)
 apply (simp_all add: all_conj_distrib)
 apply (blast dest: respond_certificate)
 done
 
 lemma unique_session_keys:
      "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB};
          Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB};
          (PB,RB,KXY) \<in> respond evs |]
-      ==> (A'=A & B'=B) | (A'=B & B'=A)"
+      ==> (A'=A \<and> B'=B) | (A'=B \<and> B'=A)"
 by (rule unique_lemma, auto)
 
 
 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
     Does not in itself guarantee security: an attack could violate
     the premises, e.g. by having A=Spy **)
 
 lemma respond_Spy_not_see_session_key [rule_format]:
      "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
-      ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
-          Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} -->
+      ==> \<forall>A A' N. A \<notin> bad \<and> A' \<notin> bad \<longrightarrow>
+          Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} \<longrightarrow>
           Key K \<notin> analz (insert RB (spies evs))"
 apply (erule respond.induct)
 apply (frule_tac [2] respond_imp_responses)
 apply (frule_tac [2] respond_imp_not_used)
 apply (simp_all del: image_insert parts_image

 
 text\<open>Certificates can only originate with the Server.\<close>
 lemma Cert_imp_Server_msg:
      "[| Crypt (shrK A) Y \<in> parts (spies evs);
          A \<notin> bad;  evs \<in> recur |]
-      ==> \<exists>C RC. Says Server C RC \<in> set evs  &
+      ==> \<exists>C RC. Says Server C RC \<in> set evs  \<and>
                    Crypt (shrK A) Y \<in> parts {RC}"
 apply (erule rev_mp, erule recur.induct, simp_all)
 txt\<open>Fake\<close>
 apply blast
 txt\<open>RA1\<close>