--- a/src/HOL/Auth/TLS.ML Mon Sep 29 15:39:28 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Tue Sep 30 11:03:55 1997 +0200
@@ -93,8 +93,9 @@
\ A ~= B |] ==> EX SID M. EX evs: tls. \
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
- RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2);
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
+ tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
+ tls.ClientAccepts) 2);
by possibility_tac;
by (REPEAT (Blast_tac 1));
result();
@@ -105,8 +106,9 @@
\ A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls. \
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
- RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2);
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
+ tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
+ tls.ServerAccepts) 2);
by possibility_tac;
by (REPEAT (Blast_tac 1));
result();
@@ -117,8 +119,8 @@
\ A ~= B |] ==> EX NB PMS. EX evs: tls. \
\ Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
- RS tls.CertVerify) 2);
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
+ tls.ClientKeyExch RS tls.CertVerify) 2);
by possibility_tac;
by (REPEAT (Blast_tac 1));
result();
@@ -135,7 +137,8 @@
\ Nonce NA, Number PA, Agent A, \
\ Nonce NB, Number PB, Agent B|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
+by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS
+ tls.ClientResume) 2);
by possibility_tac;
by (REPEAT (Blast_tac 1));
result();
@@ -182,8 +185,7 @@
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
-goal thy "!!A. [| Key (priK A) : parts (spies evs); \
-\ evs : tls |] ==> A:bad";
+goal thy "!!A. [| Key (priK A) : parts (spies evs); evs : tls |] ==> A:bad";
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
qed "Spy_see_priK_D";
@@ -196,25 +198,21 @@
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 (spies evs) --> KB = pubK B";
+ "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
-(*Replace key KB in ClientCertKeyEx by (pubK B) *)
-val ClientCertKeyEx_tac =
- forward_tac [Says_imp_spies RS parts.Inj RS
- parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
+(*Replace key KB in ClientKeyExch by (pubK B) *)
+val ClientKeyExch_tac =
+ forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
THEN' assume_tac
THEN' hyp_subst_tac;
fun analz_induct_tac i =
etac tls.induct i THEN
- ClientCertKeyEx_tac (i+7) THEN (*ClientFinished*)
- ClientCertKeyEx_tac (i+6) THEN (*CertVerify*)
- ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*)
+ ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(!simpset addcongs [if_weak_cong]
setloop split_tac [expand_if])) THEN
@@ -295,34 +293,48 @@
(*** Protocol goal: if B receives CertVerify, then A sent it ***)
-(*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~:bad; otherwise, the Spy can forge A's signature.*)
+(*B can check A's signature if he has received A's certificate.*)
goal thy
- "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}); \
-\ evs : tls; A ~: bad; B ~= Spy |] \
-\ ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|} \
-\ : set evs --> \
-\ X : parts (spies evs) --> Says A B X : set evs";
+ "!!evs. [| X : parts (spies evs); \
+\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \
+\ evs : tls; A ~: bad |] \
+\ ==> Says A B X : set evs";
+by (etac rev_mp 1);
by (hyp_subst_tac 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-(*ServerHello: nonce NB cannot be in X because it's fresh!*)
-by (blast_tac (!claset addSDs [Hash_Nonce_CV]
- addSEs spies_partsEs) 1);
-qed_spec_mp "TrustCertVerify";
+val lemma = result();
+
+(*Final version: B checks X using the distributed KA instead of priK A*)
+goal thy
+ "!!evs. [| X : parts (spies evs); \
+\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
+\ certificate A KA : parts (spies evs); \
+\ evs : tls; A ~: bad |] \
+\ ==> Says A B X : set evs";
+by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
+qed "TrustCertVerify";
(*If CertVerify is present then A has chosen PMS.*)
goal thy
- "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}) \
+ "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
\ : parts (spies evs); \
\ evs : tls; A ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
be rev_mp 1;
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
+val lemma = result();
+
+(*Final version using the distributed KA instead of priK A*)
+goal thy
+ "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
+\ : parts (spies evs); \
+\ certificate A KA : parts (spies evs); \
+\ evs : tls; A ~: bad |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
+by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
qed "UseCertVerify";
@@ -343,6 +355,11 @@
qed_spec_mp "analz_image_priK";
+(*slightly speeds up the big simplification below*)
+goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
+by (Blast_tac 1);
+val range_sessionkeys_not_priK = result();
+
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
"!!evs. (X : analz (G Un H)) --> (X : analz H) ==> \
@@ -350,11 +367,6 @@
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
val lemma = result();
-(*slightly speeds up the big simplification below*)
-goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
-by (Blast_tac 1);
-val range_sessionkeys_not_priK = result();
-
(** It is a mystery to me why the following formulation is actually slower
in simplification:
@@ -371,12 +383,10 @@
\ (Nonce N : analz (Key``KK Un (spies evs))) = \
\ (Nonce N : analz (spies evs))";
by (etac tls.induct 1);
-by (ClientCertKeyEx_tac 6);
+by (ClientKeyExch_tac 7);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac lemma));
-writeln"SLOW simplification: 55 secs??";
-(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
-by (ALLGOALS
+by (ALLGOALS (*23 seconds*)
(asm_simp_tac (analz_image_keys_ss
addsimps [range_sessionkeys_not_priK,
analz_image_priK, analz_insert_certificate])));
@@ -398,7 +408,7 @@
goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
by (parts_induct_tac 1);
-(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
+(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
by (Blast_tac 1);
qed "no_Notes_A_PRF";
Addsimps [no_Notes_A_PRF];
@@ -419,7 +429,7 @@
-(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
+(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
(** Some lemmas about session keys, comprising clientK and serverK **)
@@ -475,7 +485,7 @@
\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*30 seconds??*)
+by (analz_induct_tac 1); (*17 seconds*)
(*Oops*)
by (Blast_tac 4);
(*SpyKeys*)
@@ -507,8 +517,8 @@
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-(*ClientCertKeyEx*)
-by (ClientCertKeyEx_tac 1);
+(*ClientKeyExch*)
+by (ClientKeyExch_tac 1);
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
by (expand_case_tac "PMS = ?y" 1 THEN
blast_tac (!claset addSEs partsEs) 1);
@@ -536,7 +546,7 @@
\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
by (parts_induct_tac 1);
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
+(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
by (expand_case_tac "PMS = ?y" 1 THEN
blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
val lemma = result();
@@ -551,15 +561,15 @@
-(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
+(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
goal thy
"!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce PMS ~: analz (spies evs)";
-by (analz_induct_tac 1); (*30 seconds??*)
+by (analz_induct_tac 1); (*11 seconds*)
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
-by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
-(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume:
+by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
+(*ClientHello, ServerHello, ClientKeyExch, ServerResume:
mostly freshness reasoning*)
by (REPEAT (blast_tac (!claset addSEs partsEs
addDs [Notes_Crypt_parts_spies,
@@ -572,13 +582,13 @@
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
-(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
+(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
will stay secret.*)
goal thy
"!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
-by (analz_induct_tac 1); (*35 seconds*)
+by (analz_induct_tac 1); (*13 seconds*)
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS,
Says_imp_spies RS analz.Inj,
@@ -590,7 +600,7 @@
Says_imp_spies RS analz.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
-(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+(*ServerHello and ClientKeyExch: mostly freshness reasoning*)
by (REPEAT (blast_tac (!claset addSEs partsEs
addDs [Notes_Crypt_parts_spies,
impOfSubs analz_subset_parts,
@@ -607,13 +617,13 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
\ A = A'";
-by (analz_induct_tac 1); (*17 seconds*)
+by (analz_induct_tac 1); (*8 seconds*)
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
by (REPEAT
(blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
addIs [Notes_unique_PMS RS conjunct1]) 2));
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
addSDs [Says_imp_spies RS parts.Inj]) 1);
bind_thm ("Says_clientK_unique",
@@ -635,7 +645,7 @@
by (ALLGOALS Asm_simp_tac);
(*Oops*)
by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
spies_partsEs)) 1);
qed_spec_mp "clientK_Oops_ALL";
@@ -651,7 +661,7 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
\ B = B'";
-by (analz_induct_tac 1); (*17 seconds*)
+by (analz_induct_tac 1); (*9 seconds*)
by (ALLGOALS Clarify_tac);
(*ServerResume, ServerFinished: by unicity of PMS*)
by (REPEAT
@@ -661,7 +671,7 @@
addDs [Spy_not_see_PMS,
Notes_Crypt_parts_spies,
Crypt_unique_PMS]) 2));
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
addSDs [Says_imp_spies RS parts.Inj]) 1);
bind_thm ("Says_serverK_unique",
@@ -682,7 +692,7 @@
by (ALLGOALS Asm_simp_tac);
(*Oops*)
by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
spies_partsEs)) 1);
qed_spec_mp "serverK_Oops_ALL";
@@ -699,19 +709,19 @@
"!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
\ X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Nonce M, Number SID, \
-\ Nonce NA, Number PA, Agent A, \
-\ Nonce NB, Number PB, Agent B|}); \
+\ Nonce Na, Number PA, Agent A, \
+\ Nonce Nb, Number PB, Agent B|}); \
\ M = PRF(PMS,NA,NB); \
\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ X : parts (spies evs) --> Says B A X : set evs";
by (etac rev_mp 1);
by (hyp_subst_tac 1);
-by (analz_induct_tac 1); (*27 seconds*)
+by (analz_induct_tac 1); (*22 seconds*)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
(*proves ServerResume*)
by (ALLGOALS Clarify_tac);
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (fast_tac (*blast_tac gives PROOF FAILED*)
(!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
@@ -725,8 +735,8 @@
goal thy
"!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Nonce M, Number SID, \
-\ Nonce NA, Number PA, Agent A, \
-\ Nonce NB, Number PB, Agent B|}); \
+\ Nonce Na, Number PA, Agent A, \
+\ Nonce Nb, Number PB, Agent B|}); \
\ M = PRF(PMS,NA,NB); \
\ X : parts (spies evs); \
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
@@ -764,7 +774,7 @@
addDs [Spy_not_see_PMS,
Notes_Crypt_parts_spies,
Crypt_unique_PMS]) 3));
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (blast_tac
(!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
@@ -801,13 +811,13 @@
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) --> \
\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
-by (analz_induct_tac 1); (*23 seconds*)
+by (analz_induct_tac 1); (*15 seconds*)
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
by (REPEAT (blast_tac (!claset delrules [conjI]
addSDs [Notes_master_imp_Notes_PMS]
addDs [Notes_unique_PMS]) 3));
-(*ClientCertKeyEx*)
+(*ClientKeyExch*)
by (fast_tac (*blast_tac gives PROOF FAILED*)
(!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
@@ -837,9 +847,8 @@
goal thy
"!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
\ Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
-\ Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|} \
-\ : set evs; \
-\ Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
+\ certificate A KA : parts (spies evs); \
+\ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
\ : set evs; \
\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
@@ -849,5 +858,4 @@
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
-
-
+(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)