diff -r e381884c09d4 -r cdc14f94c754 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Oct 13 15:38:32 2022 +0100
@@ -102,14 +102,14 @@
 
  | Fake: \<comment> \<open>The Spy may say anything he can say.  The sender field is correct,
           but agents don't use that information.\<close>
-         "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
-          ==> Says Spy B X # evsf \<in> tls"
+         "\<lbrakk>evsf \<in> tls;  X \<in> synth (analz (spies evsf))\<rbrakk>
+          \<Longrightarrow> Says Spy B X # evsf \<in> tls"
 
  | SpyKeys: \<comment> \<open>The spy may apply \<^term>\<open>PRF\<close> and \<^term>\<open>sessionK\<close>
                 to available nonces\<close>
-         "[| evsSK \<in> tls;
-             {Nonce NA, Nonce NB, Nonce M} \<subseteq> analz (spies evsSK) |]
-          ==> Notes Spy \<lbrace> Nonce (PRF(M,NA,NB)),
+         "\<lbrakk>evsSK \<in> tls;
+             {Nonce NA, Nonce NB, Nonce M} \<subseteq> analz (spies evsSK)\<rbrakk>
+          \<Longrightarrow> Notes Spy \<lbrace> Nonce (PRF(M,NA,NB)),
                            Key (sessionK((NA,NB,M),role))\<rbrace> # evsSK \<in> tls"
 
  | ClientHello:
@@ -120,8 +120,8 @@
            UNIX TIME is omitted because the protocol doesn't use it.
            May assume \<^term>\<open>NA \<notin> range PRF\<close> because CLIENT RANDOM is 
            28 bytes while MASTER SECRET is 48 bytes\<close>
-         "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
-          ==> Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
+         "\<lbrakk>evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF\<rbrakk>
+          \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                 # evsCH  \<in>  tls"
 
  | ServerHello:
@@ -129,14 +129,14 @@
            PB represents \<open>CLIENT_VERSION\<close>, \<open>CIPHER_SUITE\<close> and \<open>COMPRESSION_METHOD\<close>.
            SERVER CERTIFICATE (7.4.2) is always present.
            \<open>CERTIFICATE_REQUEST\<close> (7.4.4) is implied.\<close>
-         "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
+         "\<lbrakk>evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
              Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
-               \<in> set evsSH |]
-          ==> Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> # evsSH  \<in>  tls"
+               \<in> set evsSH\<rbrakk>
+          \<Longrightarrow> Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> # evsSH  \<in>  tls"
 
  | Certificate:
          \<comment> \<open>SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.\<close>
-         "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC  \<in>  tls"
+         "evsC \<in> tls \<Longrightarrow> Says B A (certificate B (pubK B)) # evsC  \<in>  tls"
 
  | ClientKeyExch:
          \<comment> \<open>CLIENT KEY EXCHANGE (7.4.7).
@@ -147,9 +147,9 @@
            both items have the same length, 48 bytes).
            The Note event records in the trace that she knows PMS
                (see REMARK at top).\<close>
-         "[| evsCX \<in> tls;  Nonce PMS \<notin> used evsCX;  PMS \<notin> range PRF;
-             Says B' A (certificate B KB) \<in> set evsCX |]
-          ==> Says A B (Crypt KB (Nonce PMS))
+         "\<lbrakk>evsCX \<in> tls;  Nonce PMS \<notin> used evsCX;  PMS \<notin> range PRF;
+             Says B' A (certificate B KB) \<in> set evsCX\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt KB (Nonce PMS))
               # Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>
               # evsCX  \<in>  tls"
 
@@ -159,10 +159,10 @@
           It adds the pre-master-secret, which is also essential!
           Checking the signature, which is the only use of A's certificate,
           assures B of A's presence\<close>
-         "[| evsCV \<in> tls;
+         "\<lbrakk>evsCV \<in> tls;
              Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCV;
-             Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCV |]
-          ==> Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>))
+             Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCV\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>))
               # evsCV  \<in>  tls"
 
         \<comment> \<open>Finally come the FINISHED messages (7.4.8), confirming PA and PB
@@ -176,13 +176,13 @@
           Spy does not know PMS and could not send ClientFinished.  One
           could simply put \<^term>\<open>A\<noteq>Spy\<close> into the rule, but one should not
           expect the spy to be well-behaved.\<close>
