--- a/src/HOL/Auth/TLS.ML Thu Oct 02 22:54:00 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Fri Oct 03 10:32:50 1997 +0200
@@ -23,30 +23,8 @@
proof_timing:=true;
HOL_quantifiers := false;
-(** We mostly DO NOT unfold the definition of "certificate". The attached
- lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
- contexts.
-**)
-
-goalw thy [certificate_def]
- "parts (insert (certificate B KB) H) = \
-\ parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
-by (rtac refl 1);
-qed "parts_insert_certificate";
-
-goalw thy [certificate_def]
- "analz (insert (certificate B KB) H) = \
-\ analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
-by (rtac refl 1);
-qed "analz_insert_certificate";
-Addsimps [parts_insert_certificate, analz_insert_certificate];
-
-goalw thy [certificate_def]
- "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
-by (Blast_tac 1);
-qed "eq_certificate_iff";
-AddIffs [eq_certificate_iff];
-
+(*Automatically unfold the definition of "certificate"*)
+Addsimps [certificate_def];
(*Injectiveness of key-generating functions*)
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
@@ -75,15 +53,14 @@
(**** Protocol Proofs ****)
-(*A "possibility property": there are traces that reach the end.
- This protocol has three end points and six messages to consider.*)
+(*Possibility properties state that some traces run the protocol to the end.
+ Four paths and 12 rules are considered.*)
-(** These proofs make the further assumption that the Nonce_supply nonces
+(** These proofs assume that the Nonce_supply nonces
(which have the form @ N. Nonce N ~: used evs)
- lie outside the range of PRF. This assumption seems reasonable, but
- as it is needed only for the possibility theorems, it is not taken
- as an axiom.
+ lie outside the range of PRF. It seems reasonable, but as it is needed
+ only for the possibility theorems, it is not taken as an axiom.
**)
@@ -202,15 +179,17 @@
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. [| certificate B KB : parts (spies evs); evs : tls |] \
+\ ==> pubK B = KB";
+by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
+qed "certificate_valid";
(*Replace key KB in ClientKeyExch by (pubK B) *)
val ClientKeyExch_tac =
- forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
+ forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid]
THEN' assume_tac
THEN' hyp_subst_tac;
@@ -268,9 +247,9 @@
(*B can check A's signature if he has received A's certificate.*)
goal thy
- "!!evs. [| X : parts (spies evs); \
-\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \
-\ evs : tls; A ~: bad |] \
+ "!!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);
@@ -280,20 +259,20 @@
(*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 |] \
+ "!!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);
+by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
qed "TrustCertVerify";
(*If CertVerify is present then A has chosen PMS.*)
goal thy
- "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
-\ : parts (spies evs); \
-\ evs : tls; A ~: bad |] \
+ "!!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);
@@ -302,83 +281,15 @@
(*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 |] \
+ "!!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);
+by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
qed "UseCertVerify";
-(*Key compromise lemma needed to prove analz_image_keys.
- No collection of keys can help the spy get new private keys.*)
-goal thy
- "!!evs. evs : tls ==> \
-\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
-\ (priK B : KK | B : bad)";
-by (etac tls.induct 1);
-by (ALLGOALS
- (asm_simp_tac (analz_image_keys_ss
- addsimps (analz_insert_certificate::keys_distinct))));
-(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-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) ==> \
-\ (X : analz (G Un H)) = (X : analz H)";
-by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
-(** It is a mystery to me why the following formulation is actually slower
- in simplification:
-
-\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
-\ (Nonce N : analz (spies evs))";
-
-More so as it can take advantage of unconditional rewrites such as
- priK B ~: sessionK``Z
-**)
-
-goal thy
- "!!evs. evs : tls ==> \
-\ ALL KK. KK <= range sessionK --> \
-\ (Nonce N : analz (Key``KK Un (spies evs))) = \
-\ (Nonce N : analz (spies evs))";
-by (etac tls.induct 1);
-by (ClientKeyExch_tac 7);
-by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac lemma));
-by (ALLGOALS (*23 seconds*)
- (asm_simp_tac (analz_image_keys_ss
- addsimps [range_sessionkeys_not_priK,
- analz_image_priK, analz_insert_certificate])));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
-(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed_spec_mp "analz_image_keys";
-
-(*Knowing some session keys is no help in getting new nonces*)
-goal thy
- "!!evs. evs : tls ==> \
-\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \
-\ (Nonce N : analz (spies evs))";
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
-qed "analz_insert_key";
-Addsimps [analz_insert_key];
-
goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
by (parts_induct_tac 1);
(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
@@ -402,75 +313,6 @@
-(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
-
-(** Some lemmas about session keys, comprising clientK and serverK **)
-
-
-(*Lemma: session keys are never used if PMS is fresh.
- Nonces don't have to agree, allowing session resumption.
- Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
- THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
-goal thy
- "!!evs. [| Nonce PMS ~: parts (spies evs); \
-\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \
-\ evs : tls |] \
-\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
-by (etac rev_mp 1);
-by (hyp_subst_tac 1);
-by (analz_induct_tac 1);
-(*SpyKeys*)
-by (blast_tac (!claset addSEs spies_partsEs) 3);
-(*Fake*)
-by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
-by (Fake_parts_insert_tac 2);
-(** LEVEL 6 **)
-(*Oops*)
-by (fast_tac (!claset addSEs [MPair_parts]
- addDs [Says_imp_spies RS parts.Inj]
- addss (!simpset)) 6);
-by (REPEAT
- (blast_tac (!claset addSDs [Notes_Crypt_parts_spies,
- Notes_master_imp_Crypt_PMS]
- addSEs spies_partsEs) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \
-\ ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
-by (blast_tac (!claset addDs [lemma]) 1);
-qed "PMS_sessionK_not_spied";
-
-goal thy
- "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \
-\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
-by (blast_tac (!claset addDs [lemma]) 1);
-qed "PMS_Crypt_sessionK_not_spied";
-
-
-(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.
- Converse doesn't hold; betraying M doesn't force the keys to be sent!
- The strong Oops condition can be weakened later by unicity reasoning,
- with some effort.*)
-goal thy
- "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
-\ Nonce M ~: analz (spies evs); evs : tls |] \
-\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1); (*17 seconds*)
-(*Oops*)
-by (Blast_tac 4);
-(*SpyKeys*)
-by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
-(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed "sessionK_not_spied";
-Addsimps [sessionK_not_spied];
-
-
(*** Unicity results for PMS, the pre-master-secret ***)
(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
@@ -525,6 +367,144 @@
+(**** Secrecy Theorems ****)
+
+(*Key compromise lemma needed to prove analz_image_keys.
+ No collection of keys can help the spy get new private keys.*)
+goal thy
+ "!!evs. evs : tls ==> \
+\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\ (priK B : KK | B : bad)";
+by (etac tls.induct 1);
+by (ALLGOALS
+ (asm_simp_tac (analz_image_keys_ss
+ addsimps (certificate_def::keys_distinct))));
+(*Fake*)
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+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) ==> \
+\ (X : analz (G Un H)) = (X : analz H)";
+by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
+val lemma = result();
+
+(** Strangely, the following version doesn't work:
+\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
+\ (Nonce N : analz (spies evs))";
+**)
+
+goal thy
+ "!!evs. evs : tls ==> \
+\ ALL KK. KK <= range sessionK --> \
+\ (Nonce N : analz (Key``KK Un (spies evs))) = \
+\ (Nonce N : analz (spies evs))";
+by (etac tls.induct 1);
+by (ClientKeyExch_tac 7);
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac lemma));
+by (ALLGOALS (*24 seconds*)
+ (asm_simp_tac (analz_image_keys_ss
+ addsimps [range_sessionkeys_not_priK,
+ analz_image_priK, certificate_def])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
+(*Fake*)
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+qed_spec_mp "analz_image_keys";
+
+(*Knowing some session keys is no help in getting new nonces*)
+goal thy
+ "!!evs. evs : tls ==> \
+\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \
+\ (Nonce N : analz (spies evs))";
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
+qed "analz_insert_key";
+Addsimps [analz_insert_key];
+
+
+(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
+
+(** Some lemmas about session keys, comprising clientK and serverK **)
+
+
+(*Lemma: session keys are never used if PMS is fresh.
+ Nonces don't have to agree, allowing session resumption.
+ Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
+ THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
+goal thy
+ "!!evs. [| Nonce PMS ~: parts (spies evs); \
+\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \
+\ evs : tls |] \
+\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
+by (etac rev_mp 1);
+by (hyp_subst_tac 1);
+by (analz_induct_tac 1);
+(*SpyKeys*)
+by (blast_tac (!claset addSEs spies_partsEs) 3);
+(*Fake*)
+by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
+by (Fake_parts_insert_tac 2);
+(** LEVEL 6 **)
+(*Oops*)
+by (fast_tac (!claset addSEs [MPair_parts]
+ addDs [Says_imp_spies RS parts.Inj]
+ addss (!simpset)) 6);
+by (REPEAT
+ (blast_tac (!claset addSDs [Notes_Crypt_parts_spies,
+ Notes_master_imp_Crypt_PMS]
+ addSEs spies_partsEs) 1));
+val lemma = result();
+
+goal thy
+ "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \
+\ ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
+by (blast_tac (!claset addDs [lemma]) 1);
+qed "PMS_sessionK_not_spied";
+bind_thm ("PMS_sessionK_spiedE",
+ PMS_sessionK_not_spied RSN (2,rev_notE));
+
+goal thy
+ "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \
+\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
+by (blast_tac (!claset addDs [lemma]) 1);
+qed "PMS_Crypt_sessionK_not_spied";
+bind_thm ("PMS_Crypt_sessionK_spiedE",
+ PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
+
+(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.
+ Converse doesn't hold; betraying M doesn't force the keys to be sent!
+ The strong Oops condition can be weakened later by unicity reasoning,
+ with some effort.*)
+goal thy
+ "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
+\ Nonce M ~: analz (spies evs); evs : tls |] \
+\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (analz_induct_tac 1); (*17 seconds*)
+(*Oops*)
+by (Blast_tac 4);
+(*SpyKeys*)
+by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
+(*Fake*)
+by (spy_analz_tac 2);
+(*Base*)
+by (Blast_tac 1);
+qed "sessionK_not_spied";
+Addsimps [sessionK_not_spied];
+
+
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
goal thy
"!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
@@ -588,7 +568,7 @@
(blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
addIs [Notes_unique_PMS RS conjunct1]) 2));
(*ClientKeyExch*)
-by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
+by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
addSDs [Says_imp_spies RS parts.Inj]) 1);
bind_thm ("Says_clientK_unique",
result() RSN(2,rev_mp) RSN(2,rev_mp));
@@ -610,8 +590,7 @@
(*Oops*)
by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
(*ClientKeyExch*)
-by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
- spies_partsEs)) 1);
+by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
qed_spec_mp "clientK_Oops_ALL";
@@ -636,7 +615,7 @@
Notes_Crypt_parts_spies,
Crypt_unique_PMS]) 2));
(*ClientKeyExch*)
-by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
+by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
addSDs [Says_imp_spies RS parts.Inj]) 1);
bind_thm ("Says_serverK_unique",
result() RSN(2,rev_mp) RSN(2,rev_mp));
@@ -657,8 +636,7 @@
(*Oops*)
by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
(*ClientKeyExch*)
-by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
- spies_partsEs)) 1);
+by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
qed_spec_mp "serverK_Oops_ALL";
@@ -670,16 +648,15 @@
(*The mention of her name (A) in X assures A that B knows who she is.*)
goal thy
- "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
-\ X = Crypt (serverK(Na,Nb,M)) \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Number SID, Nonce M, \
\ 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);
+\ evs : tls; A ~: bad; B ~: bad |] \
+\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ X : parts (spies evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*22 seconds*)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -687,13 +664,13 @@
by (ALLGOALS Clarify_tac);
(*ClientKeyExch*)
by (fast_tac (*blast_tac gives PROOF FAILED*)
- (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+ (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
(*Final version*)
goal thy
@@ -719,13 +696,11 @@
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented
to bind A's identity with PMS, then we could replace A' by A below.*)
goal thy
- "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
-\ evs : tls; A ~: bad; B ~: bad; \
-\ M = PRF(PMS,NA,NB) |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+ "!!evs. [| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \
+\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
-by (etac rev_mp 1);
by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*20 seconds*)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -740,13 +715,13 @@
Crypt_unique_PMS]) 3));
(*ClientKeyExch*)
by (blast_tac
- (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+ (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
(*Final version*)
goal thy
@@ -758,7 +733,6 @@
\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
by (blast_tac (!claset addIs [lemma]
addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
-
qed_spec_mp "TrustServerMsg";
@@ -770,11 +744,12 @@
***)
goal thy
- "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \
-\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
-\ 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";
+ "!!evs. [| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \
+\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \
+\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
+by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*15 seconds*)
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
@@ -783,24 +758,25 @@
addDs [Notes_unique_PMS]) 3));
(*ClientKeyExch*)
by (fast_tac (*blast_tac gives PROOF FAILED*)
- (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
+ (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
(*Fake: the Spy doesn't have the critical session key!*)
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
-val lemma = normalize_thm [RSspec, RSmp] (result());
+val lemma = normalize_thm [RSmp] (result());
(*Final version*)
goal thy
- "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs); \
+ "!!evs. [| M = PRF(PMS,NA,NB); \
+\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
-\ Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs; \
+\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \
\ evs : tls; A ~: bad; B ~: bad |] \
-\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
+\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
by (blast_tac (!claset addIs [lemma]
addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
-qed_spec_mp "TrustClientMsg";
+qed "TrustClientMsg";
@@ -809,13 +785,14 @@
values PA, PB, etc. Even this one requires A to be uncompromised.
***)
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; \
+ "!!evs. [| M = PRF(PMS,NA,NB); \
+\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
+\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
\ 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";
+\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
addDs [Says_imp_spies RS parts.Inj]) 1);
qed "AuthClientFinished";