# HG changeset patch
# User paulson
# Date 868265354 -7200
# Node ID a36e0a49d2cd06f9ae8c4b1ad0411da9bef0d78d
# Parent  1cb4ea47d967463a0614e03b9118f2d5ff1998c5
New proofs involving CERTIFICATE VERIFY

diff -r 1cb4ea47d967 -r a36e0a49d2cd src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Mon Jul 07 09:09:21 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Mon Jul 07 10:49:14 1997 +0200
@@ -125,11 +125,12 @@
 
 (*Another one, for CertVerify (which is optional)*)
 goal thy 
- "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
+ "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
 \  Says A B (Crypt (priK A)                 \
-\            (Hash{|Nonce NB, certificate B (pubK B)|})) : set evs";
+\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
+	  RS tls.CertVerify) 2);
 by possibility_tac;
 result();
 
@@ -226,26 +227,24 @@
 by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
 		      addSEs partsEs) 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
-(*ServerFinished*)
-by (Blast_tac 3);
-(*ClientFinished*)
-by (Blast_tac 2);
 by (Fake_parts_insert_tac 1);
+(*CertVerify, ClientFinished, ServerFinished (?)*)
+by (REPEAT (Blast_tac 1));
 qed "Hash_imp_Nonce_seen";
 
 
 (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
 
-(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
+(*B can check A's signature if he has received A's certificate.
+  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   assume A~:lost; otherwise, the Spy can forge A's signature.*)
 goalw thy [certificate_def]
- "!!evs. [| X = Crypt (priK A)                          \
-\                 (Hash{|Nonce NB,                                      \
-\                        certificate B KB|});    \
-\           evs : tls;  A ~: lost;  B ~= Spy |]         \
-\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
-\                   certificate B KB|} : set evs --> \
+ "!!evs. [| X = Crypt (priK A)                                        \
+\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
+\           evs : tls;  A ~: lost;  B ~= Spy |]                       \
+\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
+\          : set evs --> \
 \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
 by (etac tls.induct 1);
@@ -257,14 +256,23 @@
 qed_spec_mp "TrustCertVerify";
 
 
+goal thy
+ "!!evs. [| evs : tls;  A ~= Spy |]                                      \
+\ ==> Says A B (Crypt (priK A)                                           \
+\               (Hash{|Nonce NB, certificate B KB, Nonce M|})) : set evs \
+\     --> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} : set evs";
+by (etac tls.induct 1);
+by (ALLGOALS Asm_full_simp_tac);
+bind_thm ("UseCertVerify", result() RSN (2, rev_mp));
+
+
 (*This lemma says that no false certificates exist.  One might extend the
   model to include bogus certificates for the lost agents, but there seems
   little point in doing so: the loss of their private keys is a worse
   breach of security.*)
 goalw thy [certificate_def]
  "!!evs. evs : tls     \
-\    ==> certificate B KB : parts (sees lost Spy evs) \
-\        --> KB = pubK B";
+\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
 by (etac tls.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Fake_parts_insert_tac 2);
@@ -359,10 +367,9 @@
   The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
   here.*)
 goalw thy [certificate_def]
- "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
-\        ==> Says A B {|certificate A (pubK A), \
-\                       Crypt KB (Nonce M)|} : set evs -->             \
-\            Nonce M ~: analz (sees lost Spy evs)";
+ "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                        \
+\        ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
+\              : set evs  -->  Nonce M ~: analz (sees lost Spy evs)";
 by (analz_induct_tac 1);
 (*ClientHello*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
@@ -420,11 +427,10 @@
  "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
 \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
 \                        Nonce NA, Agent XA, Agent A,               \
-\                        Nonce NB, Agent XB,                        \
-\                        certificate B (pubK B)|}); \
+\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
 \           evs : tls;  A~=Spy;  B ~: lost |]                       \
-\    ==> Says A B {|certificate A (pubK A),  \
-\                   Crypt KB (Nonce M)|} : set evs -->              \
+\    ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
+\          : set evs -->              \
 \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
 by (etac tls.induct 1);
@@ -444,8 +450,8 @@
 
 (*** Protocol goal: if B receives CLIENT FINISHED, then A has used the
      quoted values XA, XB, etc., which B can then check.  BUT NOTE:
-     B has no way of knowing that A is the sender of CERTIFICATE VERIFY
- ***)
+     B has no way of knowing that A is the sender of CLIENT CERTIFICATE!
+***)
 goalw thy [certificate_def]
  "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
 \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