-         "[| evsCF \<in> tls;
+         "\<lbrakk>evsCF \<in> tls;
              Says A  B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                \<in> set evsCF;
              Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCF;
              Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCF;
-             M = PRF(PMS,NA,NB) |]
-          ==> Says A B (Crypt (clientK(NA,NB,M))
+             M = PRF(PMS,NA,NB)\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (clientK(NA,NB,M))
                         (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
                                Nonce NB, Number PB, Agent B\<rbrace>))
@@ -191,13 +191,13 @@
  | ServerFinished:
         \<comment> \<open>Keeping A' and A'' distinct means B cannot even check that the
           two messages originate from the same source.\<close>
-         "[| evsSF \<in> tls;
+         "\<lbrakk>evsSF \<in> tls;
              Says A' B  \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                \<in> set evsSF;
              Says B  A  \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSF;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF;
-             M = PRF(PMS,NA,NB) |]
-          ==> Says B A (Crypt (serverK(NA,NB,M))
+             M = PRF(PMS,NA,NB)\<rbrakk>
+          \<Longrightarrow> Says B A (Crypt (serverK(NA,NB,M))
                         (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
                                Nonce NB, Number PB, Agent B\<rbrace>))
@@ -208,15 +208,15 @@
           message encrypted with serverK, the client stores the parameters
           needed to resume this session.  The "Notes A ..." premise is
           used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close>
-         "[| evsCA \<in> tls;
+         "\<lbrakk>evsCA \<in> tls;
              Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCA;
              M = PRF(PMS,NA,NB);
              X = Hash\<lbrace>Number SID, Nonce M,
                        Nonce NA, Number PA, Agent A,
                        Nonce NB, Number PB, Agent B\<rbrace>;
              Says A  B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA;
-             Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |]
-          ==>
+             Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA\<rbrakk>
+          \<Longrightarrow>
              Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsCA  \<in>  tls"
 
  | ServerAccepts:
@@ -224,7 +224,7 @@
           message encrypted with clientK, the server stores the parameters
           needed to resume this session.  The "Says A'' B ..." premise is
           used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close>
-         "[| evsSA \<in> tls;
+         "\<lbrakk>evsSA \<in> tls;
              A \<noteq> B;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
              M = PRF(PMS,NA,NB);
@@ -232,18 +232,18 @@
                        Nonce NA, Number PA, Agent A,
                        Nonce NB, Number PB, Agent B\<rbrace>;
              Says B  A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA;
-             Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |]
-          ==>
+             Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA\<rbrakk>
+          \<Longrightarrow>
              Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsSA  \<in>  tls"
 
  | ClientResume:
          \<comment> \<open>If A recalls the \<open>SESSION_ID\<close>, then she sends a FINISHED
              message using the new nonces and stored MASTER SECRET.\<close>
-         "[| evsCR \<in> tls;
+         "\<lbrakk>evsCR \<in> tls;
              Says A  B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> \<in> set evsCR;
              Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCR;
-             Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsCR |]
-          ==> Says A B (Crypt (clientK(NA,NB,M))
+             Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsCR\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (clientK(NA,NB,M))
                         (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
                                Nonce NB, Number PB, Agent B\<rbrace>))
@@ -252,11 +252,11 @@
  | ServerResume:
          \<comment> \<open>Resumption (7.3):  If B finds the \<open>SESSION_ID\<close> then he can 
              send a FINISHED message using the recovered MASTER SECRET\<close>
-         "[| evsSR \<in> tls;
+         "\<lbrakk>evsSR \<in> tls;
              Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> \<in> set evsSR;
              Says B  A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSR;
