src/HOL/Auth/TLS.thy
changeset 13922 75ae4244a596
parent 13507 febb8e5d2a9d
child 13956 8fe7e12290e1
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Apr 23 18:09:48 2003 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Apr 25 11:18:14 2003 +0200
     1.3 @@ -43,7 +43,11 @@
     1.4  
     1.5  constdefs
     1.6    certificate      :: "[agent,key] => msg"
     1.7 -    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
     1.8 +    "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
     1.9 +
    1.10 +text{*TLS apparently does not require separate keypairs for encryption and
    1.11 +signature.  Therefore, we formalize signature as encryption using the
    1.12 +private encryption key.*}
    1.13  
    1.14  datatype role = ClientRole | ServerRole
    1.15  
    1.16 @@ -66,67 +70,72 @@
    1.17    "serverK X" == "sessionK(X, ServerRole)"
    1.18  
    1.19  axioms
    1.20 -  (*the pseudo-random function is collision-free*)
    1.21 +  --{*the pseudo-random function is collision-free*}
    1.22    inj_PRF:       "inj PRF"
    1.23  
    1.24 -  (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
    1.25 +  --{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
    1.26    inj_sessionK:  "inj sessionK"	
    1.27  
    1.28 -  (*sessionK makes symmetric keys*)
    1.29 +  --{*sessionK makes symmetric keys*}
    1.30    isSym_sessionK: "sessionK nonces \<in> symKeys"
    1.31  
    1.32 +  --{*sessionK never clashes with a long-term symmetric key  
    1.33 +     (they don't exist in TLS anyway)*}
    1.34 +  sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A"
    1.35 +
    1.36  
    1.37  consts    tls :: "event list set"
    1.38  inductive tls
    1.39    intros
    1.40 -   Nil:  (*Initial trace is empty*)
    1.41 +   Nil:  --{*The initial, empty trace*}
    1.42           "[] \<in> tls"
    1.43  
    1.44 -   Fake: (*The spy, an active attacker, MAY say anything he CAN say.*)
    1.45 +   Fake: --{*The Spy may say anything he can say.  The sender field is correct,
    1.46 +          but agents don't use that information.*}
    1.47           "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
    1.48            ==> Says Spy B X # evsf \<in> tls"
    1.49  
    1.50 -   SpyKeys: (*The spy may apply PRF & sessionK to available nonces*)
    1.51 +   SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
    1.52           "[| evsSK \<in> tls;
    1.53  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
    1.54            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    1.55  			   Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
    1.56  
    1.57     ClientHello:
    1.58 -	 (*(7.4.1.2)
    1.59 +	 --{*(7.4.1.2)
    1.60  	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    1.61  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.62  	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    1.63             UNIX TIME is omitted because the protocol doesn't use it.
    1.64             May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
    1.65 -	   while MASTER SECRET is 48 bytes*)
    1.66 +	   while MASTER SECRET is 48 bytes*}
    1.67           "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
    1.68            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.69  	        # evsCH  \<in>  tls"
    1.70  
    1.71     ServerHello:
    1.72 -         (*7.4.1.3 of the TLS Internet-Draft
    1.73 +         --{*7.4.1.3 of the TLS Internet-Draft
    1.74  	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.75             SERVER CERTIFICATE (7.4.2) is always present.
    1.76 -           CERTIFICATE_REQUEST (7.4.4) is implied.*)
    1.77 +           CERTIFICATE_REQUEST (7.4.4) is implied.*}
    1.78           "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
    1.79               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.80  	       \<in> set evsSH |]
    1.81            ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  \<in>  tls"
    1.82  
    1.83     Certificate:
    1.84 -         (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    1.85 +         --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*}
    1.86           "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC  \<in>  tls"
    1.87  
    1.88     ClientKeyExch:
    1.89 -         (*CLIENT KEY EXCHANGE (7.4.7).
    1.90 +         --{*CLIENT KEY EXCHANGE (7.4.7).
    1.91             The client, A, chooses PMS, the PREMASTER SECRET.
    1.92             She encrypts PMS using the supplied KB, which ought to be pubK B.
    1.93             We assume PMS \<notin> range PRF because a clash betweem the PMS
    1.94             and another MASTER SECRET is highly unlikely (even though
    1.95  	   both items have the same length, 48 bytes).
    1.96             The Note event records in the trace that she knows PMS
    1.97 -               (see REMARK at top). *)
    1.98 +               (see REMARK at top). *}
    1.99           "[| evsCX \<in> tls;  Nonce PMS \<notin> used evsCX;  PMS \<notin> range PRF;
   1.100               Says B' A (certificate B KB) \<in> set evsCX |]
   1.101            ==> Says A B (Crypt KB (Nonce PMS))
   1.102 @@ -134,28 +143,28 @@
   1.103  	      # evsCX  \<in>  tls"
   1.104  
   1.105     CertVerify:
   1.106 -	(*The optional Certificate Verify (7.4.8) message contains the
   1.107 +	--{*The optional Certificate Verify (7.4.8) message contains the
   1.108            specific components listed in the security analysis, F.1.1.2.
   1.109            It adds the pre-master-secret, which is also essential!
   1.110            Checking the signature, which is the only use of A's certificate,
   1.111 -          assures B of A's presence*)
   1.112 +          assures B of A's presence*}
   1.113           "[| evsCV \<in> tls;
   1.114               Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV;
   1.115  	     Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |]
   1.116            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
   1.117                # evsCV  \<in>  tls"
   1.118  
   1.119 -	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
   1.120 +	--{*Finally come the FINISHED messages (7.4.8), confirming PA and PB
   1.121            among other things.  The master-secret is PRF(PMS,NA,NB).
   1.122 -          Either party may send its message first.*)
   1.123 +          Either party may send its message first.*}
   1.124  
   1.125     ClientFinished:
   1.126 -        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
   1.127 +        --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
   1.128            rule's applying when the Spy has satisfied the "Says A B" by
   1.129            repaying messages sent by the true client; in that case, the
   1.130            Spy does not know PMS and could not send ClientFinished.  One
   1.131            could simply put A\<noteq>Spy into the rule, but one should not
   1.132 -          expect the spy to be well-behaved.*)
   1.133 +          expect the spy to be well-behaved.*}
   1.134           "[| evsCF \<in> tls;
   1.135  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.136  	       \<in> set evsCF;
   1.137 @@ -169,8 +178,8 @@
   1.138                # evsCF  \<in>  tls"
   1.139  
   1.140     ServerFinished:
   1.141 -	(*Keeping A' and A'' distinct means B cannot even check that the
   1.142 -          two messages originate from the same source. *)
   1.143 +	--{*Keeping A' and A'' distinct means B cannot even check that the
   1.144 +          two messages originate from the same source. *}
   1.145           "[| evsSF \<in> tls;
   1.146  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
   1.147  	       \<in> set evsSF;
   1.148 @@ -184,10 +193,10 @@
   1.149                # evsSF  \<in>  tls"
   1.150  
   1.151     ClientAccepts:
   1.152 -	(*Having transmitted ClientFinished and received an identical
   1.153 +	--{*Having transmitted ClientFinished and received an identical
   1.154            message encrypted with serverK, the client stores the parameters
   1.155            needed to resume this session.  The "Notes A ..." premise is
   1.156 -          used to prove Notes_master_imp_Crypt_PMS.*)
   1.157 +          used to prove Notes_master_imp_Crypt_PMS.*}
   1.158           "[| evsCA \<in> tls;
   1.159  	     Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
   1.160  	     M = PRF(PMS,NA,NB);
   1.161 @@ -200,10 +209,10 @@
   1.162               Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  \<in>  tls"
   1.163  
   1.164     ServerAccepts:
   1.165 -	(*Having transmitted ServerFinished and received an identical
   1.166 +	--{*Having transmitted ServerFinished and received an identical
   1.167            message encrypted with clientK, the server stores the parameters
   1.168            needed to resume this session.  The "Says A'' B ..." premise is
   1.169 -          used to prove Notes_master_imp_Crypt_PMS.*)
   1.170 +          used to prove Notes_master_imp_Crypt_PMS.*}
   1.171           "[| evsSA \<in> tls;
   1.172  	     A \<noteq> B;
   1.173               Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
   1.174 @@ -217,8 +226,8 @@
   1.175               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
   1.176  
   1.177     ClientResume:
   1.178 -         (*If A recalls the SESSION_ID, then she sends a FINISHED message
   1.179 -           using the new nonces and stored MASTER SECRET.*)
   1.180 +         --{*If A recalls the SESSION_ID, then she sends a FINISHED message
   1.181 +           using the new nonces and stored MASTER SECRET.*}
   1.182           "[| evsCR \<in> tls;
   1.183  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
   1.184               Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
   1.185 @@ -230,8 +239,8 @@
   1.186                # evsCR  \<in>  tls"
   1.187  
   1.188     ServerResume:
   1.189 -         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
   1.190 -           a FINISHED message using the recovered MASTER SECRET*)
   1.191 +         --{*Resumption (7.3):  If B finds the SESSION_ID then he can send
   1.192 +           a FINISHED message using the recovered MASTER SECRET*}
   1.193           "[| evsSR \<in> tls;
   1.194  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
   1.195  	     Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
   1.196 @@ -243,10 +252,10 @@
   1.197  	        \<in>  tls"
   1.198  
   1.199     Oops:
   1.200 -         (*The most plausible compromise is of an old session key.  Losing
   1.201 +         --{*The most plausible compromise is of an old session key.  Losing
   1.202             the MASTER SECRET or PREMASTER SECRET is more serious but
   1.203             rather unlikely.  The assumption A \<noteq> Spy is essential: otherwise
   1.204 -           the Spy could learn session keys merely by replaying messages!*)
   1.205 +           the Spy could learn session keys merely by replaying messages!*}
   1.206           "[| evso \<in> tls;  A \<noteq> Spy;
   1.207  	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
   1.208            ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
   1.209 @@ -272,10 +281,10 @@
   1.210  declare Fake_parts_insert_in_Un  [dest]
   1.211  
   1.212  
   1.213 -(*Automatically unfold the definition of "certificate"*)
   1.214 +text{*Automatically unfold the definition of "certificate"*}
   1.215  declare certificate_def [simp]
   1.216  
   1.217 -(*Injectiveness of key-generating functions*)
   1.218 +text{*Injectiveness of key-generating functions*}
   1.219  declare inj_PRF [THEN inj_eq, iff]
   1.220  declare inj_sessionK [THEN inj_eq, iff]
   1.221  declare isSym_sessionK [simp]
   1.222 @@ -283,12 +292,12 @@
   1.223  
   1.224  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
   1.225  
   1.226 -lemma pubK_neq_sessionK [iff]: "pubK A \<noteq> sessionK arg"
   1.227 +lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg"
   1.228  by (simp add: symKeys_neq_imp_neq)
   1.229  
   1.230  declare pubK_neq_sessionK [THEN not_sym, iff]
   1.231  
   1.232 -lemma priK_neq_sessionK [iff]: "priK A \<noteq> sessionK arg"
   1.233 +lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg"
   1.234  by (simp add: symKeys_neq_imp_neq)
   1.235  
   1.236  declare priK_neq_sessionK [THEN not_sym, iff]
   1.237 @@ -296,10 +305,10 @@
   1.238  lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK
   1.239  
   1.240  
   1.241 -(**** Protocol Proofs ****)
   1.242 +subsection{*Protocol Proofs*}
   1.243  
   1.244 -(*Possibility properties state that some traces run the protocol to the end.
   1.245 -  Four paths and 12 rules are considered.*)
   1.246 +text{*Possibility properties state that some traces run the protocol to the
   1.247 +end.  Four paths and 12 rules are considered.*}
   1.248  
   1.249  
   1.250  (** These proofs assume that the Nonce_supply nonces
   1.251 @@ -309,7 +318,7 @@
   1.252  **)
   1.253  
   1.254  
   1.255 -(*Possibility property ending with ClientAccepts.*)
   1.256 +text{*Possibility property ending with ClientAccepts.*}
   1.257  lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
   1.258        ==> \<exists>SID M. \<exists>evs \<in> tls.
   1.259              Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
   1.260 @@ -322,7 +331,7 @@
   1.261  done
   1.262  
   1.263  
   1.264 -(*And one for ServerAccepts.  Either FINISHED message may come first.*)
   1.265 +text{*And one for ServerAccepts.  Either FINISHED message may come first.*}
   1.266  lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
   1.267        ==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
   1.268             Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
   1.269 @@ -335,7 +344,7 @@
   1.270  done
   1.271  
   1.272  
   1.273 -(*Another one, for CertVerify (which is optional)*)
   1.274 +text{*Another one, for CertVerify (which is optional)*}
   1.275  lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
   1.276         ==> \<exists>NB PMS. \<exists>evs \<in> tls.
   1.277                Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) 
   1.278 @@ -348,8 +357,8 @@
   1.279  done
   1.280  
   1.281  
   1.282 -(*Another one, for session resumption (both ServerResume and ClientResume).
   1.283 -  NO tls.Nil here: we refer to a previous session, not the empty trace.*)
   1.284 +text{*Another one, for session resumption (both ServerResume and ClientResume).
   1.285 +  NO tls.Nil here: we refer to a previous session, not the empty trace.*}
   1.286  lemma "[| evs0 \<in> tls;
   1.287            Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
   1.288            Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
   1.289 @@ -368,41 +377,30 @@
   1.290  done
   1.291  
   1.292  
   1.293 -(**** Inductive proofs about tls ****)
   1.294 -
   1.295 +subsection{*Inductive proofs about tls*}
   1.296  
   1.297 -(*Induction for regularity theorems.  If induction formula has the form
   1.298 -   X \<notin> analz (spies evs) --> ... then it shortens the proof by discarding
   1.299 -   needless information about analz (insert X (spies evs))  
   1.300 -fun parts_induct_tac i =
   1.301 -    etac tls.induct i
   1.302 -    THEN REPEAT (FIRSTGOAL analz_mono_contra_tac)
   1.303 -    THEN Force_tac i THEN
   1.304 -    ALLGOALS Asm_simp_tac
   1.305 -*)
   1.306  
   1.307  (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   1.308      sends messages containing X! **)
   1.309  
   1.310 -(*Spy never sees a good agent's private key!*)
   1.311 +text{*Spy never sees a good agent's private key!*}
   1.312  lemma Spy_see_priK [simp]:
   1.313 -     "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   1.314 -apply (erule tls.induct, force, simp_all, blast)
   1.315 -done
   1.316 +     "evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
   1.317 +by (erule tls.induct, force, simp_all, blast)
   1.318  
   1.319  lemma Spy_analz_priK [simp]:
   1.320 -     "evs \<in> tls ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   1.321 +     "evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)"
   1.322  by auto
   1.323  
   1.324  lemma Spy_see_priK_D [dest!]:
   1.325 -     "[|Key (priK A) \<in> parts (knows Spy evs);  evs \<in> tls|] ==> A \<in> bad"
   1.326 +    "[|Key (privateKey b A) \<in> parts (knows Spy evs);  evs \<in> tls|] ==> A \<in> bad"
   1.327  by (blast dest: Spy_see_priK)
   1.328  
   1.329  
   1.330 -(*This lemma says that no false certificates exist.  One might extend the
   1.331 +text{*This lemma says that no false certificates exist.  One might extend the
   1.332    model to include bogus certificates for the agents, but there seems
   1.333    little point in doing so: the loss of their private keys is a worse
   1.334 -  breach of security.*)
   1.335 +  breach of security.*}
   1.336  lemma certificate_valid:
   1.337      "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
   1.338  apply (erule rev_mp)
   1.339 @@ -412,7 +410,7 @@
   1.340  lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
   1.341  
   1.342  
   1.343 -(*** Properties of items found in Notes ***)
   1.344 +subsubsection{*Properties of items found in Notes*}
   1.345  
   1.346  lemma Notes_Crypt_parts_spies:
   1.347       "[| Notes A {|Agent B, X|} \<in> set evs;  evs \<in> tls |]
   1.348 @@ -423,34 +421,34 @@
   1.349  apply (blast intro: parts_insertI)
   1.350  done
   1.351  
   1.352 -(*C may be either A or B*)
   1.353 +text{*C may be either A or B*}
   1.354  lemma Notes_master_imp_Crypt_PMS:
   1.355       "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
   1.356           evs \<in> tls |]
   1.357        ==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
   1.358  apply (erule rev_mp)
   1.359  apply (erule tls.induct, force, simp_all)
   1.360 -(*Fake*)
   1.361 +txt{*Fake*}
   1.362  apply (blast intro: parts_insertI)
   1.363 -(*Client, Server Accept*)
   1.364 +txt{*Client, Server Accept*}
   1.365  apply (blast dest!: Notes_Crypt_parts_spies)+
   1.366  done
   1.367  
   1.368 -(*Compared with the theorem above, both premise and conclusion are stronger*)
   1.369 +text{*Compared with the theorem above, both premise and conclusion are stronger*}
   1.370  lemma Notes_master_imp_Notes_PMS:
   1.371       "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
   1.372           evs \<in> tls |]
   1.373        ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
   1.374  apply (erule rev_mp)
   1.375  apply (erule tls.induct, force, simp_all)
   1.376 -(*ServerAccepts*)
   1.377 +txt{*ServerAccepts*}
   1.378  apply blast
   1.379  done
   1.380  
   1.381  
   1.382 -(*** Protocol goal: if B receives CertVerify, then A sent it ***)
   1.383 +subsubsection{*Protocol goal: if B receives CertVerify, then A sent it*}
   1.384  
   1.385 -(*B can check A's signature if he has received A's certificate.*)
   1.386 +text{*B can check A's signature if he has received A's certificate.*}
   1.387  lemma TrustCertVerify_lemma:
   1.388       "[| X \<in> parts (spies evs);
   1.389           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
   1.390 @@ -460,7 +458,7 @@
   1.391  apply (erule tls.induct, force, simp_all, blast)
   1.392  done
   1.393  
   1.394 -(*Final version: B checks X using the distributed KA instead of priK A*)
   1.395 +text{*Final version: B checks X using the distributed KA instead of priK A*}
   1.396  lemma TrustCertVerify:
   1.397       "[| X \<in> parts (spies evs);
   1.398           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
   1.399 @@ -470,7 +468,7 @@
   1.400  by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)
   1.401  
   1.402  
   1.403 -(*If CertVerify is present then A has chosen PMS.*)
   1.404 +text{*If CertVerify is present then A has chosen PMS.*}
   1.405  lemma UseCertVerify_lemma:
   1.406       "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
   1.407           evs \<in> tls;  A \<notin> bad |]
   1.408 @@ -479,7 +477,7 @@
   1.409  apply (erule tls.induct, force, simp_all, blast)
   1.410  done
   1.411  
   1.412 -(*Final version using the distributed KA instead of priK A*)
   1.413 +text{*Final version using the distributed KA instead of priK A*}
   1.414  lemma UseCertVerify:
   1.415       "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
   1.416             \<in> parts (spies evs);
   1.417 @@ -492,7 +490,7 @@
   1.418  lemma no_Notes_A_PRF [simp]:
   1.419       "evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
   1.420  apply (erule tls.induct, force, simp_all)
   1.421 -(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   1.422 +txt{*ClientKeyExch: PMS is assumed to differ from any PRF.*}
   1.423  apply blast
   1.424  done
   1.425  
   1.426 @@ -502,18 +500,18 @@
   1.427        ==> Nonce PMS \<in> parts (spies evs)"
   1.428  apply (erule rev_mp)
   1.429  apply (erule tls.induct, force, simp_all)
   1.430 -(*Fake*)
   1.431 +txt{*Fake*}
   1.432  apply (blast intro: parts_insertI)
   1.433 -(*Easy, e.g. by freshness*)
   1.434 +txt{*Easy, e.g. by freshness*}
   1.435  apply (blast dest: Notes_Crypt_parts_spies)+
   1.436  done
   1.437  
   1.438  
   1.439  
   1.440  
   1.441 -(*** Unicity results for PMS, the pre-master-secret ***)
   1.442 +subsubsection{*Unicity results for PMS, the pre-master-secret*}
   1.443  
   1.444 -(*PMS determines B.*)
   1.445 +text{*PMS determines B.*}
   1.446  lemma Crypt_unique_PMS:
   1.447       "[| Crypt(pubK B)  (Nonce PMS) \<in> parts (spies evs);
   1.448           Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs);
   1.449 @@ -522,7 +520,7 @@
   1.450        ==> B=B'"
   1.451  apply (erule rev_mp, erule rev_mp, erule rev_mp)
   1.452  apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
   1.453 -(*Fake, ClientKeyExch*)
   1.454 +txt{*Fake, ClientKeyExch*}
   1.455  apply blast+
   1.456  done
   1.457  
   1.458 @@ -533,7 +531,7 @@
   1.459      determines B alone, and only if PMS is secret.
   1.460  **)
   1.461  
   1.462 -(*In A's internal Note, PMS determines A and B.*)
   1.463 +text{*In A's internal Note, PMS determines A and B.*}
   1.464  lemma Notes_unique_PMS:
   1.465       "[| Notes A  {|Agent B,  Nonce PMS|} \<in> set evs;
   1.466           Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
   1.467 @@ -541,15 +539,15 @@
   1.468        ==> A=A' & B=B'"
   1.469  apply (erule rev_mp, erule rev_mp)
   1.470  apply (erule tls.induct, force, simp_all)
   1.471 -(*ClientKeyExch*)
   1.472 +txt{*ClientKeyExch*}
   1.473  apply (blast dest!: Notes_Crypt_parts_spies)
   1.474  done
   1.475  
   1.476  
   1.477 -(**** Secrecy Theorems ****)
   1.478 +subsection{*Secrecy Theorems*}
   1.479  
   1.480 -(*Key compromise lemma needed to prove analz_image_keys.
   1.481 -  No collection of keys can help the spy get new private keys.*)
   1.482 +text{*Key compromise lemma needed to prove analz_image_keys.
   1.483 +  No collection of keys can help the spy get new private keys.*}
   1.484  lemma analz_image_priK [rule_format]:
   1.485       "evs \<in> tls
   1.486        ==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) =
   1.487 @@ -559,18 +557,18 @@
   1.488  		del: image_insert
   1.489                  add: image_Un [THEN sym]
   1.490                       insert_Key_image Un_assoc [THEN sym])
   1.491 -(*Fake*)
   1.492 +txt{*Fake*}
   1.493  apply spy_analz
   1.494  done
   1.495  
   1.496  
   1.497 -(*slightly speeds up the big simplification below*)
   1.498 +text{*slightly speeds up the big simplification below*}
   1.499  lemma range_sessionkeys_not_priK:
   1.500       "KK <= range sessionK ==> priK B \<notin> KK"
   1.501  by blast
   1.502  
   1.503  
   1.504 -(*Lemma for the trivial direction of the if-and-only-if*)
   1.505 +text{*Lemma for the trivial direction of the if-and-only-if*}
   1.506  lemma analz_image_keys_lemma:
   1.507       "(X \<in> analz (G Un H)) --> (X \<in> analz H)  ==>
   1.508        (X \<in> analz (G Un H))  =  (X \<in> analz H)"
   1.509 @@ -595,11 +593,11 @@
   1.510  		     insert_Key_singleton
   1.511  		     range_sessionkeys_not_priK analz_image_priK)
   1.512  apply (simp_all add: insert_absorb)
   1.513 -(*Fake*)
   1.514 +txt{*Fake*}
   1.515  apply spy_analz
   1.516  done
   1.517  
   1.518 -(*Knowing some session keys is no help in getting new nonces*)
   1.519 +text{*Knowing some session keys is no help in getting new nonces*}
   1.520  lemma analz_insert_key [simp]:
   1.521       "evs \<in> tls ==>
   1.522        (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
   1.523 @@ -608,28 +606,28 @@
   1.524           add: insert_Key_singleton analz_image_keys)
   1.525  
   1.526  
   1.527 -(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   1.528 +subsubsection{*Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure*}
   1.529  
   1.530  (** Some lemmas about session keys, comprising clientK and serverK **)
   1.531  
   1.532  
   1.533 -(*Lemma: session keys are never used if PMS is fresh.
   1.534 +text{*Lemma: session keys are never used if PMS is fresh.
   1.535    Nonces don't have to agree, allowing session resumption.
   1.536    Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.537 -  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   1.538 +  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*}
   1.539  lemma PMS_lemma:
   1.540       "[| Nonce PMS \<notin> parts (spies evs);
   1.541           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
   1.542           evs \<in> tls |]
   1.543     ==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
   1.544  apply (erule rev_mp, erule ssubst)
   1.545 -apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.546 +apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 
   1.547  apply (force, simp_all (no_asm_simp))
   1.548 -(*Fake*)
   1.549 +txt{*Fake*}
   1.550  apply (blast intro: parts_insertI)
   1.551 -(*SpyKeys*)
   1.552 +txt{*SpyKeys*}
   1.553  apply blast
   1.554 -(*Many others*)
   1.555 +txt{*Many others*}
   1.556  apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+
   1.557  done
   1.558  
   1.559 @@ -645,11 +643,11 @@
   1.560        ==> Nonce PMS \<in> parts (spies evs)"
   1.561  by (blast dest: PMS_lemma)
   1.562  
   1.563 -(*Write keys are never sent if M (MASTER SECRET) is secure.
   1.564 +text{*Write keys are never sent if M (MASTER SECRET) is secure.
   1.565    Converse fails; betraying M doesn't force the keys to be sent!
   1.566    The strong Oops condition can be weakened later by unicity reasoning,
   1.567    with some effort.
   1.568 -  NO LONGER USED: see clientK_not_spied and serverK_not_spied*)
   1.569 +  NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
   1.570  lemma sessionK_not_spied:
   1.571       "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
   1.572           Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
   1.573 @@ -657,57 +655,57 @@
   1.574  apply (erule rev_mp, erule rev_mp)
   1.575  apply (erule tls.induct, analz_mono_contra)
   1.576  apply (force, simp_all (no_asm_simp))
   1.577 -(*Fake, SpyKeys*)
   1.578 +txt{*Fake, SpyKeys*}
   1.579  apply blast+
   1.580  done
   1.581  
   1.582  
   1.583 -(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   1.584 +text{*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*}
   1.585  lemma Spy_not_see_PMS:
   1.586       "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.587           evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   1.588        ==> Nonce PMS \<notin> analz (spies evs)"
   1.589  apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.590  apply (force, simp_all (no_asm_simp))
   1.591 -(*Fake*)
   1.592 +txt{*Fake*}
   1.593  apply spy_analz
   1.594 -(*SpyKeys*)
   1.595 +txt{*SpyKeys*}
   1.596  apply force
   1.597  apply (simp_all add: insert_absorb) 
   1.598 -(*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*)
   1.599 +txt{*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*}
   1.600  apply (blast dest: Notes_Crypt_parts_spies)
   1.601  apply (blast dest: Notes_Crypt_parts_spies)
   1.602  apply (blast dest: Notes_Crypt_parts_spies)
   1.603 -(*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*)
   1.604 +txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
   1.605  apply force+
   1.606  done
   1.607  
   1.608  
   1.609 -(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   1.610 -  will stay secret.*)
   1.611 +text{*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   1.612 +  will stay secret.*}
   1.613  lemma Spy_not_see_MS:
   1.614       "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.615           evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   1.616        ==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
   1.617  apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.618  apply (force, simp_all (no_asm_simp))
   1.619 -(*Fake*)
   1.620 +txt{*Fake*}
   1.621  apply spy_analz
   1.622 -(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   1.623 +txt{*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*}
   1.624  apply (blast dest!: Spy_not_see_PMS)
   1.625  apply (simp_all add: insert_absorb)
   1.626 -(*ClientAccepts and ServerAccepts: because PMS was already visible;
   1.627 -  others, freshness etc.*)
   1.628 +txt{*ClientAccepts and ServerAccepts: because PMS was already visible;
   1.629 +  others, freshness etc.*}
   1.630  apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS 
   1.631                     Notes_imp_knows_Spy [THEN analz.Inj])+
   1.632  done
   1.633  
   1.634  
   1.635  
   1.636 -(*** Weakening the Oops conditions for leakage of clientK ***)
   1.637 +subsubsection{*Weakening the Oops conditions for leakage of clientK*}
   1.638  
   1.639 -(*If A created PMS then nobody else (except the Spy in replays)
   1.640 -  would send a message using a clientK generated from that PMS.*)
   1.641 +text{*If A created PMS then nobody else (except the Spy in replays)
   1.642 +  would send a message using a clientK generated from that PMS.*}
   1.643  lemma Says_clientK_unique:
   1.644       "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
   1.645           Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.646 @@ -716,16 +714,16 @@
   1.647  apply (erule rev_mp, erule rev_mp)
   1.648  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.649  apply (force, simp_all)
   1.650 -(*ClientKeyExch*)
   1.651 +txt{*ClientKeyExch*}
   1.652  apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   1.653 -(*ClientFinished, ClientResume: by unicity of PMS*)
   1.654 +txt{*ClientFinished, ClientResume: by unicity of PMS*}
   1.655  apply (blast dest!: Notes_master_imp_Notes_PMS 
   1.656               intro: Notes_unique_PMS [THEN conjunct1])+
   1.657  done
   1.658  
   1.659  
   1.660 -(*If A created PMS and has not leaked her clientK to the Spy,
   1.661 -  then it is completely secure: not even in parts!*)
   1.662 +text{*If A created PMS and has not leaked her clientK to the Spy,
   1.663 +  then it is completely secure: not even in parts!*}
   1.664  lemma clientK_not_spied:
   1.665       "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.666           Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
   1.667 @@ -735,21 +733,21 @@
   1.668  apply (erule rev_mp, erule rev_mp)
   1.669  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.670  apply (force, simp_all (no_asm_simp))
   1.671 -(*ClientKeyExch*)
   1.672 +txt{*ClientKeyExch*}
   1.673  apply blast 
   1.674 -(*SpyKeys*)
   1.675 +txt{*SpyKeys*}
   1.676  apply (blast dest!: Spy_not_see_MS)
   1.677 -(*ClientKeyExch*)
   1.678 +txt{*ClientKeyExch*}
   1.679  apply (blast dest!: PMS_sessionK_not_spied)
   1.680 -(*Oops*)
   1.681 +txt{*Oops*}
   1.682  apply (blast intro: Says_clientK_unique)
   1.683  done
   1.684  
   1.685  
   1.686 -(*** Weakening the Oops conditions for leakage of serverK ***)
   1.687 +subsubsection{*Weakening the Oops conditions for leakage of serverK*}
   1.688  
   1.689 -(*If A created PMS for B, then nobody other than B or the Spy would
   1.690 -  send a message using a serverK generated from that PMS.*)
   1.691 +text{*If A created PMS for B, then nobody other than B or the Spy would
   1.692 +  send a message using a serverK generated from that PMS.*}
   1.693  lemma Says_serverK_unique:
   1.694       "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
   1.695           Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.696 @@ -758,16 +756,16 @@
   1.697  apply (erule rev_mp, erule rev_mp)
   1.698  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.699  apply (force, simp_all)
   1.700 -(*ClientKeyExch*)
   1.701 +txt{*ClientKeyExch*}
   1.702  apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   1.703 -(*ServerResume, ServerFinished: by unicity of PMS*)
   1.704 +txt{*ServerResume, ServerFinished: by unicity of PMS*}
   1.705  apply (blast dest!: Notes_master_imp_Crypt_PMS 
   1.706               dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
   1.707  done
   1.708  
   1.709  
   1.710 -(*If A created PMS for B, and B has not leaked his serverK to the Spy,
   1.711 -  then it is completely secure: not even in parts!*)
   1.712 +text{*If A created PMS for B, and B has not leaked his serverK to the Spy,
   1.713 +  then it is completely secure: not even in parts!*}
   1.714  lemma serverK_not_spied:
   1.715       "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   1.716           Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
   1.717 @@ -776,23 +774,23 @@
   1.718  apply (erule rev_mp, erule rev_mp)
   1.719  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.720  apply (force, simp_all (no_asm_simp))
   1.721 -(*Fake*)
   1.722 +txt{*Fake*}
   1.723  apply blast 
   1.724 -(*SpyKeys*)
   1.725 +txt{*SpyKeys*}
   1.726  apply (blast dest!: Spy_not_see_MS)
   1.727 -(*ClientKeyExch*)
   1.728 +txt{*ClientKeyExch*}
   1.729  apply (blast dest!: PMS_sessionK_not_spied)
   1.730 -(*Oops*)
   1.731 +txt{*Oops*}
   1.732  apply (blast intro: Says_serverK_unique)
   1.733  done
   1.734  
   1.735  
   1.736 -(*** Protocol goals: if A receives ServerFinished, then B is present
   1.737 +subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
   1.738       and has used the quoted values PA, PB, etc.  Note that it is up to A
   1.739       to compare PA with what she originally sent.
   1.740  ***)
   1.741  
   1.742 -(*The mention of her name (A) in X assures A that B knows who she is.*)
   1.743 +text{*The mention of her name (A) in X assures A that B knows who she is.*}
   1.744  lemma TrustServerFinished [rule_format]:
   1.745       "[| X = Crypt (serverK(Na,Nb,M))
   1.746                 (Hash{|Number SID, Nonce M,
   1.747 @@ -806,17 +804,17 @@
   1.748  apply (erule ssubst)+
   1.749  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.750  apply (force, simp_all (no_asm_simp))
   1.751 -(*Fake: the Spy doesn't have the critical session key!*)
   1.752 +txt{*Fake: the Spy doesn't have the critical session key!*}
   1.753  apply (blast dest: serverK_not_spied)
   1.754 -(*ClientKeyExch*)
   1.755 +txt{*ClientKeyExch*}
   1.756  apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   1.757  done
   1.758  
   1.759 -(*This version refers not to ServerFinished but to any message from B.
   1.760 +text{*This version refers not to ServerFinished but to any message from B.
   1.761    We don't assume B has received CertVerify, and an intruder could
   1.762    have changed A's identity in all other messages, so we can't be sure
   1.763    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.764 -  to bind A's identity with PMS, then we could replace A' by A below.*)
   1.765 +  to bind A's identity with PMS, then we could replace A' by A below.*}
   1.766  lemma TrustServerMsg [rule_format]:
   1.767       "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   1.768        ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
   1.769 @@ -826,21 +824,22 @@
   1.770  apply (erule ssubst)
   1.771  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.772  apply (force, simp_all (no_asm_simp) add: ex_disj_distrib)
   1.773 -(*Fake: the Spy doesn't have the critical session key!*)
   1.774 +txt{*Fake: the Spy doesn't have the critical session key!*}
   1.775  apply (blast dest: serverK_not_spied)
   1.776 -(*ClientKeyExch*)
   1.777 +txt{*ClientKeyExch*}
   1.778  apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied)
   1.779 -(*ServerResume, ServerFinished: by unicity of PMS*)
   1.780 +txt{*ServerResume, ServerFinished: by unicity of PMS*}
   1.781  apply (blast dest!: Notes_master_imp_Crypt_PMS 
   1.782               dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
   1.783  done
   1.784  
   1.785  
   1.786 -(*** Protocol goal: if B receives any message encrypted with clientK
   1.787 -     then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.788 +subsubsection{*Protocol goal: if B receives any message encrypted with clientK
   1.789 +      then A has sent it*}
   1.790 +
   1.791 +text{*ASSUMING that A chose PMS.  Authentication is
   1.792       assumed here; B cannot verify it.  But if the message is
   1.793 -     ClientFinished, then B can then check the quoted values PA, PB, etc.
   1.794 -***)
   1.795 +     ClientFinished, then B can then check the quoted values PA, PB, etc.*}
   1.796  
   1.797  lemma TrustClientMsg [rule_format]:
   1.798       "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   1.799 @@ -851,19 +850,19 @@
   1.800  apply (erule ssubst)
   1.801  apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   1.802  apply (force, simp_all (no_asm_simp))
   1.803 -(*Fake: the Spy doesn't have the critical session key!*)
   1.804 +txt{*Fake: the Spy doesn't have the critical session key!*}
   1.805  apply (blast dest: clientK_not_spied)
   1.806 -(*ClientKeyExch*)
   1.807 +txt{*ClientKeyExch*}
   1.808  apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   1.809 -(*ClientFinished, ClientResume: by unicity of PMS*)
   1.810 +txt{*ClientFinished, ClientResume: by unicity of PMS*}
   1.811  apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+
   1.812  done
   1.813  
   1.814  
   1.815 -(*** Protocol goal: if B receives ClientFinished, and if B is able to
   1.816 +subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
   1.817       check a CertVerify from A, then A has used the quoted
   1.818       values PA, PB, etc.  Even this one requires A to be uncompromised.
   1.819 - ***)
   1.820 +*}
   1.821  lemma AuthClientFinished:
   1.822       "[| M = PRF(PMS,NA,NB);
   1.823           Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;