src/HOL/Auth/TLS.thy
changeset 5434 9b4bed3f394c
parent 5359 bd539b72d484
child 5653 204083e3f368
     1.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -82,8 +82,7 @@
     1.4           "[]: tls"
     1.5  
     1.6      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
     1.7 -         "[| evs: tls;  B ~= Spy;  
     1.8 -             X: synth (analz (spies evs)) |]
     1.9 +         "[| evs: tls;  X: synth (analz (spies evs)) |]
    1.10            ==> Says Spy B X # evs : tls"
    1.11  
    1.12      SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
    1.13 @@ -100,7 +99,7 @@
    1.14             UNIX TIME is omitted because the protocol doesn't use it.
    1.15             May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    1.16  	   while MASTER SECRET is 48 bytes*)
    1.17 -         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.18 +         "[| evsCH: tls;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.19            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.20  	        # evsCH  :  tls"
    1.21  
    1.22 @@ -109,14 +108,14 @@
    1.23  	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.24             SERVER CERTIFICATE (7.4.2) is always present.
    1.25             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    1.26 -         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.27 +         "[| evsSH: tls;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.28               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.29  	       : set evsSH |]
    1.30            ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
    1.31  
    1.32      Certificate
    1.33           (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    1.34 -         "[| evsC: tls;  A ~= B |]
    1.35 +         "[| evsC: tls |]
    1.36            ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    1.37  
    1.38      ClientKeyExch
    1.39 @@ -128,7 +127,7 @@
    1.40  	   both items have the same length, 48 bytes).
    1.41             The Note event records in the trace that she knows PMS
    1.42                 (see REMARK at top). *)
    1.43 -         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.44 +         "[| evsCX: tls;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.45               Says B' A (certificate B KB) : set evsCX |]
    1.46            ==> Says A B (Crypt KB (Nonce PMS))
    1.47  	      # Notes A {|Agent B, Nonce PMS|}
    1.48 @@ -140,7 +139,7 @@
    1.49            It adds the pre-master-secret, which is also essential!
    1.50            Checking the signature, which is the only use of A's certificate,
    1.51            assures B of A's presence*)
    1.52 -         "[| evsCV: tls;  A ~= B;  
    1.53 +         "[| evsCV: tls;  
    1.54               Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
    1.55  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    1.56            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    1.57 @@ -206,6 +205,7 @@
    1.58            needed to resume this session.  The "Says A'' B ..." premise is
    1.59            used to prove Notes_master_imp_Crypt_PMS.*)
    1.60           "[| evsSA: tls;
    1.61 +	     A ~= B;
    1.62               Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
    1.63  	     M = PRF(PMS,NA,NB);  
    1.64  	     X = Hash{|Number SID, Nonce M,
    1.65 @@ -245,8 +245,9 @@
    1.66      Oops 
    1.67           (*The most plausible compromise is of an old session key.  Losing
    1.68             the MASTER SECRET or PREMASTER SECRET is more serious but
    1.69 -           rather unlikely.*)
    1.70 -         "[| evso: tls;  A ~= Spy;  
    1.71 +           rather unlikely.  The assumption A ~= Spy is essential: otherwise
    1.72 +           the Spy could learn session keys merely by replaying messages!*)
    1.73 +         "[| evso: tls;  A ~= Spy;
    1.74  	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
    1.75            ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
    1.76