-             Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsSR |]
-          ==> Says B A (Crypt (serverK(NA,NB,M))
+             Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsSR\<rbrakk>
+          \<Longrightarrow> Says B A (Crypt (serverK(NA,NB,M))
                         (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
                                Nonce NB, Number PB, Agent B\<rbrace>)) # evsSR
@@ -268,9 +268,9 @@
            rather unlikely.  The assumption \<^term>\<open>A\<noteq>Spy\<close> is essential: 
            otherwise the Spy could learn session keys merely by 
            replaying messages!\<close>
-         "[| evso \<in> tls;  A \<noteq> Spy;
-             Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
-          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
+         "\<lbrakk>evso \<in> tls;  A \<noteq> Spy;
+             Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso\<rbrakk>
+          \<Longrightarrow> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
 
 (*
 Protocol goals:
@@ -331,8 +331,8 @@
 
 
 text\<open>Possibility property ending with ClientAccepts.\<close>
-lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
-      ==> \<exists>SID M. \<exists>evs \<in> tls.
+lemma "\<lbrakk>\<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B\<rbrakk>
+      \<Longrightarrow> \<exists>SID M. \<exists>evs \<in> tls.
             Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] tls.Nil
@@ -344,8 +344,8 @@
 
 
 text\<open>And one for ServerAccepts.  Either FINISHED message may come first.\<close>
-lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
-      ==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
+lemma "\<lbrakk>\<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B\<rbrakk>
+      \<Longrightarrow> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
            Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] tls.Nil
@@ -357,8 +357,8 @@
 
 
 text\<open>Another one, for CertVerify (which is optional)\<close>
-lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
-       ==> \<exists>NB PMS. \<exists>evs \<in> tls.
+lemma "\<lbrakk>\<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B\<rbrakk>
+       \<Longrightarrow> \<exists>NB PMS. \<exists>evs \<in> tls.
               Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>)) 
                 \<in> set evs"
 apply (intro exI bexI)
@@ -371,12 +371,12 @@
 
 text\<open>Another one, for session resumption (both ServerResume and ClientResume).
   NO tls.Nil here: we refer to a previous session, not the empty trace.\<close>
-lemma "[| evs0 \<in> tls;
+lemma "\<lbrakk>evs0 \<in> tls;
           Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
           Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
           \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF;
-          A \<noteq> B |]
-      ==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls.
+          A \<noteq> B\<rbrakk>
+      \<Longrightarrow> \<exists>NA PA NB PB X. \<exists>evs \<in> tls.
                 X = Hash\<lbrace>Number SID, Nonce M,
                           Nonce NA, Number PA, Agent A,
                           Nonce NB, Number PB, Agent B\<rbrace>  \<and>
@@ -397,15 +397,15 @@
 
 text\<open>Spy never sees a good agent's private key!\<close>
 lemma Spy_see_priK [simp]:
-     "evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
+     "evs \<in> tls \<Longrightarrow> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
 by (erule tls.induct, force, simp_all, blast)
 
 lemma Spy_analz_priK [simp]:
-     "evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)"
+     "evs \<in> tls \<Longrightarrow> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)"
 by auto
 
 lemma Spy_see_priK_D [dest!]:
-    "[|Key (privateKey b A) \<in> parts (knows Spy evs);  evs \<in> tls|] ==> A \<in> bad"
+    "\<lbrakk>Key (privateKey b A) \<in> parts (knows Spy evs);  evs \<in> tls\<rbrakk> \<Longrightarrow> A \<in> bad"
 by (blast dest: Spy_see_priK)
 
 
@@ -414,7 +414,7 @@
   little point in doing so: the loss of their private keys is a worse
   breach of security.\<close>
 lemma certificate_valid:
-    "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
+    "\<lbrakk>certificate B KB \<in> parts (spies evs);  evs \<in> tls\<rbrakk> \<Longrightarrow> KB = pubK B"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all, blast) 
 done
@@ -425,8 +425,8 @@
 subsubsection\<open>Properties of items found in Notes\<close>
 
 lemma Notes_Crypt_parts_spies:
-     "[| Notes A \<lbrace>Agent B, X\<rbrace> \<in> set evs;  evs \<in> tls |]
-      ==> Crypt (pubK B) X \<in> parts (spies evs)"
+     "\<lbrakk>Notes A \<lbrace>Agent B, X\<rbrace> \<in> set evs;  evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Crypt (pubK B) X \<in> parts (spies evs)"
 apply (erule rev_mp)
 apply (erule tls.induct, 
        frule_tac [7] CX_KB_is_pubKB, force, simp_all)
@@ -435,9 +435,9 @@
 
 text\<open>C may be either A or B\<close>
 lemma Notes_master_imp_Crypt_PMS:
-     "[| Notes C \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
-         evs \<in> tls |]
-      ==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
+     "\<lbrakk>Notes C \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all)
 txt\<open>Fake\<close>
@@ -448,9 +448,9 @@
 
 text\<open>Compared with the theorem above, both premise and conclusion are stronger\<close>
 lemma Notes_master_imp_Notes_PMS:
