New proofs involving CERTIFICATE VERIFY
authorpaulson
Mon Jul 07 10:49:14 1997 +0200 (1997-07-07)
changeset 3506a36e0a49d2cd
parent 3505 1cb4ea47d967
child 3507 157be29ad5ba
New proofs involving CERTIFICATE VERIFY
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Mon Jul 07 09:09:21 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Mon Jul 07 10:49:14 1997 +0200
     1.3 @@ -125,11 +125,12 @@
     1.4  
     1.5  (*Another one, for CertVerify (which is optional)*)
     1.6  goal thy 
     1.7 - "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
     1.8 + "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
     1.9  \  Says A B (Crypt (priK A)                 \
    1.10 -\            (Hash{|Nonce NB, certificate B (pubK B)|})) : set evs";
    1.11 +\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
    1.12  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.13 -by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
    1.14 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.15 +	  RS tls.CertVerify) 2);
    1.16  by possibility_tac;
    1.17  result();
    1.18  
    1.19 @@ -226,26 +227,24 @@
    1.20  by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.21  		      addSEs partsEs) 1);
    1.22  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
    1.23 -(*ServerFinished*)
    1.24 -by (Blast_tac 3);
    1.25 -(*ClientFinished*)
    1.26 -by (Blast_tac 2);
    1.27  by (Fake_parts_insert_tac 1);
    1.28 +(*CertVerify, ClientFinished, ServerFinished (?)*)
    1.29 +by (REPEAT (Blast_tac 1));
    1.30  qed "Hash_imp_Nonce_seen";
    1.31  
    1.32  
    1.33  (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
    1.34  
    1.35 -(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
    1.36 +(*B can check A's signature if he has received A's certificate.
    1.37 +  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
    1.38    message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.39    assume A~:lost; otherwise, the Spy can forge A's signature.*)
    1.40  goalw thy [certificate_def]
    1.41 - "!!evs. [| X = Crypt (priK A)                          \
    1.42 -\                 (Hash{|Nonce NB,                                      \
    1.43 -\                        certificate B KB|});    \
    1.44 -\           evs : tls;  A ~: lost;  B ~= Spy |]         \
    1.45 -\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
    1.46 -\                   certificate B KB|} : set evs --> \
    1.47 + "!!evs. [| X = Crypt (priK A)                                        \
    1.48 +\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
    1.49 +\           evs : tls;  A ~: lost;  B ~= Spy |]                       \
    1.50 +\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
    1.51 +\          : set evs --> \
    1.52  \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
    1.53  by (hyp_subst_tac 1);
    1.54  by (etac tls.induct 1);
    1.55 @@ -257,14 +256,23 @@
    1.56  qed_spec_mp "TrustCertVerify";
    1.57  
    1.58  
    1.59 +goal thy
    1.60 + "!!evs. [| evs : tls;  A ~= Spy |]                                      \
    1.61 +\ ==> Says A B (Crypt (priK A)                                           \
    1.62 +\               (Hash{|Nonce NB, certificate B KB, Nonce M|})) : set evs \
    1.63 +\     --> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} : set evs";
    1.64 +by (etac tls.induct 1);
    1.65 +by (ALLGOALS Asm_full_simp_tac);
    1.66 +bind_thm ("UseCertVerify", result() RSN (2, rev_mp));
    1.67 +
    1.68 +
    1.69  (*This lemma says that no false certificates exist.  One might extend the
    1.70    model to include bogus certificates for the lost agents, but there seems
    1.71    little point in doing so: the loss of their private keys is a worse
    1.72    breach of security.*)
    1.73  goalw thy [certificate_def]
    1.74   "!!evs. evs : tls     \
    1.75 -\    ==> certificate B KB : parts (sees lost Spy evs) \
    1.76 -\        --> KB = pubK B";
    1.77 +\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
    1.78  by (etac tls.induct 1);
    1.79  by (ALLGOALS Asm_simp_tac);
    1.80  by (Fake_parts_insert_tac 2);
    1.81 @@ -359,10 +367,9 @@
    1.82    The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
    1.83    here.*)
    1.84  goalw thy [certificate_def]
    1.85 - "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
    1.86 -\        ==> Says A B {|certificate A (pubK A), \
    1.87 -\                       Crypt KB (Nonce M)|} : set evs -->             \
    1.88 -\            Nonce M ~: analz (sees lost Spy evs)";
    1.89 + "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                        \
    1.90 +\        ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
    1.91 +\              : set evs  -->  Nonce M ~: analz (sees lost Spy evs)";
    1.92  by (analz_induct_tac 1);
    1.93  (*ClientHello*)
    1.94  by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
    1.95 @@ -420,11 +427,10 @@
    1.96   "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
    1.97  \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
    1.98  \                        Nonce NA, Agent XA, Agent A,               \
    1.99 -\                        Nonce NB, Agent XB,                        \
   1.100 -\                        certificate B (pubK B)|}); \
   1.101 +\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
   1.102  \           evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.103 -\    ==> Says A B {|certificate A (pubK A),  \
   1.104 -\                   Crypt KB (Nonce M)|} : set evs -->              \
   1.105 +\    ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
   1.106 +\          : set evs -->              \
   1.107  \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.108  by (hyp_subst_tac 1);
   1.109  by (etac tls.induct 1);
   1.110 @@ -444,8 +450,8 @@
   1.111  
   1.112  (*** Protocol goal: if B receives CLIENT FINISHED, then A has used the
   1.113       quoted values XA, XB, etc., which B can then check.  BUT NOTE:
   1.114 -     B has no way of knowing that A is the sender of CERTIFICATE VERIFY
   1.115 - ***)
   1.116 +     B has no way of knowing that A is the sender of CLIENT CERTIFICATE!
   1.117 +***)
   1.118  goalw thy [certificate_def]
   1.119   "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.120  \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.121 @@ -454,7 +460,7 @@
   1.122  \                        Nonce NB, Agent XB, Agent B|});        \
   1.123  \           evs : tls;  A~=Spy;  B ~: lost |]                   \
   1.124  \     ==> Says A B {|certificate A (pubK A),                    \
   1.125 -\                    Crypt KB (Nonce M)|} : set evs -->              \
   1.126 +\                    Crypt KB (Nonce M)|} : set evs -->         \
   1.127  \         X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.128  by (hyp_subst_tac 1);
   1.129  by (etac tls.induct 1);
   1.130 @@ -470,3 +476,29 @@
   1.131  				     not_parts_not_analz]) 2);
   1.132  by (Fake_parts_insert_tac 1);
   1.133  qed_spec_mp "TrustClientFinished";
   1.134 +
   1.135 +
   1.136 +(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
   1.137 +     check a CERTIFICATE VERIFY from A, then A has used the quoted
   1.138 +     values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.139 + ***)
   1.140 +goal thy
   1.141 + "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.142 +\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.143 +\                        Nonce NA, Agent XA,                    \
   1.144 +\                        certificate A (pubK A),                \
   1.145 +\                        Nonce NB, Agent XB, Agent B|});        \
   1.146 +\           Says A' B X : set evs;                              \
   1.147 +\           Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   1.148 +\             : set evs;                                        \
   1.149 +\           Says A'' B (Crypt (priK A)                                   \
   1.150 +\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))   \
   1.151 +\             : set evs;                                        \
   1.152 +\        evs : tls;  A ~: lost;  B ~: lost |]                   \
   1.153 +\     ==> Says A B X : set evs";
   1.154 +br TrustClientFinished 1;
   1.155 +br (TrustCertVerify RS UseCertVerify) 5;
   1.156 +by (REPEAT_FIRST (ares_tac [refl]));
   1.157 +by (ALLGOALS 
   1.158 +    (asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj])));
   1.159 +qed_spec_mp "AuthClientFinished";
     2.1 --- a/src/HOL/Auth/TLS.thy	Mon Jul 07 09:09:21 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Mon Jul 07 10:49:14 1997 +0200
     2.3 @@ -18,13 +18,6 @@
     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 @@ -96,23 +89,23 @@
    2.18           (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    2.19             Note that A encrypts using the supplied KB, not pubK B.*)
    2.20           "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    2.21 -             Says B' A {|Nonce NA, Nonce NB, Agent XB,
    2.22 -			 certificate B KB|} : set evs |]
    2.23 -          ==> Says A B {|certificate A (pubK A),
    2.24 -			 Crypt KB (Nonce M)|}
    2.25 +             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.26 +	       : set evs |]
    2.27 +          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.28                  # evs  :  tls"
    2.29  
    2.30      CertVerify
    2.31  	(*The optional CERTIFICATE VERIFY message contains the specific
    2.32 -          components listed in the security analysis, Appendix F.1.1.2.
    2.33 -          By checking the signature, B is assured of A's existence:
    2.34 -          the only use of A's certificate.*)
    2.35 +          components listed in the security analysis, Appendix F.1.1.2;
    2.36 +          it also contains the pre-master-secret.  Checking the signature,
    2.37 +          which is the only use of A's certificate, assures B of A's presence*)
    2.38           "[| evs: tls;  A ~= B;  
    2.39 -             Says B' A {|Nonce NA, Nonce NB, Agent XB,
    2.40 -			 certificate B KB|} : set evs |]
    2.41 +             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.42 +	       : set evs;
    2.43 +	     Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.44 +	       : set evs |]
    2.45            ==> Says A B (Crypt (priK A)
    2.46 -			(Hash{|Nonce NB,
    2.47 -	 		       certificate B KB|}))
    2.48 +			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
    2.49                  # evs  :  tls"
    2.50  
    2.51  	(*Finally come the FINISHED messages, confirming XA and XB among
    2.52 @@ -122,10 +115,10 @@
    2.53      ClientFinished
    2.54           "[| evs: tls;  A ~= B;
    2.55  	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
    2.56 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, 
    2.57 -			 certificate B KB|} : set evs;
    2.58 -             Says A  B {|certificate A (pubK A),
    2.59 -		         Crypt KB (Nonce M)|} : set evs |]
    2.60 +             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.61 +	       : set evs;
    2.62 +             Says A  B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.63 +	       : set evs |]
    2.64            ==> Says A B (Crypt (clientK(NA,NB,M))
    2.65  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
    2.66  			       Nonce NA, Agent XA,