src/HOL/Auth/TLS.thy

   --{*sessionK never clashes with a long-term symmetric key  
      (they don't exist in TLS anyway)*}
   sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A"
 
 
-consts    tls :: "event list set"
-inductive tls
-  intros
+inductive_set tls :: "event list set"
+  where
    Nil:  --{*The initial, empty trace*}
          "[] \<in> tls"
 
-   Fake: --{*The Spy may say anything he can say.  The sender field is correct,
+ | Fake: --{*The Spy may say anything he can say.  The sender field is correct,
           but agents don't use that information.*}
          "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
           ==> Says Spy B X # evsf \<in> tls"
 
-   SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK}
+ | SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK}
                 to available nonces*}
          "[| evsSK \<in> tls;
 	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
           ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
 			   Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
 
-   ClientHello:
+ | ClientHello:
 	 --{*(7.4.1.2)
 	   PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.
 	   NA is CLIENT RANDOM, while SID is @{text SESSION_ID}.
            UNIX TIME is omitted because the protocol doesn't use it.

            28 bytes while MASTER SECRET is 48 bytes*}
          "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  \<in>  tls"
 
-   ServerHello:
+ | ServerHello:
          --{*7.4.1.3 of the TLS Internet-Draft
 	   PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}.
            SERVER CERTIFICATE (7.4.2) is always present.
            @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*}
          "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
              Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       \<in> set evsSH |]
           ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  \<in>  tls"
 
-   Certificate:
+ | Certificate:
          --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*}
          "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC  \<in>  tls"
 
-   ClientKeyExch:
+ | ClientKeyExch:
          --{*CLIENT KEY EXCHANGE (7.4.7).
            The client, A, chooses PMS, the PREMASTER SECRET.
            She encrypts PMS using the supplied KB, which ought to be pubK B.
            We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS
            and another MASTER SECRET is highly unlikely (even though

              Says B' A (certificate B KB) \<in> set evsCX |]
           ==> Says A B (Crypt KB (Nonce PMS))
 	      # Notes A {|Agent B, Nonce PMS|}
 	      # evsCX  \<in>  tls"
 
-   CertVerify:
+ | CertVerify:
 	--{*The optional Certificate Verify (7.4.8) message contains the
           specific components listed in the security analysis, F.1.1.2.
           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*}

 
 	--{*Finally come the FINISHED messages (7.4.8), confirming PA and PB
           among other things.  The master-secret is PRF(PMS,NA,NB).
           Either party may send its message first.*}
 
-   ClientFinished:
+ | ClientFinished:
         --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
           rule's applying when the Spy has satisfied the "Says A B" by
           repaying messages sent by the true client; in that case, the
           Spy does not know PMS and could not send ClientFinished.  One
           could simply put @{term "A\<noteq>Spy"} into the rule, but one should not

 			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A,
 			       Nonce NB, Number PB, Agent B|}))
               # evsCF  \<in>  tls"
 
-   ServerFinished:
+ | ServerFinished:
 	--{*Keeping A' and A'' distinct means B cannot even check that the
           two messages originate from the same source. *}
          "[| evsSF \<in> tls;
 	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
 	       \<in> set evsSF;

 			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A,
 			       Nonce NB, Number PB, Agent B|}))
               # evsSF  \<in>  tls"
 
-   ClientAccepts:
+ | ClientAccepts:
 	--{*Having transmitted ClientFinished and received an identical
           message encrypted with serverK, the client stores the parameters
           needed to resume this session.  The "Notes A ..." premise is
           used to prove @{text Notes_master_imp_Crypt_PMS}.*}
          "[| evsCA \<in> tls;

              Says A  B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA;
              Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |]
           ==>
              Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  \<in>  tls"
 
-   ServerAccepts:
+ | ServerAccepts:
 	--{*Having transmitted ServerFinished and received an identical
           message encrypted with clientK, the server stores the parameters
           needed to resume this session.  The "Says A'' B ..." premise is
           used to prove @{text Notes_master_imp_Crypt_PMS}.*}
          "[| evsSA \<in> tls;

              Says B  A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA;
              Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |]
           ==>
              Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
 
-   ClientResume:
+ | ClientResume:
          --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED
              message using the new nonces and stored MASTER SECRET.*}
          "[| evsCR \<in> tls;
 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
              Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;

 			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A,
 			       Nonce NB, Number PB, Agent B|}))
               # evsCR  \<in>  tls"
 
-   ServerResume:
+ | ServerResume:
          --{*Resumption (7.3):  If B finds the @{text SESSION_ID} then he can 
              send a FINISHED message using the recovered MASTER SECRET*}
          "[| evsSR \<in> tls;
 	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
 	     Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;

 			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A,
 			       Nonce NB, Number PB, Agent B|})) # evsSR
 	        \<in>  tls"
 
-   Oops:
+ | Oops:
          --{*The most plausible compromise is of an old session key.  Losing
            the MASTER SECRET or PREMASTER SECRET is more serious but
            rather unlikely.  The assumption @{term "A\<noteq>Spy"} is essential: 
            otherwise the Spy could learn session keys merely by 
            replaying messages!*}