--- 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*)
--- a/src/HOL/Auth/TLS.thy Mon Sep 29 15:39:28 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 30 11:03:55 1997 +0200
@@ -21,9 +21,9 @@
The model assumes that no fraudulent certificates are present, but it does
assume that some private keys are to the spy.
-REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
+REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
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
+herself. Nobody else can see it. In ClientKeyExch, the Spy can substitute
his own certificate for A's, but he cannot replace A's note by one for himself.
The Note event avoids a weakness in the public-key model. Each
@@ -33,7 +33,7 @@
In the shared-key model, the ability to encrypt implies the ability to
decrypt, so the problem does not arise.
-Proofs would be simpler if ClientCertKeyEx included A's name within
+Proofs would be simpler if ClientKeyExch included A's name within
Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs
about that message (which B receives) and the stronger event
Notes A {|Agent B, Nonce PMS|}.
@@ -61,17 +61,18 @@
clientK, serverK :: "nat*nat*nat => key"
translations
- "clientK (x)" == "sessionK(x,0)"
- "serverK (x)" == "sessionK(x,1)"
+ "clientK (nonces)" == "sessionK(nonces,0)"
+ "serverK (nonces)" == "sessionK(nonces,1)"
rules
+ (*the pseudo-random function is collision-free*)
inj_PRF "inj PRF"
- (*sessionK is collision-free and makes symmetric keys. Also, no clientK
- clashes with any serverK.*)
+ (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
inj_sessionK "inj sessionK"
- isSym_sessionK "isSymKey (sessionK x)"
+ (*sessionK makes symmetric keys*)
+ isSym_sessionK "isSymKey (sessionK nonces)"
consts tls :: event list set
@@ -111,12 +112,15 @@
"[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSH |]
- ==> Says B A {|Nonce NB, Number SID, Number PB,
- certificate B (pubK B)|}
- # evsSH : tls"
+ ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH : tls"
- ClientCertKeyEx
- (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
+ Certificate
+ (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
+ "[| evsC: tls; A ~= B |]
+ ==> Says B A (certificate B (pubK B)) # evsC : tls"
+
+ ClientKeyExch
+ (*CLIENT 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
@@ -125,9 +129,9 @@
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 NB, Number SID, Number PB, certificate B KB|}
- : set evsCX |]
- ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
+ Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCX;
+ Says B'' A (certificate B KB) : set evsCX |]
+ ==> Says A B (Crypt KB (Nonce PMS))
# Notes A {|Agent B, Nonce PMS|}
# evsCX : tls"
@@ -138,8 +142,7 @@
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 NB, Number SID, Number PB, certificate B KB|}
- : set evsCV;
+ Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
Notes A {|Agent B, Nonce PMS|} : set evsCV |]
==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
# evsCV : tls"
@@ -158,8 +161,7 @@
"[| evsCF: tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsCF;
- Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
- : set evsCF;
+ Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
Notes A {|Agent B, Nonce PMS|} : set evsCF;
M = PRF(PMS,NA,NB) |]
==> Says A B (Crypt (clientK(NA,NB,M))
@@ -174,11 +176,8 @@
"[| evsSF: tls;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSF;
- Says B A {|Nonce NB, Number SID, Number PB,
- certificate B (pubK B)|}
- : set evsSF;
- Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
- : set evsSF;
+ Says B A {|Nonce NB, Number SID, Number PB|} : set evsSF;
+ Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
M = PRF(PMS,NA,NB) |]
==> Says B A (Crypt (serverK(NA,NB,M))
(Hash{|Nonce M, Number SID,
@@ -208,8 +207,7 @@
needed to resume this session. The "Says A'' B ..." premise is
used to prove Notes_master_imp_Crypt_PMS.*)
"[| evsSA: tls;
- Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
- : set evsSA;
+ Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
M = PRF(PMS,NA,NB);
X = Hash{|Nonce M, Number SID,
Nonce NA, Number PA, Agent A,
@@ -220,9 +218,8 @@
Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA : tls"
ServerResume
- (*Resumption is described in 7.3. If B finds the SESSION_ID
- then he sends HELLO and FINISHED messages, using the
- previously stored MASTER SECRET*)
+ (*Resumption (7.3): If B finds the SESSION_ID then he can send
+ a FINISHED message using the recovered MASTER SECRET*)
"[| evsSR: tls; A ~= B; Nonce NB ~: used evsSR; NB ~: range PRF;
Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
@@ -230,12 +227,12 @@
==> Says B A (Crypt (serverK(NA,NB,M))
(Hash{|Nonce M, Number SID,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|}))
- # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR : tls"
+ Nonce NB, Number PB, Agent B|})) # evsSR
+ : tls"
ClientResume
- (*If the response to ClientHello is ServerResume then send
- a FINISHED message using the new nonces and stored MASTER SECRET.*)
+ (*If A recalls the SESSION_ID, then she sends a FINISHED message
+ using the new nonces and stored MASTER SECRET.*)
"[| evsCR: tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsCR;