src/HOL/Auth/TLS.thy
changeset 13956 8fe7e12290e1
parent 13922 75ae4244a596
child 14126 28824746d046
     1.1 --- a/src/HOL/Auth/TLS.thy	Mon May 05 15:55:56 2003 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Mon May 05 18:22:01 2003 +0200
     1.3 @@ -39,6 +39,8 @@
     1.4  	Notes A {|Agent B, Nonce PMS|}.
     1.5  *)
     1.6  
     1.7 +header{*The TLS Protocol: Transport Layer Security*}
     1.8 +
     1.9  theory TLS = Public:
    1.10  
    1.11  constdefs
    1.12 @@ -95,7 +97,8 @@
    1.13           "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
    1.14            ==> Says Spy B X # evsf \<in> tls"
    1.15  
    1.16 -   SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
    1.17 +   SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK}
    1.18 +                to available nonces*}
    1.19           "[| evsSK \<in> tls;
    1.20  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
    1.21            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    1.22 @@ -103,21 +106,21 @@
    1.23  
    1.24     ClientHello:
    1.25  	 --{*(7.4.1.2)
    1.26 -	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    1.27 +	   PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}.
    1.28  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.29 -	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    1.30 +	   NA is CLIENT RANDOM, while SID is @{text SESSION_ID}.
    1.31             UNIX TIME is omitted because the protocol doesn't use it.
    1.32 -           May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
    1.33 -	   while MASTER SECRET is 48 bytes*}
    1.34 +           May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is 
    1.35 +           28 bytes while MASTER SECRET is 48 bytes*}
    1.36           "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
    1.37            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.38  	        # evsCH  \<in>  tls"
    1.39  
    1.40     ServerHello:
    1.41           --{*7.4.1.3 of the TLS Internet-Draft
    1.42 -	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.43 +	   PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}.
    1.44             SERVER CERTIFICATE (7.4.2) is always present.
    1.45 -           CERTIFICATE_REQUEST (7.4.4) is implied.*}
    1.46 +           @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*}
    1.47           "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
    1.48               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.49  	       \<in> set evsSH |]
    1.50 @@ -131,7 +134,7 @@
    1.51           --{*CLIENT KEY EXCHANGE (7.4.7).
    1.52             The client, A, chooses PMS, the PREMASTER SECRET.
    1.53             She encrypts PMS using the supplied KB, which ought to be pubK B.
    1.54 -           We assume PMS \<notin> range PRF because a clash betweem the PMS
    1.55 +           We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS
    1.56             and another MASTER SECRET is highly unlikely (even though
    1.57  	   both items have the same length, 48 bytes).
    1.58             The Note event records in the trace that she knows PMS
    1.59 @@ -163,7 +166,7 @@
    1.60            rule's applying when the Spy has satisfied the "Says A B" by
    1.61            repaying messages sent by the true client; in that case, the
    1.62            Spy does not know PMS and could not send ClientFinished.  One
    1.63 -          could simply put A\<noteq>Spy into the rule, but one should not
    1.64 +          could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
    1.65            expect the spy to be well-behaved.*}
    1.66           "[| evsCF \<in> tls;
    1.67  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.68 @@ -196,7 +199,7 @@
    1.69  	--{*Having transmitted ClientFinished and received an identical
    1.70            message encrypted with serverK, the client stores the parameters
    1.71            needed to resume this session.  The "Notes A ..." premise is
    1.72 -          used to prove Notes_master_imp_Crypt_PMS.*}
    1.73 +          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
    1.74           "[| evsCA \<in> tls;
    1.75  	     Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
    1.76  	     M = PRF(PMS,NA,NB);
    1.77 @@ -212,7 +215,7 @@
    1.78  	--{*Having transmitted ServerFinished and received an identical
    1.79            message encrypted with clientK, the server stores the parameters
    1.80            needed to resume this session.  The "Says A'' B ..." premise is
    1.81 -          used to prove Notes_master_imp_Crypt_PMS.*}
    1.82 +          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
    1.83           "[| evsSA \<in> tls;
    1.84  	     A \<noteq> B;
    1.85               Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
    1.86 @@ -226,8 +229,8 @@
    1.87               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
    1.88  
    1.89     ClientResume:
    1.90 -         --{*If A recalls the SESSION_ID, then she sends a FINISHED message
    1.91 -           using the new nonces and stored MASTER SECRET.*}
    1.92 +         --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED
    1.93 +             message using the new nonces and stored MASTER SECRET.*}
    1.94           "[| evsCR \<in> tls;
    1.95  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
    1.96               Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
    1.97 @@ -239,8 +242,8 @@
    1.98                # evsCR  \<in>  tls"
    1.99  
   1.100     ServerResume:
   1.101 -         --{*Resumption (7.3):  If B finds the SESSION_ID then he can send
   1.102 -           a FINISHED message using the recovered MASTER SECRET*}
   1.103 +         --{*Resumption (7.3):  If B finds the @{text SESSION_ID} then he can 
   1.104 +             send a FINISHED message using the recovered MASTER SECRET*}
   1.105           "[| evsSR \<in> tls;
   1.106  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
   1.107  	     Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
   1.108 @@ -254,8 +257,9 @@
   1.109     Oops:
   1.110           --{*The most plausible compromise is of an old session key.  Losing
   1.111             the MASTER SECRET or PREMASTER SECRET is more serious but
   1.112 -           rather unlikely.  The assumption A \<noteq> Spy is essential: otherwise
   1.113 -           the Spy could learn session keys merely by replaying messages!*}
   1.114 +           rather unlikely.  The assumption @{term "A\<noteq>Spy"} is essential: 
   1.115 +           otherwise the Spy could learn session keys merely by 
   1.116 +           replaying messages!*}
   1.117           "[| evso \<in> tls;  A \<noteq> Spy;
   1.118  	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
   1.119            ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
   1.120 @@ -546,7 +550,7 @@
   1.121  
   1.122  subsection{*Secrecy Theorems*}
   1.123  
   1.124 -text{*Key compromise lemma needed to prove analz_image_keys.
   1.125 +text{*Key compromise lemma needed to prove @{term analz_image_keys}.
   1.126    No collection of keys can help the spy get new private keys.*}
   1.127  lemma analz_image_priK [rule_format]:
   1.128       "evs \<in> tls
   1.129 @@ -647,7 +651,7 @@
   1.130    Converse fails; betraying M doesn't force the keys to be sent!
   1.131    The strong Oops condition can be weakened later by unicity reasoning,
   1.132    with some effort.
   1.133 -  NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
   1.134 +  NO LONGER USED: see @{text clientK_not_spied} and @{text serverK_not_spied}*}
   1.135  lemma sessionK_not_spied:
   1.136       "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
   1.137           Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
   1.138 @@ -676,7 +680,7 @@
   1.139  apply (blast dest: Notes_Crypt_parts_spies)
   1.140  apply (blast dest: Notes_Crypt_parts_spies)
   1.141  apply (blast dest: Notes_Crypt_parts_spies)
   1.142 -txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
   1.143 +txt{*ClientAccepts and ServerAccepts: because @{term "PMS \<notin> range PRF"}*}
   1.144  apply force+
   1.145  done
   1.146  
   1.147 @@ -787,8 +791,7 @@
   1.148  
   1.149  subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
   1.150       and has used the quoted values PA, PB, etc.  Note that it is up to A
   1.151 -     to compare PA with what she originally sent.
   1.152 -***)
   1.153 +     to compare PA with what she originally sent.*}
   1.154  
   1.155  text{*The mention of her name (A) in X assures A that B knows who she is.*}
   1.156  lemma TrustServerFinished [rule_format]:
   1.157 @@ -861,8 +864,7 @@
   1.158  
   1.159  subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
   1.160       check a CertVerify from A, then A has used the quoted
   1.161 -     values PA, PB, etc.  Even this one requires A to be uncompromised.
   1.162 -*}
   1.163 +     values PA, PB, etc.  Even this one requires A to be uncompromised.*}
   1.164  lemma AuthClientFinished:
   1.165       "[| M = PRF(PMS,NA,NB);
   1.166           Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;