@@ -454,7 +460,7 @@
 \                        Nonce NB, Agent XB, Agent B|});        \
 \           evs : tls;  A~=Spy;  B ~: lost |]                   \
 \     ==> Says A B {|certificate A (pubK A),                    \
-\                    Crypt KB (Nonce M)|} : set evs -->              \
+\                    Crypt KB (Nonce M)|} : set evs -->         \
 \         X : parts (sees lost Spy evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
 by (etac tls.induct 1);
@@ -470,3 +476,29 @@
 				     not_parts_not_analz]) 2);
 by (Fake_parts_insert_tac 1);
 qed_spec_mp "TrustClientFinished";
+
+
+(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
+     check a CERTIFICATE VERIFY from A, then A has used the quoted
+     values XA, XB, etc.  Even this one requires A to be uncompromised.
+ ***)
+goal thy
+ "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
+\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
+\                        Nonce NA, Agent XA,                    \
+\                        certificate A (pubK A),                \
+\                        Nonce NB, Agent XB, Agent B|});        \
+\           Says A' B X : set evs;                              \
+\           Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
+\             : set evs;                                        \
+\           Says A'' B (Crypt (priK A)                                   \
+\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))   \
+\             : set evs;                                        \
+\        evs : tls;  A ~: lost;  B ~: lost |]                   \
+\     ==> Says A B X : set evs";
+br TrustClientFinished 1;
+br (TrustCertVerify RS UseCertVerify) 5;
+by (REPEAT_FIRST (ares_tac [refl]));
+by (ALLGOALS 
+    (asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj])));
+qed_spec_mp "AuthClientFinished";
diff -r 1cb4ea47d967 -r a36e0a49d2cd src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Mon Jul 07 09:09:21 1997 +0200
+++ b/src/HOL/Auth/TLS.thy	Mon Jul 07 10:49:14 1997 +0200
@@ -18,13 +18,6 @@
 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
 Allen, Transport Layer Security Working Group, 21 May 1997,
 INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
-
-
-FOR CertVerify
-;
-	     Says A B {|certificate A (pubK A),
-			 Crypt KB (Nonce M)|} : set evs
-
 *)
 
 TLS = Public + 
@@ -96,23 +89,23 @@
          (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
            Note that A encrypts using the supplied KB, not pubK B.*)
          "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
-             Says B' A {|Nonce NA, Nonce NB, Agent XB,
-			 certificate B KB|} : set evs |]
-          ==> Says A B {|certificate A (pubK A),
-			 Crypt KB (Nonce M)|}
+             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
+	       : set evs |]
+          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
                 # evs  :  tls"
 
     CertVerify
 	(*The optional CERTIFICATE VERIFY message contains the specific
-          components listed in the security analysis, Appendix F.1.1.2.
-          By checking the signature, B is assured of A's existence:
-          the only use of A's certificate.*)
+          components listed in the security analysis, Appendix F.1.1.2;
+          it also contains the pre-master-secret.  Checking the signature,
+          which is the only use of A's certificate, assures B of A's presence*)
          "[| evs: tls;  A ~= B;  
-             Says B' A {|Nonce NA, Nonce NB, Agent XB,
-			 certificate B KB|} : set evs |]
+             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
+	       : set evs;
+	     Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
+	       : set evs |]
           ==> Says A B (Crypt (priK A)
-			(Hash{|Nonce NB,
-	 		       certificate B KB|}))
+			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
                 # evs  :  tls"
 
 	(*Finally come the FINISHED messages, confirming XA and XB among
@@ -122,10 +115,10 @@
     ClientFinished
          "[| evs: tls;  A ~= B;
 	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
-             Says B' A {|Nonce NA, Nonce NB, Agent XB, 
-			 certificate B KB|} : set evs;
-             Says A  B {|certificate A (pubK A),
-		         Crypt KB (Nonce M)|} : set evs |]
+             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
+	       : set evs;
+             Says A  B {|certificate A (pubK A), Crypt KB (Nonce M)|}
+	       : set evs |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
 			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
 			       Nonce NA, Agent XA,