--- a/src/HOL/Auth/TLS.ML Fri Sep 12 10:45:51 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Tue Sep 16 13:32:22 1997 +0200
@@ -48,7 +48,7 @@
(*Injectiveness of key-generating functions*)
-AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
+AddIffs [inj_PRF RS inj_eq, inj_clientK RS inj_eq, inj_serverK RS inj_eq];
(* invKey(clientK x) = clientK x and similarly for serverK*)
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
@@ -97,43 +97,56 @@
(*A "possibility property": there are traces that reach the end.
This protocol has three end points and six messages to consider.*)
+
+(** These proofs make the further assumption 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.
+**)
+
+
+
(*Possibility property ending with ServerFinished.*)
goal thy
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
-\ Says B A (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)|})) \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
+\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \
+\ Says B A (Crypt (serverK(NA,NB,M)) \
+\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\ Nonce NB, Number XB, Agent B|})) \
\ : 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) 2);
by possibility_tac;
+by (REPEAT (Blast_tac 1));
result();
(*And one for ClientFinished. Either FINISHED message may come first.*)
goal thy
- "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
+\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \
\ Says A B (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|})) : set evs";
+\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\ Nonce NB, Number XB, Agent B|})) : 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) 2);
by possibility_tac;
+by (REPEAT (Blast_tac 1));
result();
(*Another one, for CertVerify (which is optional)*)
goal thy
- "!!A B. A ~= B ==> EX NB M. EX evs: tls. \
+ "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
+\ A ~= B |] ==> EX NB PMS. EX evs: tls. \
\ Says A B (Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
+\ (Hash{|Nonce NB, certificate B (pubK 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 possibility_tac;
+by (REPEAT (Blast_tac 1));
result();
@@ -211,40 +224,33 @@
ClientCertKeyEx_tac (i+6) THEN (*CertVerify*)
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*)
ALLGOALS (asm_simp_tac
- (!simpset addsimps [not_parts_not_analz]
+ (!simpset addcongs [if_weak_cong]
setloop split_tac [expand_if])) THEN
(*Remove instances of pubK B: the Spy already knows all public keys.
Combining the two simplifier calls makes them run extremely slowly.*)
ALLGOALS (asm_simp_tac
- (!simpset addsimps [insert_absorb]
+ (!simpset addcongs [if_weak_cong]
+ addsimps [insert_absorb]
setloop split_tac [expand_if]));
(*** Hashing of nonces ***)
-(*Every Nonce that's hashed is already in past traffic. *)
-goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees Spy evs); \
-\ evs : tls |] \
-\ ==> Nonce N : parts (sees Spy evs)";
+(*Every Nonce that's hashed is already in past traffic.
+ This event occurs in CERTIFICATE VERIFY*)
+goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs); \
+\ NB ~: range PRF; evs : tls |] \
+\ ==> Nonce NB : parts (sees Spy evs)";
+by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
by (Fake_parts_insert_tac 1);
-by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
- addSEs partsEs) 1);
-qed "Hash_imp_Nonce1";
-
-(*Lemma needed to prove Hash_Hash_imp_Nonce*)
-goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|} \
-\ : parts (sees Spy evs); \
-\ evs : tls |] \
-\ ==> Nonce M : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
-by (Fake_parts_insert_tac 1);
-qed "Hash_imp_Nonce2";
-AddSDs [Hash_imp_Nonce2];
+(*FINISHED messages are trivial because M : range PRF*)
+by (REPEAT (Blast_tac 2));
+(*CERTIFICATE VERIFY is the only interesting case*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+qed "Hash_Nonce_CV";
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \
@@ -255,38 +261,25 @@
qed "Notes_Crypt_parts_sees";
-(*NEEDED??*)
-goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \
-\ : parts (sees Spy evs); \
-\ evs : tls |] \
-\ ==> Nonce M : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
-by (Fake_parts_insert_tac 1);
-by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy RS parts.Inj]
- addSEs partsEs) 1));
-qed "Hash_Hash_imp_Nonce";
-
-
-(*NEEDED??
- Every Nonce that's hashed is already in past traffic.
- This general formulation is tricky to prove and hard to use, since the
- 2nd premise is typically proved by simplification.*)
-goal thy "!!evs. [| Hash X : parts (sees Spy evs); \
-\ Nonce N : parts {X}; evs : tls |] \
-\ ==> Nonce N : parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy RS parts.Inj]
- addSEs partsEs) 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
-by (Fake_parts_insert_tac 1);
-(*CertVerify, ClientFinished, ServerFinished (?)*)
-by (REPEAT (Blast_tac 1));
-qed "Hash_imp_Nonce_seen";
+(*****************
+ (*NEEDED? TRUE???
+ Every Nonce that's hashed is already in past traffic.
+ This general formulation is tricky to prove and hard to use, since the
+ 2nd premise is typically proved by simplification.*)
+ goal thy "!!evs. [| Hash X : parts (sees Spy evs); \
+ \ Nonce N : parts {X}; evs : tls |] \
+ \ ==> Nonce N : parts (sees Spy evs)";
+ by (etac rev_mp 1);
+ by (parts_induct_tac 1);
+ by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
+ Says_imp_sees_Spy RS parts.Inj]
+ addSEs partsEs) 1);
+ by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
+ 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 ***)
@@ -297,26 +290,26 @@
assume A~:lost; otherwise, the Spy can forge A's signature.*)
goal thy
"!!evs. [| X = Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B KB, Nonce M|}); \
+\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}); \
\ evs : tls; A ~: lost; B ~= Spy |] \
-\ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \
+\ ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \
\ : set evs --> \
\ X : parts (sees Spy evs) --> Says A B X : set evs";
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_imp_Nonce1]
+by (blast_tac (!claset addSDs [Hash_Nonce_CV]
addSEs sees_Spy_partsEs) 1);
qed_spec_mp "TrustCertVerify";
-(*If CERTIFICATE VERIFY is present then A has chosen M.*)
+(*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
goal thy
- "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|}) \
+ "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|}) \
\ : parts (sees Spy evs); \
\ evs : tls; A ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs";
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
be rev_mp 1;
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -356,12 +349,11 @@
by (ClientCertKeyEx_tac 6);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac lemma));
-writeln"SLOW simplification: 50 secs!??";
+writeln"SLOW simplification: 60 secs!??";
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
- addsimps (analz_image_priK::certificate_def::
+ addsimps (analz_image_priK::certificate_def::
keys_distinct))));
-by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
by (Blast_tac 3);
@@ -372,17 +364,26 @@
qed_spec_mp "analz_image_keys";
-(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
+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.*)
+by (Blast_tac 1);
+qed "no_Notes_A_PRF";
+Addsimps [no_Notes_A_PRF];
+
+
+(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
goal thy
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Nonce M ~: analz (sees Spy evs)";
-by (analz_induct_tac 1);
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Nonce PMS ~: analz (sees Spy evs)";
+by (analz_induct_tac 1); (*47 seconds???*)
(*ClientHello*)
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
addSEs sees_Spy_partsEs) 3);
(*SpyKeys*)
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (fast_tac (!claset addss (!simpset)) 2);
(*Fake*)
by (spy_analz_tac 1);
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
@@ -390,7 +391,52 @@
addDs [Notes_Crypt_parts_sees,
impOfSubs analz_subset_parts,
Says_imp_sees_Spy RS analz.Inj]) 1));
-bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
+bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
+
+
+
+goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs); \
+\ evs : tls |] \
+\ ==> Nonce PMS : parts (sees Spy evs)";
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (Fake_parts_insert_tac 1);
+(*Client key exchange*)
+by (Blast_tac 4);
+(*Server Hello: by freshness*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
+(*Client Hello: trivial*)
+by (Blast_tac 2);
+(*SpyKeys*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+qed "MS_imp_PMS";
+AddSDs [MS_imp_PMS];
+
+
+(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
+ will stay secret.*)
+goal thy
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
+by (analz_induct_tac 1); (*47 seconds???*)
+(*ClientHello*)
+by (Blast_tac 3);
+(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (blast_tac (!claset addSDs [Spy_not_see_PMS,
+ Says_imp_sees_Spy RS analz.Inj]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+by (REPEAT (blast_tac (!claset addSEs partsEs
+ addDs [MS_imp_PMS,
+ Notes_Crypt_parts_sees,
+ impOfSubs analz_subset_parts,
+ Says_imp_sees_Spy RS analz.Inj]) 1));
+bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
+
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
@@ -398,7 +444,7 @@
(** First, some lemmas about those write keys. The proofs for serverK are
nearly identical to those for clientK. **)
-(*Lemma: those write keys are never sent if M is secure.
+(*Lemma: those 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!*)
goal thy
@@ -414,9 +460,10 @@
(*Base*)
by (Blast_tac 1);
qed "clientK_notin_parts";
-
+bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
Addsimps [clientK_notin_parts];
-AddSEs [clientK_notin_parts RSN (2, rev_notE)];
+AddSEs [clientK_in_partsE,
+ impOfSubs analz_subset_parts RS clientK_in_partsE];
goal thy
"!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
@@ -431,33 +478,35 @@
(*Base*)
by (Blast_tac 1);
qed "serverK_notin_parts";
-
+bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
Addsimps [serverK_notin_parts];
-AddSEs [serverK_notin_parts RSN (2, rev_notE)];
+AddSEs [serverK_in_partsE,
+ impOfSubs analz_subset_parts RS serverK_in_partsE];
-(*Lemma: those write keys are never used if M is fresh.
- Converse doesn't hold; betraying M doesn't force the keys to be sent!
- NOT suitable as safe elim rules.*)
+
+(*Lemma: those write 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 M ~: used evs; evs : tls |] \
-\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \
+\ ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 3);
+ addSEs sees_Spy_partsEs) 3);
by (Fake_parts_insert_tac 2);
(*Base*)
by (Blast_tac 1);
qed "Crypt_clientK_notin_parts";
-
Addsimps [Crypt_clientK_notin_parts];
AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
goal thy
- "!!evs. [| Nonce M ~: used evs; evs : tls |] \
-\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \
+\ ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
@@ -481,54 +530,54 @@
qed "A_Crypt_pubB";
-(*** Unicity results for M, the pre-master-secret ***)
+(*** Unicity results for PMS, the pre-master-secret ***)
-(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
+(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
+ "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \
\ ==> EX B'. ALL B. \
-\ Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'";
+\ Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
(*ClientCertKeyEx*)
by (ClientCertKeyEx_tac 1);
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-by (expand_case_tac "M = ?y" 1 THEN
+by (expand_case_tac "PMS = ?y" 1 THEN
blast_tac (!claset addSEs partsEs) 1);
val lemma = result();
goal thy
- "!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees Spy evs); \
-\ Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \
-\ Nonce M ~: analz (sees Spy evs); \
+ "!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (sees Spy evs); \
+\ Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
+\ Nonce PMS ~: analz (sees Spy evs); \
\ evs : tls |] \
\ ==> B=B'";
by (prove_unique_tac lemma 1);
-qed "unique_M";
+qed "unique_PMS";
-(*In A's note to herself, M determines A and B.*)
+(*In A's note to herself, PMS determines A and B.*)
goal thy
- "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
+ "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \
\ ==> EX A' B'. ALL A B. \
-\ Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
-by (expand_case_tac "M = ?y" 1 THEN
+(*ClientCertKeyEx: 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_sees] addSEs partsEs) 1);
val lemma = result();
goal thy
- "!!evs. [| Notes A {|Agent B, Nonce M|} : set evs; \
-\ Notes A' {|Agent B', Nonce M|} : set evs; \
-\ Nonce M ~: analz (sees Spy evs); \
+ "!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \
+\ Notes A' {|Agent B', Nonce PMS|} : set evs; \
+\ Nonce PMS ~: analz (sees Spy evs); \
\ evs : tls |] \
\ ==> A=A' & B=B'";
by (prove_unique_tac lemma 1);
-qed "Notes_unique_M";
+qed "Notes_unique_PMS";
@@ -539,20 +588,20 @@
(*The mention of her name (A) in X assumes A that B knows who she is.*)
goal thy
- "!!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)|}); \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
+\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\ Nonce NB, Number XB, Agent B|}); \
+\ M = PRF(PMS,NA,NB); \
\ evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ X : parts (sees Spy evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1);
-by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
by (REPEAT (rtac impI 1));
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
+by (subgoal_tac
+ "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
qed_spec_mp "TrustServerFinished";
@@ -562,56 +611,60 @@
We don't assume B has received CERTIFICATE VERIFY, and an intruder could
have changed A's identity in all other messages, so we can't be sure
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented
- to bind A's identify with M, then we could replace A' by A below.*)
+ to bind A's identity with M, then we could replace A' by A below.*)
goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Crypt (serverK(NA,NB,M)) Y : parts (sees Spy evs) --> \
-\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost; \
+\ M = PRF(PMS,NA,NB) |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs) --> \
+\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
+by (hyp_subst_tac 1);
by (analz_induct_tac 1);
by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
+by (subgoal_tac
+ "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
(*ServerFinished. If the message is old then apply induction hypothesis...*)
by (rtac conjI 1 THEN Blast_tac 2);
-(*...otherwise delete induction hyp and use unicity of M.*)
+(*...otherwise delete induction hyp and use unicity of PMS.*)
by (thin_tac "?PP-->?QQ" 1);
by (Step_tac 1);
-by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
+by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
addDs [Notes_Crypt_parts_sees,
Says_imp_sees_Spy RS parts.Inj,
- unique_M]) 1);
+ unique_PMS]) 1);
qed_spec_mp "TrustServerMsg";
(*** Protocol goal: if B receives any message encrypted with clientK
- then A has sent it, ASSUMING that A chose M. Authentication is
+ then A has sent it, ASSUMING that A chose PMS. Authentication is
assumed here; B cannot verify it. But if the message is
CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
***)
goal thy
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \
-\ Crypt (clientK(NA,NB,M)) Y : parts (sees Spy evs) --> \
-\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) --> \
+\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
by (analz_induct_tac 1);
by (REPEAT_FIRST (rtac impI));
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret,
+by (subgoal_tac
+ "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
(*ClientFinished. If the message is old then apply induction hypothesis...*)
by (step_tac (!claset delrules [conjI]) 1);
-by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
-by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
+by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
+by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
- addDs [Notes_unique_M]) 1);
+ addDs [Notes_unique_PMS]) 1);
qed_spec_mp "TrustClientMsg";
@@ -620,14 +673,14 @@
values XA, XB, etc. Even this one requires A to be uncompromised.
***)
goal thy
- "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs; \
-\ Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \
+ "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
+\ Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \
\ : set evs; \
\ Says A'' B (Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) \
+\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) \
\ : set evs; \
\ evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
+\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "AuthClientFinished";
--- a/src/HOL/Auth/TLS.thy Fri Sep 12 10:45:51 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 16 13:32:22 1997 +0200
@@ -4,6 +4,12 @@
Copyright 1997 University of Cambridge
Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
+This protocol is essentially the same as SSL 3.0.
+
+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. Section numbers below refer
+to that memo.
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
@@ -15,18 +21,14 @@
The model assumes that no fraudulent certificates are present, but it does
assume that some private keys are to the spy.
-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
-
-NOTE. The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
+REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
CertVerify, ClientFinished to record that A knows M. It is a note from A to
herself. Nobody else can see it. In ClientCertKeyEx, the Spy can substitute
his own certificate for A's, but he cannot replace A's note by one for himself.
-The note is needed because of a weakness in the public-key model. Each
+The Note event avoids a weakness in the public-key model. Each
agent's state is recorded as the trace of messages. When the true client (A)
-invents M, he encrypts M with B's public key before sending it. The model
+invents PMS, he encrypts PMS with B's public key before sending it. The model
does not distinguish the original occurrence of such a message from a replay.
In the shared-key model, the ability to encrypt implies the ability to
@@ -36,8 +38,12 @@
TLS = Public +
consts
- (*Client, server write keys. They implicitly include the MAC secrets.*)
+ (*Pseudo-random function of Section 5*)
+ PRF :: "nat*nat*nat => nat"
+
+ (*Client, server write keys implicitly include the MAC secrets.*)
clientK, serverK :: "nat*nat*nat => key"
+
certificate :: "[agent,key] => msg"
defs
@@ -45,6 +51,8 @@
"certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
rules
+ inj_PRF "inj PRF"
+
(*clientK is collision-free and makes symmetric keys*)
inj_clientK "inj clientK"
isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*)
@@ -68,95 +76,105 @@
X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : tls"
- SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
- "[| evs: tls;
- Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
- ==> Says Spy B {| Key (clientK(NA,NB,M)),
- Key (serverK(NA,NB,M)) |} # evs : tls"
+ SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
+ "[| evsSK: tls;
+ Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
+ ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
+ Key (clientK(NA,NB,M)),
+ Key (serverK(NA,NB,M)) |} # evsSK : tls"
ClientHello
- (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+ (*(7.4.1.2)
+ XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
It is uninterpreted but will be confirmed in the FINISHED messages.
As an initial simplification, SESSION_ID is identified with NA
- and reuse of sessions is not supported.*)
- "[| evs: tls; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs : tls"
+ and reuse of sessions is not supported.
+ May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
+ while MASTER SECRET is 48 byptes (6.1)*)
+ "[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |]
+ ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH : tls"
ServerHello
- (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
- NA is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is
- implied and a SERVER CERTIFICATE is always present.*)
- "[| evs: tls; A ~= B; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
- ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
+ (*7.4.1.3 of the TLS Internet-Draft
+ XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+ NA is returned in its role as SESSION_ID.
+ SERVER CERTIFICATE (7.4.2) is always present.
+ CERTIFICATE_REQUEST (7.4.4) is implied.*)
+ "[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF;
+ Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
+ ==> Says B A {|Nonce NA, Nonce NB, Number XB,
certificate B (pubK B)|}
- # evs : tls"
+ # evsSH : tls"
ClientCertKeyEx
- (*CLIENT CERTIFICATE and KEY EXCHANGE. The client, A, chooses M,
- the pre-master-secret. She encrypts M using the supplied KB,
- which ought to be pubK B, and also with her own public key,
- to record in the trace that she knows M (see NOTE at top).*)
- "[| 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)|}
- # Notes A {|Agent B, Nonce M|}
- # evs : tls"
+ (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
+ The client, A, chooses PMS, the PREMASTER SECRET.
+ She encrypts PMS using the supplied KB, which ought to be pubK B.
+ We assume PMS ~: range PRF because a clash betweem the PMS
+ and another MASTER SECRET is highly unlikely (even though
+ both items have the same length, 48 bytes).
+ The Note event records in the trace that she knows PMS
+ (see REMARK at top).*)
+ "[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCX |]
+ ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
+ # Notes A {|Agent B, Nonce PMS|}
+ # evsCX : tls"
CertVerify
- (*The optional CERTIFICATE VERIFY message contains the specific
- 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;
- Notes A {|Agent B, Nonce M|} : set evs |]
+ (*The optional CERTIFICATE VERIFY (7.4.8) message contains the
+ specific components listed in the security analysis, F.1.1.2.
+ It adds the pre-master-secret, which is also essential!
+ Checking the signature, which is the only use of A's certificate,
+ assures B of A's presence*)
+ "[| evsCV: tls; A ~= B;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCV;
+ Notes A {|Agent B, Nonce PMS|} : set evsCV |]
==> Says A B (Crypt (priK A)
- (Hash{|Nonce NB, certificate B KB, Nonce M|}))
- # evs : tls"
+ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
+ # evsCV : tls"
- (*Finally come the FINISHED messages, confirming XA and XB among
- other things. The master-secret is the hash of NA, NB and M.
+ (*Finally come the FINISHED messages (7.4.8), confirming XA and XB
+ among other things. The master-secret is PRF(PMS,NA,NB).
Either party may sent its message first.*)
- (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the
+ (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
rule's applying when the Spy has satisfied the "Says A B" by
repaying messages sent by the true client; in that case, the
- Spy does not know M and could not sent CLIENT FINISHED. One
+ Spy does not know PMS and could not sent CLIENT FINISHED. One
could simply put A~=Spy into the rule, but one should not
expect the spy to be well-behaved.*)
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;
- Notes A {|Agent B, Nonce M|} : set evs |]
+ "[| evsCF: tls;
+ Says A B {|Agent A, Nonce NA, Number XA|} : set evsCF;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCF;
+ Notes A {|Agent B, Nonce PMS|} : set evsCF;
+ M = PRF(PMS,NA,NB) |]
==> Says A B (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|}))
- # evs : tls"
+ (Hash{|Nonce M,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|}))
+ # evsCF : tls"
(*Keeping A' and A'' distinct means B cannot even check that the
- two messages originate from the same source. B does not attempt
- to read A's encrypted "note to herself".*)
+ two messages originate from the same source. *)
ServerFinished
- "[| evs: tls; A ~= B;
- Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs;
- Says B A {|Nonce NA, Nonce NB, Agent XB,
+ "[| evsSF: tls;
+ Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSF;
+ Says B A {|Nonce NA, Nonce NB, Number XB,
certificate B (pubK B)|}
- : set evs;
- Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
- : set evs |]
+ : set evsSF;
+ Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
+ : set evsSF;
+ M = PRF(PMS,NA,NB) |]
==> Says B A (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)|}))
- # evs : tls"
+ (Hash{|Nonce M,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|}))
+ # evsSF : tls"
(**Oops message??**)