src/HOL/Auth/TLS.thy
changeset 3687 fb7d096d7884
parent 3686 4b484805b4c4
child 3704 2f99d7a0dccc
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 18:27:31 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Mon Sep 22 13:17:29 1997 +0200
     1.3 @@ -66,7 +66,8 @@
     1.4  rules
     1.5    inj_PRF       "inj PRF"	
     1.6  
     1.7 -  (*sessionK is collision-free and makes symmetric keys*)
     1.8 +  (*sessionK is collision-free and makes symmetric keys.  Also, no clientK
     1.9 +    clashes with any serverK.*)
    1.10    inj_sessionK  "inj sessionK"	
    1.11  
    1.12    isSym_sessionK "isSymKey (sessionK x)"
    1.13 @@ -75,9 +76,6 @@
    1.14    inj_serverK   "inj serverK"	
    1.15    isSym_serverK "isSymKey (serverK x)"
    1.16  
    1.17 -  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    1.18 -  clientK_range "range clientK <= Compl (range serverK)"
    1.19 -
    1.20  
    1.21  consts    tls :: event list set
    1.22  inductive tls
    1.23 @@ -90,12 +88,11 @@
    1.24               X: synth (analz (spies evs)) |]
    1.25            ==> Says Spy B X # evs : tls"
    1.26  
    1.27 -    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    1.28 +    SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
    1.29           "[| evsSK: tls;
    1.30  	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    1.31            ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    1.32 -			    Key (clientK(NA,NB,M)),
    1.33 -			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    1.34 +			    Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    1.35  
    1.36      ClientHello
    1.37  	 (*(7.4.1.2)
    1.38 @@ -196,7 +193,8 @@
    1.39      ClientAccepts
    1.40  	(*Having transmitted ClientFinished and received an identical
    1.41            message encrypted with serverK, the client stores the parameters
    1.42 -          needed to resume this session.*)
    1.43 +          needed to resume this session.  The "Notes A ..." premise is
    1.44 +          used to prove Notes_master_imp_Crypt_PMS.*)
    1.45           "[| evsCA: tls;
    1.46  	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
    1.47  	     M = PRF(PMS,NA,NB);  
    1.48 @@ -211,7 +209,8 @@
    1.49      ServerAccepts
    1.50  	(*Having transmitted ServerFinished and received an identical
    1.51            message encrypted with clientK, the server stores the parameters
    1.52 -          needed to resume this session.*)
    1.53 +          needed to resume this session.  The "Says A'' B ..." premise is
    1.54 +          used to prove Notes_master_imp_Crypt_PMS.*)
    1.55           "[| evsSA: tls;
    1.56               Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    1.57  	       : set evsSA;