src/HOL/Auth/TLS.thy
changeset 3745 4c5d3b1ddc75
parent 3729 6be7cf5086ab
child 3757 7524781c5c83
     1.1 --- a/src/HOL/Auth/TLS.thy	Mon Sep 29 15:39:28 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 30 11:03:55 1997 +0200
     1.3 @@ -21,9 +21,9 @@
     1.4  The model assumes that no fraudulent certificates are present, but it does
     1.5  assume that some private keys are to the spy.
     1.6  
     1.7 -REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
     1.8 +REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
     1.9  CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    1.10 -herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    1.11 +herself.  Nobody else can see it.  In ClientKeyExch, the Spy can substitute
    1.12  his own certificate for A's, but he cannot replace A's note by one for himself.
    1.13  
    1.14  The Note event avoids a weakness in the public-key model.  Each
    1.15 @@ -33,7 +33,7 @@
    1.16  In the shared-key model, the ability to encrypt implies the ability to
    1.17  decrypt, so the problem does not arise.
    1.18  
    1.19 -Proofs would be simpler if ClientCertKeyEx included A's name within
    1.20 +Proofs would be simpler if ClientKeyExch included A's name within
    1.21  Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
    1.22  about that message (which B receives) and the stronger event
    1.23  	Notes A {|Agent B, Nonce PMS|}.
    1.24 @@ -61,17 +61,18 @@
    1.25      clientK, serverK :: "nat*nat*nat => key"
    1.26  
    1.27  translations
    1.28 -  "clientK (x)"	== "sessionK(x,0)"
    1.29 -  "serverK (x)"	== "sessionK(x,1)"
    1.30 +  "clientK (nonces)"	== "sessionK(nonces,0)"
    1.31 +  "serverK (nonces)"	== "sessionK(nonces,1)"
    1.32  
    1.33  rules
    1.34 +  (*the pseudo-random function is collision-free*)
    1.35    inj_PRF       "inj PRF"	
    1.36  
    1.37 -  (*sessionK is collision-free and makes symmetric keys.  Also, no clientK
    1.38 -    clashes with any serverK.*)
    1.39 +  (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
    1.40    inj_sessionK  "inj sessionK"	
    1.41  
    1.42 -  isSym_sessionK "isSymKey (sessionK x)"
    1.43 +  (*sessionK makes symmetric keys*)
    1.44 +  isSym_sessionK "isSymKey (sessionK nonces)"
    1.45  
    1.46  
    1.47  consts    tls :: event list set
    1.48 @@ -111,12 +112,15 @@
    1.49           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.50               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.51  	       : set evsSH |]
    1.52 -          ==> Says B A {|Nonce NB, Number SID, Number PB,
    1.53 -			 certificate B (pubK B)|}
    1.54 -                # evsSH  :  tls"
    1.55 +          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
    1.56  
    1.57 -    ClientCertKeyEx
    1.58 -         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
    1.59 +    Certificate
    1.60 +         (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    1.61 +         "[| evsC: tls;  A ~= B |]
    1.62 +          ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    1.63 +
    1.64 +    ClientKeyExch
    1.65 +         (*CLIENT KEY EXCHANGE (7.4.7).
    1.66             The client, A, chooses PMS, the PREMASTER SECRET.
    1.67             She encrypts PMS using the supplied KB, which ought to be pubK B.
    1.68             We assume PMS ~: range PRF because a clash betweem the PMS
    1.69 @@ -125,9 +129,9 @@
    1.70             The Note event records in the trace that she knows PMS
    1.71                 (see REMARK at top). *)
    1.72           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.73 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.74 -	       : set evsCX |]
    1.75 -          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    1.76 +             Says B'  A {|Nonce NB, Number SID, Number PB|} : set evsCX;
    1.77 +             Says B'' A (certificate B KB) : set evsCX |]
    1.78 +          ==> Says A B (Crypt KB (Nonce PMS))
    1.79  	      # Notes A {|Agent B, Nonce PMS|}
    1.80  	      # evsCX  :  tls"
    1.81  
    1.82 @@ -138,8 +142,7 @@
    1.83            Checking the signature, which is the only use of A's certificate,
    1.84            assures B of A's presence*)
    1.85           "[| evsCV: tls;  A ~= B;  
    1.86 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.87 -	       : set evsCV;
    1.88 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
    1.89  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    1.90            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    1.91                # evsCV  :  tls"
    1.92 @@ -158,8 +161,7 @@
    1.93           "[| evsCF: tls;  
    1.94  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.95  	       : set evsCF;
    1.96 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.97 -	       : set evsCF;
    1.98 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
    1.99               Notes A {|Agent B, Nonce PMS|} : set evsCF;
   1.100  	     M = PRF(PMS,NA,NB) |]
   1.101            ==> Says A B (Crypt (clientK(NA,NB,M))
   1.102 @@ -174,11 +176,8 @@
   1.103           "[| evsSF: tls;
   1.104  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
   1.105  	       : set evsSF;
   1.106 -	     Says B  A  {|Nonce NB, Number SID, Number PB,
   1.107 -		 	  certificate B (pubK B)|}
   1.108 -	       : set evsSF;
   1.109 -	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   1.110 -	       : set evsSF;
   1.111 +	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
   1.112 +	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
   1.113  	     M = PRF(PMS,NA,NB) |]
   1.114            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.115  			(Hash{|Nonce M, Number SID,
   1.116 @@ -208,8 +207,7 @@
   1.117            needed to resume this session.  The "Says A'' B ..." premise is
   1.118            used to prove Notes_master_imp_Crypt_PMS.*)
   1.119           "[| evsSA: tls;
   1.120 -             Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   1.121 -	       : set evsSA;
   1.122 +             Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
   1.123  	     M = PRF(PMS,NA,NB);  
   1.124  	     X = Hash{|Nonce M, Number SID,
   1.125  	               Nonce NA, Number PA, Agent A, 
   1.126 @@ -220,9 +218,8 @@
   1.127               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   1.128  
   1.129      ServerResume
   1.130 -         (*Resumption is described in 7.3.  If B finds the SESSION_ID
   1.131 -           then he sends HELLO and FINISHED messages, using the
   1.132 -           previously stored MASTER SECRET*)
   1.133 +         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
   1.134 +           a FINISHED message using the recovered MASTER SECRET*)
   1.135           "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   1.136               Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   1.137  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.138 @@ -230,12 +227,12 @@
   1.139            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.140  			(Hash{|Nonce M, Number SID,
   1.141  			       Nonce NA, Number PA, Agent A, 
   1.142 -			       Nonce NB, Number PB, Agent B|}))
   1.143 -              # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR  :  tls"
   1.144 +			       Nonce NB, Number PB, Agent B|})) # evsSR
   1.145 +	        :  tls"
   1.146  
   1.147      ClientResume
   1.148 -         (*If the response to ClientHello is ServerResume then send
   1.149 -           a FINISHED message using the new nonces and stored MASTER SECRET.*)
   1.150 +         (*If A recalls the SESSION_ID, then she sends a FINISHED message
   1.151 +           using the new nonces and stored MASTER SECRET.*)
   1.152           "[| evsCR: tls;  
   1.153  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.154  	       : set evsCR;