-     "[| Notes A \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
-         evs \<in> tls |]
-      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
+     "\<lbrakk>Notes A \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all)
 txt\<open>ServerAccepts\<close>
@@ -462,45 +462,45 @@
 
 text\<open>B can check A's signature if he has received A's certificate.\<close>
 lemma TrustCertVerify_lemma:
-     "[| X \<in> parts (spies evs);
+     "\<lbrakk>X \<in> parts (spies evs);
          X = Crypt (priK A) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
-         evs \<in> tls;  A \<notin> bad |]
-      ==> Says A B X \<in> set evs"
+         evs \<in> tls;  A \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says A B X \<in> set evs"
 apply (erule rev_mp, erule ssubst)
 apply (erule tls.induct, force, simp_all, blast)
 done
 
 text\<open>Final version: B checks X using the distributed KA instead of priK A\<close>
 lemma TrustCertVerify:
-     "[| X \<in> parts (spies evs);
+     "\<lbrakk>X \<in> parts (spies evs);
          X = Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
          certificate A KA \<in> parts (spies evs);
-         evs \<in> tls;  A \<notin> bad |]
-      ==> Says A B X \<in> set evs"
+         evs \<in> tls;  A \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says A B X \<in> set evs"
 by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)
 
 
 text\<open>If CertVerify is present then A has chosen PMS.\<close>
 lemma UseCertVerify_lemma:
-     "[| Crypt (priK A) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) \<in> parts (spies evs);
-         evs \<in> tls;  A \<notin> bad |]
-      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
+     "\<lbrakk>Crypt (priK A) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) \<in> parts (spies evs);
+         evs \<in> tls;  A \<notin> bad\<rbrakk>
+      \<Longrightarrow> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all, blast)
 done
 
 text\<open>Final version using the distributed KA instead of priK A\<close>
 lemma UseCertVerify:
-     "[| Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>)
+     "\<lbrakk>Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>)
            \<in> parts (spies evs);
          certificate A KA \<in> parts (spies evs);
-         evs \<in> tls;  A \<notin> bad |]
-      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
+         evs \<in> tls;  A \<notin> bad\<rbrakk>
+      \<Longrightarrow> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 by (blast dest!: certificate_valid intro!: UseCertVerify_lemma)
 
 
 lemma no_Notes_A_PRF [simp]:
-     "evs \<in> tls ==> Notes A \<lbrace>Agent B, Nonce (PRF x)\<rbrace> \<notin> set evs"
+     "evs \<in> tls \<Longrightarrow> Notes A \<lbrace>Agent B, Nonce (PRF x)\<rbrace> \<notin> set evs"
 apply (erule tls.induct, force, simp_all)
 txt\<open>ClientKeyExch: PMS is assumed to differ from any PRF.\<close>
 apply blast
@@ -508,8 +508,8 @@
 
 
 lemma MS_imp_PMS [dest!]:
-     "[| Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs);  evs \<in> tls |]
-      ==> Nonce PMS \<in> parts (spies evs)"
+     "\<lbrakk>Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs);  evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Nonce PMS \<in> parts (spies evs)"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all)
 txt\<open>Fake\<close>
@@ -525,11 +525,11 @@
 
 text\<open>PMS determines B.\<close>
 lemma Crypt_unique_PMS:
-     "[| Crypt(pubK B)  (Nonce PMS) \<in> parts (spies evs);
+     "\<lbrakk>Crypt(pubK B)  (Nonce PMS) \<in> parts (spies evs);
          Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs);
          Nonce PMS \<notin> analz (spies evs);
-         evs \<in> tls |]
-      ==> B=B'"
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> B=B'"
 apply (erule rev_mp, erule rev_mp, erule rev_mp)
 apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
 txt\<open>Fake, ClientKeyExch\<close>
@@ -545,10 +545,10 @@
 
 text\<open>In A's internal Note, PMS determines A and B.\<close>
 lemma Notes_unique_PMS:
-     "[| Notes A  \<lbrace>Agent B,  Nonce PMS\<rbrace> \<in> set evs;
+     "\<lbrakk>Notes A  \<lbrace>Agent B,  Nonce PMS\<rbrace> \<in> set evs;
          Notes A' \<lbrace>Agent B', Nonce PMS\<rbrace> \<in> set evs;
