New constant "certificate"--just an abbreviation
authorpaulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 35000d8ad2f192d8
parent 3499 ce1664057431
child 3501 4ab477ffb4c6
New constant "certificate"--just an abbreviation
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Jul 04 14:37:30 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Jul 04 17:34:55 1997 +0200
     1.3 @@ -5,11 +5,12 @@
     1.4  
     1.5  The public-key model has a weakness, especially concerning anonymous sessions.
     1.6  The Spy's state is recorded as the trace of message.  But if he himself is the
     1.7 -Client and invents M, then he sends contains M encrypted with B's public key.
     1.8 -This message gives no evidence that the spy knows M, and yet the spy actually
     1.9 -chose M!  So, in any property concerning the secrecy of some item, one must
    1.10 -establish that the spy didn't choose the item.  Guarantees normally assume
    1.11 -that the other party is uncompromised (otherwise, one can prove little).
    1.12 +Client and invents M, then he encrypts M with B's public key before sending
    1.13 +it.  This message gives no evidence that the spy knows M, and yet the spy
    1.14 +actually chose M!  So, in any property concerning the secrecy of some item,
    1.15 +one must establish that the spy didn't choose the item.  Guarantees normally
    1.16 +assume that the other party is uncompromised (otherwise, one can prove
    1.17 +little).
    1.18  
    1.19  Protocol goals: 
    1.20  * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    1.21 @@ -23,17 +24,6 @@
    1.22  * Each party who has received a FINISHED message can trust that the other
    1.23    party agrees on all message components, including XA and XB (thus foiling
    1.24    rollback attacks).
    1.25 -
    1.26 -A curious property found in these proofs is that CERTIFICATE VERIFY actually
    1.27 -gives weaker authentication than CLIENT FINISHED.  The theorem for CERTIFICATE
    1.28 -VERIFY is subject to A~:lost, since if A's private key is known to the spy
    1.29 -then he can forge A's signature.  But the theorem for CLIENT FINISHED merely
    1.30 -assumes that A is not the spy himself, since the model assumes that all other
    1.31 -agents tell the truth.
    1.32 -
    1.33 -In the real world, there are agents who are not active attackers, and yet
    1.34 -still cannot be trusted to identify themselves.  There may well be more such
    1.35 -agents than there are compromised private keys.
    1.36  *)
    1.37  
    1.38  open TLS;
    1.39 @@ -42,6 +32,7 @@
    1.40  HOL_quantifiers := false;
    1.41  
    1.42  AddIffs [Spy_in_lost, Server_not_lost];
    1.43 +Addsimps [certificate_def];
    1.44  
    1.45  goal thy "!!A. A ~: lost ==> A ~= Spy";
    1.46  by (Blast_tac 1);
    1.47 @@ -110,7 +101,7 @@
    1.48  \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    1.49  \                   Nonce NA, Agent XA, Agent A,      \
    1.50  \                   Nonce NB, Agent XB,               \
    1.51 -\                   Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
    1.52 +\                   certificate B (pubK B)|})) \
    1.53  \    : set evs";
    1.54  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.55  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.56 @@ -124,7 +115,7 @@
    1.57  \  Says A B (Crypt (clientK(NA,NB,M))                 \
    1.58  \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    1.59  \                   Nonce NA, Agent XA,               \
    1.60 -\                   Crypt (priK Server) {|Agent A, Key (pubK A)|},      \
    1.61 +\                   certificate A (pubK A),      \
    1.62  \                   Nonce NB, Agent XB, Agent B|})) : set evs";
    1.63  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.64  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.65 @@ -136,9 +127,7 @@
    1.66  goal thy 
    1.67   "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
    1.68  \  Says A B (Crypt (priK A)                 \
    1.69 -\            (Hash{|Nonce NB,               \
    1.70 -\                   Crypt (priK Server)     \
    1.71 -\                         {|Agent B, Key (pubK B)|}|})) : set evs";
    1.72 +\            (Hash{|Nonce NB, certificate B (pubK B)|})) : set evs";
    1.73  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.74  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
    1.75  by possibility_tac;
    1.76 @@ -250,13 +239,13 @@
    1.77  (*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
    1.78    message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.79    assume A~:lost; otherwise, the Spy can forge A's signature.*)
    1.80 -goal thy 
    1.81 +goalw thy [certificate_def]
    1.82   "!!evs. [| X = Crypt (priK A)                          \
    1.83  \                 (Hash{|Nonce NB,                                      \
    1.84 -\                        Crypt (priK Server) {|Agent B, Key KB|}|});    \
    1.85 +\                        certificate B KB|});    \
    1.86  \           evs : tls;  A ~: lost;  B ~= Spy |]         \
    1.87  \    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
    1.88 -\                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
    1.89 +\                   certificate B KB|} : set evs --> \
    1.90  \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
    1.91  by (hyp_subst_tac 1);
    1.92  by (etac tls.induct 1);
    1.93 @@ -272,9 +261,9 @@
    1.94    model to include bogus certificates for the lost agents, but there seems
    1.95    little point in doing so: the loss of their private keys is a worse
    1.96    breach of security.*)
    1.97 -goal thy 
    1.98 +goalw thy [certificate_def]
    1.99   "!!evs. evs : tls     \
   1.100 -\    ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
   1.101 +\    ==> certificate B KB : parts (sees lost Spy evs) \
   1.102  \        --> KB = pubK B";
   1.103  by (etac tls.induct 1);
   1.104  by (ALLGOALS Asm_simp_tac);
   1.105 @@ -369,9 +358,9 @@
   1.106  (*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
   1.107    The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
   1.108    here.*)
   1.109 -goal thy 
   1.110 +goalw thy [certificate_def]
   1.111   "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.112 -\        ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.113 +\        ==> Says A B {|certificate A (pubK A), \
   1.114  \                       Crypt KB (Nonce M)|} : set evs -->             \
   1.115  \            Nonce M ~: analz (sees lost Spy evs)";
   1.116  by (analz_induct_tac 1);
   1.117 @@ -427,14 +416,14 @@
   1.118       to compare XA with what she originally sent.
   1.119  ***)
   1.120  
   1.121 -goal thy 
   1.122 +goalw thy [certificate_def]
   1.123   "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
   1.124  \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
   1.125  \                        Nonce NA, Agent XA, Agent A,               \
   1.126  \                        Nonce NB, Agent XB,                        \
   1.127 -\                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
   1.128 +\                        certificate B (pubK B)|}); \
   1.129  \           evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.130 -\    ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.131 +\    ==> Says A B {|certificate A (pubK A),  \
   1.132  \                   Crypt KB (Nonce M)|} : set evs -->              \
   1.133  \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.134  by (hyp_subst_tac 1);
   1.135 @@ -453,20 +442,18 @@
   1.136  qed_spec_mp "TrustServerFinished";
   1.137  
   1.138  
   1.139 -(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present
   1.140 -     and has used the quoted values XA, XB, etc.  Note that it is up to B
   1.141 -     to compare XB with what he originally sent. ***)
   1.142 -
   1.143 -(*This result seems too strong: A need not have sent CERTIFICATE VERIFY.  
   1.144 -  But we assume (as always) that the other party is honest...*)
   1.145 -goal thy 
   1.146 +(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the
   1.147 +     quoted values XA, XB, etc., which B can then check.  BUT NOTE:
   1.148 +     B has no way of knowing that A is the sender of CERTIFICATE VERIFY
   1.149 + ***)
   1.150 +goalw thy [certificate_def]
   1.151   "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.152  \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.153  \                        Nonce NA, Agent XA,                    \
   1.154 -\                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.155 +\                        certificate A (pubK A),                \
   1.156  \                        Nonce NB, Agent XB, Agent B|});        \
   1.157  \           evs : tls;  A~=Spy;  B ~: lost |]                   \
   1.158 -\     ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.159 +\     ==> Says A B {|certificate A (pubK A),                    \
   1.160  \                    Crypt KB (Nonce M)|} : set evs -->              \
   1.161  \         X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.162  by (hyp_subst_tac 1);
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Jul 04 14:37:30 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Fri Jul 04 17:34:55 1997 +0200
     2.3 @@ -18,6 +18,13 @@
     2.4  Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
     2.5  Allen, Transport Layer Security Working Group, 21 May 1997,
     2.6  INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
     2.7 +
     2.8 +
     2.9 +FOR CertVerify
    2.10 +;
    2.11 +	     Says A B {|certificate A (pubK A),
    2.12 +			 Crypt KB (Nonce M)|} : set evs
    2.13 +
    2.14  *)
    2.15  
    2.16  TLS = Public + 
    2.17 @@ -25,6 +32,11 @@
    2.18  consts
    2.19    (*Client, server write keys.  They implicitly include the MAC secrets.*)
    2.20    clientK, serverK :: "nat*nat*nat => key"
    2.21 +  certificate      :: "[agent,key] => msg"
    2.22 +
    2.23 +defs
    2.24 +  certificate_def
    2.25 +    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    2.26  
    2.27  rules
    2.28    (*clientK is collision-free and makes symmetric keys*)
    2.29 @@ -77,7 +89,7 @@
    2.30           "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    2.31               Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    2.32            ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    2.33 -			 Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
    2.34 +			 certificate B (pubK B)|}
    2.35                  # evs  :  tls"
    2.36  
    2.37      ClientCertKeyEx
    2.38 @@ -85,8 +97,8 @@
    2.39             Note that A encrypts using the supplied KB, not pubK B.*)
    2.40           "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    2.41               Says B' A {|Nonce NA, Nonce NB, Agent XB,
    2.42 -			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    2.43 -          ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
    2.44 +			 certificate B KB|} : set evs |]
    2.45 +          ==> Says A B {|certificate A (pubK A),
    2.46  			 Crypt KB (Nonce M)|}
    2.47                  # evs  :  tls"
    2.48  
    2.49 @@ -97,10 +109,10 @@
    2.50            the only use of A's certificate.*)
    2.51           "[| evs: tls;  A ~= B;  
    2.52               Says B' A {|Nonce NA, Nonce NB, Agent XB,
    2.53 -			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    2.54 +			 certificate B KB|} : set evs |]
    2.55            ==> Says A B (Crypt (priK A)
    2.56  			(Hash{|Nonce NB,
    2.57 -	 		       Crypt (priK Server) {|Agent B, Key KB|}|}))
    2.58 +	 		       certificate B KB|}))
    2.59                  # evs  :  tls"
    2.60  
    2.61  	(*Finally come the FINISHED messages, confirming XA and XB among
    2.62 @@ -111,13 +123,13 @@
    2.63           "[| evs: tls;  A ~= B;
    2.64  	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
    2.65               Says B' A {|Nonce NA, Nonce NB, Agent XB, 
    2.66 -			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
    2.67 -             Says A  B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
    2.68 +			 certificate B KB|} : set evs;
    2.69 +             Says A  B {|certificate A (pubK A),
    2.70  		         Crypt KB (Nonce M)|} : set evs |]
    2.71            ==> Says A B (Crypt (clientK(NA,NB,M))
    2.72  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
    2.73  			       Nonce NA, Agent XA,
    2.74 -			       Crypt (priK Server) {|Agent A, Key(pubK A)|}, 
    2.75 +			       certificate A (pubK A), 
    2.76  			       Nonce NB, Agent XB, Agent B|}))
    2.77                  # evs  :  tls"
    2.78  
    2.79 @@ -128,14 +140,14 @@
    2.80           "[| evs: tls;  A ~= B;
    2.81  	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
    2.82  	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
    2.83 -		 	  Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
    2.84 +		 	  certificate B (pubK B)|}
    2.85  	       : set evs;
    2.86  	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
    2.87            ==> Says B A (Crypt (serverK(NA,NB,M))
    2.88  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
    2.89  			       Nonce NA, Agent XA, Agent A, 
    2.90  			       Nonce NB, Agent XB,
    2.91 -			       Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
    2.92 +			       certificate B (pubK B)|}))
    2.93                  # evs  :  tls"
    2.94  
    2.95    (**Oops message??**)