src/HOL/Auth/TLS.thy
changeset 11185 1b737b4c2108
parent 6284 147db42c1009
child 11230 756c5034f08b
     1.1 --- a/src/HOL/Auth/TLS.thy	Tue Feb 27 12:28:42 2001 +0100
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Feb 27 16:13:23 2001 +0100
     1.3 @@ -82,14 +82,14 @@
     1.4           "[]: tls"
     1.5  
     1.6      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
     1.7 -         "[| evs: tls;  X: synth (analz (spies evs)) |]
     1.8 -          ==> Says Spy B X # evs : tls"
     1.9 +         "[| evsf \\<in> tls;  X \\<in> synth (analz (spies evsf)) |]
    1.10 +          ==> Says Spy B X # evsf \\<in> tls"
    1.11  
    1.12      SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
    1.13 -         "[| evsSK: tls;
    1.14 +         "[| evsSK \\<in> tls;
    1.15  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
    1.16            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    1.17 -			   Key (sessionK((NA,NB,M),role)) |} # evsSK : tls"
    1.18 +			   Key (sessionK((NA,NB,M),role)) |} # evsSK \\<in> tls"
    1.19  
    1.20      ClientHello
    1.21  	 (*(7.4.1.2)
    1.22 @@ -97,40 +97,40 @@
    1.23  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.24  	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    1.25             UNIX TIME is omitted because the protocol doesn't use it.
    1.26 -           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    1.27 +           May assume NA \\<notin> range PRF because CLIENT RANDOM is 28 bytes
    1.28  	   while MASTER SECRET is 48 bytes*)
    1.29 -         "[| evsCH: tls;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.30 +         "[| evsCH \\<in> tls;  Nonce NA \\<notin> used evsCH;  NA \\<notin> range PRF |]
    1.31            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.32 -	        # evsCH  :  tls"
    1.33 +	        # evsCH  \\<in>  tls"
    1.34  
    1.35      ServerHello
    1.36           (*7.4.1.3 of the TLS Internet-Draft
    1.37  	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.38             SERVER CERTIFICATE (7.4.2) is always present.
    1.39             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    1.40 -         "[| evsSH: tls;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.41 +         "[| evsSH \\<in> tls;  Nonce NB \\<notin> used evsSH;  NB \\<notin> range PRF;
    1.42               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.43 -	       : set evsSH |]
    1.44 -          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
    1.45 +	       \\<in> set evsSH |]
    1.46 +          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  \\<in>  tls"
    1.47  
    1.48      Certificate
    1.49           (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    1.50 -         "evsC: tls ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    1.51 +         "evsC \\<in> tls ==> Says B A (certificate B (pubK B)) # evsC  \\<in>  tls"
    1.52  
    1.53      ClientKeyExch
    1.54           (*CLIENT KEY EXCHANGE (7.4.7).
    1.55             The client, A, chooses PMS, the PREMASTER SECRET.
    1.56             She encrypts PMS using the supplied KB, which ought to be pubK B.
    1.57 -           We assume PMS ~: range PRF because a clash betweem the PMS
    1.58 +           We assume PMS \\<notin> range PRF because a clash betweem the PMS
    1.59             and another MASTER SECRET is highly unlikely (even though
    1.60  	   both items have the same length, 48 bytes).
    1.61             The Note event records in the trace that she knows PMS
    1.62                 (see REMARK at top). *)
    1.63 -         "[| evsCX: tls;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.64 -             Says B' A (certificate B KB) : set evsCX |]
    1.65 +         "[| evsCX \\<in> tls;  Nonce PMS \\<notin> used evsCX;  PMS \\<notin> range PRF;
    1.66 +             Says B' A (certificate B KB) \\<in> set evsCX |]
    1.67            ==> Says A B (Crypt KB (Nonce PMS))
    1.68  	      # Notes A {|Agent B, Nonce PMS|}
    1.69 -	      # evsCX  :  tls"
    1.70 +	      # evsCX  \\<in>  tls"
    1.71  
    1.72      CertVerify
    1.73  	(*The optional Certificate Verify (7.4.8) message contains the
    1.74 @@ -138,11 +138,11 @@
    1.75            It adds the pre-master-secret, which is also essential!
    1.76            Checking the signature, which is the only use of A's certificate,
    1.77            assures B of A's presence*)
    1.78 -         "[| evsCV: tls;  
    1.79 -             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
    1.80 -	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    1.81 +         "[| evsCV \\<in> tls;  
    1.82 +             Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCV;
    1.83 +	     Notes A {|Agent B, Nonce PMS|} \\<in> set evsCV |]
    1.84            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    1.85 -              # evsCV  :  tls"
    1.86 +              # evsCV  \\<in>  tls"
    1.87  
    1.88  	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
    1.89            among other things.  The master-secret is PRF(PMS,NA,NB).
    1.90 @@ -153,101 +153,101 @@
    1.91            rule's applying when the Spy has satisfied the "Says A B" by
    1.92            repaying messages sent by the true client; in that case, the
    1.93            Spy does not know PMS and could not send ClientFinished.  One
    1.94 -          could simply put A~=Spy into the rule, but one should not
    1.95 +          could simply put A\\<noteq>Spy into the rule, but one should not
    1.96            expect the spy to be well-behaved.*)
    1.97 -         "[| evsCF: tls;  
    1.98 +         "[| evsCF \\<in> tls;  
    1.99  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.100 -	       : set evsCF;
   1.101 -             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
   1.102 -             Notes A {|Agent B, Nonce PMS|} : set evsCF;
   1.103 +	       \\<in> set evsCF;
   1.104 +             Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCF;
   1.105 +             Notes A {|Agent B, Nonce PMS|} \\<in> set evsCF;
   1.106  	     M = PRF(PMS,NA,NB) |]
   1.107            ==> Says A B (Crypt (clientK(NA,NB,M))
   1.108  			(Hash{|Number SID, Nonce M,
   1.109  			       Nonce NA, Number PA, Agent A, 
   1.110  			       Nonce NB, Number PB, Agent B|}))
   1.111 -              # evsCF  :  tls"
   1.112 +              # evsCF  \\<in>  tls"
   1.113  
   1.114      ServerFinished
   1.115  	(*Keeping A' and A'' distinct means B cannot even check that the
   1.116            two messages originate from the same source. *)
   1.117 -         "[| evsSF: tls;
   1.118 +         "[| evsSF \\<in> tls;
   1.119  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
   1.120 -	       : set evsSF;
   1.121 -	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
   1.122 -	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
   1.123 +	       \\<in> set evsSF;
   1.124 +	     Says B  A  {|Nonce NB, Number SID, Number PB|} \\<in> set evsSF;
   1.125 +	     Says A'' B (Crypt (pubK B) (Nonce PMS)) \\<in> set evsSF;
   1.126  	     M = PRF(PMS,NA,NB) |]
   1.127            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.128  			(Hash{|Number SID, Nonce M,
   1.129  			       Nonce NA, Number PA, Agent A, 
   1.130  			       Nonce NB, Number PB, Agent B|}))
   1.131 -              # evsSF  :  tls"
   1.132 +              # evsSF  \\<in>  tls"
   1.133  
   1.134      ClientAccepts
   1.135  	(*Having transmitted ClientFinished and received an identical
   1.136            message encrypted with serverK, the client stores the parameters
   1.137            needed to resume this session.  The "Notes A ..." premise is
   1.138            used to prove Notes_master_imp_Crypt_PMS.*)
   1.139 -         "[| evsCA: tls;
   1.140 -	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
   1.141 +         "[| evsCA \\<in> tls;
   1.142 +	     Notes A {|Agent B, Nonce PMS|} \\<in> set evsCA;
   1.143  	     M = PRF(PMS,NA,NB);  
   1.144  	     X = Hash{|Number SID, Nonce M,
   1.145  	               Nonce NA, Number PA, Agent A, 
   1.146  		       Nonce NB, Number PB, Agent B|};
   1.147 -             Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
   1.148 -             Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
   1.149 +             Says A  B (Crypt (clientK(NA,NB,M)) X) \\<in> set evsCA;
   1.150 +             Says B' A (Crypt (serverK(NA,NB,M)) X) \\<in> set evsCA |]
   1.151            ==> 
   1.152 -             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
   1.153 +             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  \\<in>  tls"
   1.154  
   1.155      ServerAccepts
   1.156  	(*Having transmitted ServerFinished and received an identical
   1.157            message encrypted with clientK, the server stores the parameters
   1.158            needed to resume this session.  The "Says A'' B ..." premise is
   1.159            used to prove Notes_master_imp_Crypt_PMS.*)
   1.160 -         "[| evsSA: tls;
   1.161 -	     A ~= B;
   1.162 -             Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
   1.163 +         "[| evsSA \\<in> tls;
   1.164 +	     A \\<noteq> B;
   1.165 +             Says A'' B (Crypt (pubK B) (Nonce PMS)) \\<in> set evsSA;
   1.166  	     M = PRF(PMS,NA,NB);  
   1.167  	     X = Hash{|Number SID, Nonce M,
   1.168  	               Nonce NA, Number PA, Agent A, 
   1.169  		       Nonce NB, Number PB, Agent B|};
   1.170 -             Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   1.171 -             Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   1.172 +             Says B  A (Crypt (serverK(NA,NB,M)) X) \\<in> set evsSA;
   1.173 +             Says A' B (Crypt (clientK(NA,NB,M)) X) \\<in> set evsSA |]
   1.174            ==> 
   1.175 -             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   1.176 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \\<in>  tls"
   1.177  
   1.178      ClientResume
   1.179           (*If A recalls the SESSION_ID, then she sends a FINISHED message
   1.180             using the new nonces and stored MASTER SECRET.*)
   1.181 -         "[| evsCR: tls;  
   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|} : set evsCR;
   1.185 -             Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   1.186 +             Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCR;
   1.187 +             Notes A {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evsCR |]
   1.188            ==> Says A B (Crypt (clientK(NA,NB,M))
   1.189  			(Hash{|Number SID, Nonce M,
   1.190  			       Nonce NA, Number PA, Agent A, 
   1.191  			       Nonce NB, Number PB, Agent B|}))
   1.192 -              # evsCR  :  tls"
   1.193 +              # evsCR  \\<in>  tls"
   1.194  
   1.195      ServerResume
   1.196           (*Resumption (7.3):  If B finds the SESSION_ID then he can send
   1.197             a FINISHED message using the recovered MASTER SECRET*)
   1.198 -         "[| evsSR: tls;
   1.199 +         "[| evsSR \\<in> tls;
   1.200  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
   1.201 -	     Says B  A {|Nonce NB, Number SID, Number PB|} : set evsSR;  
   1.202 -             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR |]
   1.203 +	     Says B  A {|Nonce NB, Number SID, Number PB|} \\<in> set evsSR;  
   1.204 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evsSR |]
   1.205            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.206  			(Hash{|Number SID, Nonce M,
   1.207  			       Nonce NA, Number PA, Agent A, 
   1.208  			       Nonce NB, Number PB, Agent B|})) # evsSR
   1.209 -	        :  tls"
   1.210 +	        \\<in>  tls"
   1.211  
   1.212      Oops 
   1.213           (*The most plausible compromise is of an old session key.  Losing
   1.214             the MASTER SECRET or PREMASTER SECRET is more serious but
   1.215 -           rather unlikely.  The assumption A ~= Spy is essential: otherwise
   1.216 +           rather unlikely.  The assumption A \\<noteq> Spy is essential: otherwise
   1.217             the Spy could learn session keys merely by replaying messages!*)
   1.218 -         "[| evso: tls;  A ~= Spy;
   1.219 -	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso |]
   1.220 -          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  :  tls"
   1.221 +         "[| evso \\<in> tls;  A \\<noteq> Spy;
   1.222 +	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) \\<in> set evso |]
   1.223 +          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \\<in>  tls"
   1.224  
   1.225  end