-         evs \<in> tls |]
-      ==> A=A' \<and> B=B'"
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> A=A' \<and> B=B'"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, force, simp_all)
 txt\<open>ClientKeyExch\<close>
@@ -562,7 +562,7 @@
   No collection of keys can help the spy get new private keys.\<close>
 lemma analz_image_priK [rule_format]:
      "evs \<in> tls
-      ==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK \<union> (spies evs))) =
+      \<Longrightarrow> \<forall>KK. (Key(priK B) \<in> analz (Key`KK \<union> (spies evs))) =
           (priK B \<in> KK | B \<in> bad)"
 apply (erule tls.induct)
 apply (simp_all (no_asm_simp)
@@ -582,7 +582,7 @@
 
 text\<open>Lemma for the trivial direction of the if-and-only-if\<close>
 lemma analz_image_keys_lemma:
-     "(X \<in> analz (G \<union> H)) \<longrightarrow> (X \<in> analz H)  ==>
+     "(X \<in> analz (G \<union> H)) \<longrightarrow> (X \<in> analz H)  \<Longrightarrow>
       (X \<in> analz (G \<union> H))  =  (X \<in> analz H)"
 by (blast intro: analz_mono [THEN subsetD])
 
@@ -592,7 +592,7 @@
 **)
 
 lemma analz_image_keys [rule_format]:
-     "evs \<in> tls ==>
+     "evs \<in> tls \<Longrightarrow>
       \<forall>KK. KK \<subseteq> range sessionK \<longrightarrow>
               (Nonce N \<in> analz (Key`KK \<union> (spies evs))) =
               (Nonce N \<in> analz (spies evs))"
@@ -611,7 +611,7 @@
 
 text\<open>Knowing some session keys is no help in getting new nonces\<close>
 lemma analz_insert_key [simp]:
-     "evs \<in> tls ==>
+     "evs \<in> tls \<Longrightarrow>
       (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
       (Nonce N \<in> analz (spies evs))"
 by (simp del: image_insert
@@ -628,10 +628,10 @@
   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   THEY ARE NOT SUITABLE AS SAFE ELIM RULES.\<close>
 lemma PMS_lemma:
-     "[| Nonce PMS \<notin> parts (spies evs);
+     "\<lbrakk>Nonce PMS \<notin> parts (spies evs);
          K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
-         evs \<in> tls |]
-   ==> Key K \<notin> parts (spies evs) \<and> (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
+         evs \<in> tls\<rbrakk>
+   \<Longrightarrow> Key K \<notin> parts (spies evs) \<and> (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
 apply (erule rev_mp, erule ssubst)
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 
 apply (force, simp_all (no_asm_simp))
@@ -644,15 +644,15 @@
 done
 
 lemma PMS_sessionK_not_spied:
-     "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs);
-         evs \<in> tls |]
-      ==> Nonce PMS \<in> parts (spies evs)"
+     "\<lbrakk>Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs);
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Nonce PMS \<in> parts (spies evs)"
 by (blast dest: PMS_lemma)
 
 lemma PMS_Crypt_sessionK_not_spied:
-     "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y
-           \<in> parts (spies evs);  evs \<in> tls |]
-      ==> Nonce PMS \<in> parts (spies evs)"
+     "\<lbrakk>Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y
+           \<in> parts (spies evs);  evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Nonce PMS \<in> parts (spies evs)"
 by (blast dest: PMS_lemma)
 
 text\<open>Write keys are never sent if M (MASTER SECRET) is secure.
@@ -661,9 +661,9 @@
   with some effort.
   NO LONGER USED: see \<open>clientK_not_spied\<close> and \<open>serverK_not_spied\<close>\<close>
 lemma sessionK_not_spied:
-     "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
-         Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
-      ==> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)"
+     "\<lbrakk>\<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
+         Nonce M \<notin> analz (spies evs);  evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, analz_mono_contra)
 apply (force, simp_all (no_asm_simp))
@@ -674,9 +674,9 @@
 
 text\<open>If A sends ClientKeyExch to an honest B, then the PMS will stay secret.\<close>
 lemma Spy_not_see_PMS:
-     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
-         evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Nonce PMS \<notin> analz (spies evs)"
+     "\<lbrakk>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
+         evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Nonce PMS \<notin> analz (spies evs)"
 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all (no_asm_simp))
 txt\<open>Fake\<close>
@@ -696,9 +696,9 @@
 text\<open>If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   will stay secret.\<close>
 lemma Spy_not_see_MS:
-     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
-         evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
+     "\<lbrakk>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
+         evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all (no_asm_simp))
 txt\<open>Fake\<close>
@@ -719,10 +719,10 @@
 text\<open>If A created PMS then nobody else (except the Spy in replays)
   would send a message using a clientK generated from that PMS.\<close>
 lemma Says_clientK_unique:
-     "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
+     "\<lbrakk>Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
          Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
-         evs \<in> tls;  A' \<noteq> Spy |]
-      ==> A = A'"
+         evs \<in> tls;  A' \<noteq> Spy\<rbrakk>
+      \<Longrightarrow> A = A'"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all)
@@ -737,11 +737,11 @@
 text\<open>If A created PMS and has not leaked her clientK to the Spy,
   then it is completely secure: not even in parts!\<close>
 lemma clientK_not_spied:
-     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
+     "\<lbrakk>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;
-         evs \<in> tls |]
-      ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
+         evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all (no_asm_simp))
@@ -761,10 +761,10 @@
 text\<open>If A created PMS for B, then nobody other than B or the Spy would
   send a message using a serverK generated from that PMS.\<close>
 lemma Says_serverK_unique:
-     "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
+     "\<lbrakk>Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
          Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
-         evs \<in> tls;  A \<notin> bad;  B \<notin> bad;  B' \<noteq> Spy |]
-      ==> B = B'"
+         evs \<in> tls;  A \<notin> bad;  B \<notin> bad;  B' \<noteq> Spy\<rbrakk>
+      \<Longrightarrow> B = B'"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all)
@@ -779,10 +779,10 @@
 text\<open>If A created PMS for B, and B has not leaked his serverK to the Spy,
   then it is completely secure: not even in parts!\<close>
 lemma serverK_not_spied:
-     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
+     "\<lbrakk>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
-         A \<notin> bad;  B \<notin> bad;  evs \<in> tls |]
-      ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
+         A \<notin> bad;  B \<notin> bad;  evs \<in> tls\<rbrakk>
+      \<Longrightarrow> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
 apply (erule rev_mp, erule rev_mp)
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
 apply (force, simp_all (no_asm_simp))
@@ -803,13 +803,13 @@
 
 text\<open>The mention of her name (A) in X assures A that B knows who she is.\<close>
 lemma TrustServerFinished [rule_format]:
-     "[| X = Crypt (serverK(Na,Nb,M))
+     "\<lbrakk>X = Crypt (serverK(Na,Nb,M))
                (Hash\<lbrace>Number SID, Nonce M,
                       Nonce Na, Number PA, Agent A,
                       Nonce Nb, Number PB, Agent B\<rbrace>);
          M = PRF(PMS,NA,NB);
-         evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
+         evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
           Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow>
           X \<in> parts (spies evs) \<longrightarrow> Says B A X \<in> set evs"
 apply (erule ssubst)+
@@ -827,8 +827,8 @@
   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   to bind A's identity with PMS, then we could replace A' by A below.\<close>
 lemma TrustServerMsg [rule_format]:
-     "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
+     "\<lbrakk>M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
           Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow>
           Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs)  \<longrightarrow>
           (\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)"
@@ -853,8 +853,8 @@
      ClientFinished, then B can then check the quoted values PA, PB, etc.\<close>
 
 lemma TrustClientMsg [rule_format]:
-     "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
+     "\<lbrakk>M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs \<longrightarrow>
           Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow>
           Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) \<longrightarrow>
           Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
@@ -874,14 +874,14 @@
      check a CertVerify from A, then A has used the quoted
      values PA, PB, etc.  Even this one requires A to be uncompromised.\<close>
 lemma AuthClientFinished:
-     "[| M = PRF(PMS,NA,NB);
+     "\<lbrakk>M = PRF(PMS,NA,NB);
          Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
          Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs;
          certificate A KA \<in> parts (spies evs);
          Says A'' B (Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>))
            \<in> set evs;
-         evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
-      ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
+         evs \<in> tls;  A \<notin> bad;  B \<notin> bad\<rbrakk>
+      \<Longrightarrow> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
 by (blast intro!: TrustClientMsg UseCertVerify)
 
 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)