--- a/src/HOL/Auth/TLS.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/TLS.thy Fri Apr 25 11:18:14 2003 +0200
@@ -43,7 +43,11 @@
constdefs
certificate :: "[agent,key] => msg"
- "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+ "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
+
+text{*TLS apparently does not require separate keypairs for encryption and
+signature. Therefore, we formalize signature as encryption using the
+private encryption key.*}
datatype role = ClientRole | ServerRole
@@ -66,67 +70,72 @@
"serverK X" == "sessionK(X, ServerRole)"
axioms
- (*the pseudo-random function is collision-free*)
+ --{*the pseudo-random function is collision-free*}
inj_PRF: "inj PRF"
- (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
+ --{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
inj_sessionK: "inj sessionK"
- (*sessionK makes symmetric keys*)
+ --{*sessionK makes symmetric keys*}
isSym_sessionK: "sessionK nonces \<in> symKeys"
+ --{*sessionK never clashes with a long-term symmetric key
+ (they don't exist in TLS anyway)*}
+ sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A"
+
consts tls :: "event list set"
inductive tls
intros
- Nil: (*Initial trace is empty*)
+ Nil: --{*The initial, empty trace*}
"[] \<in> tls"
- Fake: (*The spy, an active attacker, MAY say anything he CAN say.*)
+ Fake: --{*The Spy may say anything he can say. The sender field is correct,
+ but agents don't use that information.*}
"[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |]
==> Says Spy B X # evsf \<in> tls"
- SpyKeys: (*The spy may apply PRF & sessionK to available nonces*)
+ SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
"[| evsSK \<in> tls;
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
==> Notes Spy {| Nonce (PRF(M,NA,NB)),
Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
ClientHello:
- (*(7.4.1.2)
+ --{*(7.4.1.2)
PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
It is uninterpreted but will be confirmed in the FINISHED messages.
NA is CLIENT RANDOM, while SID is SESSION_ID.
UNIX TIME is omitted because the protocol doesn't use it.
May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
- while MASTER SECRET is 48 bytes*)
+ while MASTER SECRET is 48 bytes*}
"[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |]
==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
# evsCH \<in> tls"
ServerHello:
- (*7.4.1.3 of the TLS Internet-Draft
+ --{*7.4.1.3 of the TLS Internet-Draft
PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
SERVER CERTIFICATE (7.4.2) is always present.
- CERTIFICATE_REQUEST (7.4.4) is implied.*)
+ CERTIFICATE_REQUEST (7.4.4) is implied.*}
"[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsSH |]
==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls"
Certificate:
- (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
+ --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*}
"evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls"
ClientKeyExch:
- (*CLIENT KEY EXCHANGE (7.4.7).
+ --{*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 \<notin> 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). *)
+ (see REMARK at top). *}
"[| evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF;
Says B' A (certificate B KB) \<in> set evsCX |]
==> Says A B (Crypt KB (Nonce PMS))
@@ -134,28 +143,28 @@
# evsCX \<in> tls"
CertVerify:
- (*The optional Certificate Verify (7.4.8) message contains the
+ --{*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*)
+ assures B of A's presence*}
"[| evsCV \<in> tls;
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV;
Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |]
==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
# evsCV \<in> tls"
- (*Finally come the FINISHED messages (7.4.8), confirming PA and PB
+ --{*Finally come the FINISHED messages (7.4.8), confirming PA and PB
among other things. The master-secret is PRF(PMS,NA,NB).
- Either party may send its message first.*)
+ Either party may send its message first.*}
ClientFinished:
- (*The occurrence of Notes A {|Agent B, Nonce PMS|} 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 PMS and could not send ClientFinished. One
could simply put A\<noteq>Spy into the rule, but one should not
- expect the spy to be well-behaved.*)
+ expect the spy to be well-behaved.*}
"[| evsCF \<in> tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsCF;
@@ -169,8 +178,8 @@
# evsCF \<in> tls"
ServerFinished:
- (*Keeping A' and A'' distinct means B cannot even check that the
- two messages originate from the same source. *)
+ --{*Keeping A' and A'' distinct means B cannot even check that the
+ two messages originate from the same source. *}
"[| evsSF \<in> tls;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
\<in> set evsSF;
@@ -184,10 +193,10 @@
# evsSF \<in> tls"
ClientAccepts:
- (*Having transmitted ClientFinished and received an identical
+ --{*Having transmitted ClientFinished and received an identical
message encrypted with serverK, the client stores the parameters
needed to resume this session. The "Notes A ..." premise is
- used to prove Notes_master_imp_Crypt_PMS.*)
+ used to prove Notes_master_imp_Crypt_PMS.*}
"[| evsCA \<in> tls;
Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
M = PRF(PMS,NA,NB);
@@ -200,10 +209,10 @@
Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls"
ServerAccepts:
- (*Having transmitted ServerFinished and received an identical
+ --{*Having transmitted ServerFinished and received an identical
message encrypted with clientK, the server stores the parameters
needed to resume this session. The "Says A'' B ..." premise is
- used to prove Notes_master_imp_Crypt_PMS.*)
+ used to prove Notes_master_imp_Crypt_PMS.*}
"[| evsSA \<in> tls;
A \<noteq> B;
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
@@ -217,8 +226,8 @@
Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls"
ClientResume:
- (*If A recalls the SESSION_ID, then she sends 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 \<in> tls;
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
@@ -230,8 +239,8 @@
# evsCR \<in> tls"
ServerResume:
- (*Resumption (7.3): If B finds the SESSION_ID then he can send
- a FINISHED message using the recovered MASTER SECRET*)
+ --{*Resumption (7.3): If B finds the SESSION_ID then he can send
+ a FINISHED message using the recovered MASTER SECRET*}
"[| evsSR \<in> tls;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
@@ -243,10 +252,10 @@
\<in> tls"
Oops:
- (*The most plausible compromise is of an old session key. Losing
+ --{*The most plausible compromise is of an old session key. Losing
the MASTER SECRET or PREMASTER SECRET is more serious but
rather unlikely. The assumption A \<noteq> Spy is essential: otherwise
- the Spy could learn session keys merely by replaying messages!*)
+ the Spy could learn session keys merely by replaying messages!*}
"[| evso \<in> tls; A \<noteq> Spy;
Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \<in> tls"
@@ -272,10 +281,10 @@
declare Fake_parts_insert_in_Un [dest]
-(*Automatically unfold the definition of "certificate"*)
+text{*Automatically unfold the definition of "certificate"*}
declare certificate_def [simp]
-(*Injectiveness of key-generating functions*)
+text{*Injectiveness of key-generating functions*}
declare inj_PRF [THEN inj_eq, iff]
declare inj_sessionK [THEN inj_eq, iff]
declare isSym_sessionK [simp]
@@ -283,12 +292,12 @@
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
-lemma pubK_neq_sessionK [iff]: "pubK A \<noteq> sessionK arg"
+lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg"
by (simp add: symKeys_neq_imp_neq)
declare pubK_neq_sessionK [THEN not_sym, iff]
-lemma priK_neq_sessionK [iff]: "priK A \<noteq> sessionK arg"
+lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg"
by (simp add: symKeys_neq_imp_neq)
declare priK_neq_sessionK [THEN not_sym, iff]
@@ -296,10 +305,10 @@
lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK
-(**** Protocol Proofs ****)
+subsection{*Protocol Proofs*}
-(*Possibility properties state that some traces run the protocol to the end.
- Four paths and 12 rules are considered.*)
+text{*Possibility properties state that some traces run the protocol to the
+end. Four paths and 12 rules are considered.*}
(** These proofs assume that the Nonce_supply nonces
@@ -309,7 +318,7 @@
**)
-(*Possibility property ending with ClientAccepts.*)
+text{*Possibility property ending with ClientAccepts.*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID M. \<exists>evs \<in> tls.
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
@@ -322,7 +331,7 @@
done
-(*And one for ServerAccepts. Either FINISHED message may come first.*)
+text{*And one for ServerAccepts. Either FINISHED message may come first.*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
@@ -335,7 +344,7 @@
done
-(*Another one, for CertVerify (which is optional)*)
+text{*Another one, for CertVerify (which is optional)*}
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>NB PMS. \<exists>evs \<in> tls.
Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
@@ -348,8 +357,8 @@
done
-(*Another one, for session resumption (both ServerResume and ClientResume).
- NO tls.Nil here: we refer to a previous session, not the empty trace.*)
+text{*Another one, for session resumption (both ServerResume and ClientResume).
+ NO tls.Nil here: we refer to a previous session, not the empty trace.*}
lemma "[| evs0 \<in> tls;
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
@@ -368,41 +377,30 @@
done
-(**** Inductive proofs about tls ****)
-
+subsection{*Inductive proofs about tls*}
-(*Induction for regularity theorems. If induction formula has the form
- X \<notin> analz (spies evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (spies evs))
-fun parts_induct_tac i =
- etac tls.induct i
- THEN REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN Force_tac i THEN
- ALLGOALS Asm_simp_tac
-*)
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees a good agent's private key!*)
+text{*Spy never sees a good agent's private key!*}
lemma Spy_see_priK [simp]:
- "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule tls.induct, force, simp_all, blast)
-done
+ "evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
+by (erule tls.induct, force, simp_all, blast)
lemma Spy_analz_priK [simp]:
- "evs \<in> tls ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+ "evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
lemma Spy_see_priK_D [dest!]:
- "[|Key (priK A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad"
+ "[|Key (privateKey b A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad"
by (blast dest: Spy_see_priK)
-(*This lemma says that no false certificates exist. One might extend the
+text{*This lemma says that no false certificates exist. One might extend the
model to include bogus certificates for the agents, but there seems
little point in doing so: the loss of their private keys is a worse
- breach of security.*)
+ breach of security.*}
lemma certificate_valid:
"[| certificate B KB \<in> parts (spies evs); evs \<in> tls |] ==> KB = pubK B"
apply (erule rev_mp)
@@ -412,7 +410,7 @@
lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
-(*** Properties of items found in Notes ***)
+subsubsection{*Properties of items found in Notes*}
lemma Notes_Crypt_parts_spies:
"[| Notes A {|Agent B, X|} \<in> set evs; evs \<in> tls |]
@@ -423,34 +421,34 @@
apply (blast intro: parts_insertI)
done
-(*C may be either A or B*)
+text{*C may be either A or B*}
lemma Notes_master_imp_Crypt_PMS:
"[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
evs \<in> tls |]
==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*Client, Server Accept*)
+txt{*Client, Server Accept*}
apply (blast dest!: Notes_Crypt_parts_spies)+
done
-(*Compared with the theorem above, both premise and conclusion are stronger*)
+text{*Compared with the theorem above, both premise and conclusion are stronger*}
lemma Notes_master_imp_Notes_PMS:
"[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
evs \<in> tls |]
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*ServerAccepts*)
+txt{*ServerAccepts*}
apply blast
done
-(*** Protocol goal: if B receives CertVerify, then A sent it ***)
+subsubsection{*Protocol goal: if B receives CertVerify, then A sent it*}
-(*B can check A's signature if he has received A's certificate.*)
+text{*B can check A's signature if he has received A's certificate.*}
lemma TrustCertVerify_lemma:
"[| X \<in> parts (spies evs);
X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
@@ -460,7 +458,7 @@
apply (erule tls.induct, force, simp_all, blast)
done
-(*Final version: B checks X using the distributed KA instead of priK A*)
+text{*Final version: B checks X using the distributed KA instead of priK A*}
lemma TrustCertVerify:
"[| X \<in> parts (spies evs);
X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
@@ -470,7 +468,7 @@
by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)
-(*If CertVerify is present then A has chosen PMS.*)
+text{*If CertVerify is present then A has chosen PMS.*}
lemma UseCertVerify_lemma:
"[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
evs \<in> tls; A \<notin> bad |]
@@ -479,7 +477,7 @@
apply (erule tls.induct, force, simp_all, blast)
done
-(*Final version using the distributed KA instead of priK A*)
+text{*Final version using the distributed KA instead of priK A*}
lemma UseCertVerify:
"[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
\<in> parts (spies evs);
@@ -492,7 +490,7 @@
lemma no_Notes_A_PRF [simp]:
"evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
apply (erule tls.induct, force, simp_all)
-(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
+txt{*ClientKeyExch: PMS is assumed to differ from any PRF.*}
apply blast
done
@@ -502,18 +500,18 @@
==> Nonce PMS \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*Easy, e.g. by freshness*)
+txt{*Easy, e.g. by freshness*}
apply (blast dest: Notes_Crypt_parts_spies)+
done
-(*** Unicity results for PMS, the pre-master-secret ***)
+subsubsection{*Unicity results for PMS, the pre-master-secret*}
-(*PMS determines B.*)
+text{*PMS determines B.*}
lemma Crypt_unique_PMS:
"[| Crypt(pubK B) (Nonce PMS) \<in> parts (spies evs);
Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs);
@@ -522,7 +520,7 @@
==> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
-(*Fake, ClientKeyExch*)
+txt{*Fake, ClientKeyExch*}
apply blast+
done
@@ -533,7 +531,7 @@
determines B alone, and only if PMS is secret.
**)
-(*In A's internal Note, PMS determines A and B.*)
+text{*In A's internal Note, PMS determines A and B.*}
lemma Notes_unique_PMS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
@@ -541,15 +539,15 @@
==> A=A' & B=B'"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: Notes_Crypt_parts_spies)
done
-(**** Secrecy Theorems ****)
+subsection{*Secrecy Theorems*}
-(*Key compromise lemma needed to prove analz_image_keys.
- No collection of keys can help the spy get new private keys.*)
+text{*Key compromise lemma needed to prove analz_image_keys.
+ No collection of keys can help the spy get new private keys.*}
lemma analz_image_priK [rule_format]:
"evs \<in> tls
==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) =
@@ -559,18 +557,18 @@
del: image_insert
add: image_Un [THEN sym]
insert_Key_image Un_assoc [THEN sym])
-(*Fake*)
+txt{*Fake*}
apply spy_analz
done
-(*slightly speeds up the big simplification below*)
+text{*slightly speeds up the big simplification below*}
lemma range_sessionkeys_not_priK:
"KK <= range sessionK ==> priK B \<notin> KK"
by blast
-(*Lemma for the trivial direction of the if-and-only-if*)
+text{*Lemma for the trivial direction of the if-and-only-if*}
lemma analz_image_keys_lemma:
"(X \<in> analz (G Un H)) --> (X \<in> analz H) ==>
(X \<in> analz (G Un H)) = (X \<in> analz H)"
@@ -595,11 +593,11 @@
insert_Key_singleton
range_sessionkeys_not_priK analz_image_priK)
apply (simp_all add: insert_absorb)
-(*Fake*)
+txt{*Fake*}
apply spy_analz
done
-(*Knowing some session keys is no help in getting new nonces*)
+text{*Knowing some session keys is no help in getting new nonces*}
lemma analz_insert_key [simp]:
"evs \<in> tls ==>
(Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
@@ -608,28 +606,28 @@
add: insert_Key_singleton analz_image_keys)
-(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
+subsubsection{*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.
+text{*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.*)
+ THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*}
lemma PMS_lemma:
"[| Nonce PMS \<notin> parts (spies evs);
K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
evs \<in> tls |]
==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
apply (erule rev_mp, erule ssubst)
-apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
+apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
-(*SpyKeys*)
+txt{*SpyKeys*}
apply blast
-(*Many others*)
+txt{*Many others*}
apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+
done
@@ -645,11 +643,11 @@
==> Nonce PMS \<in> parts (spies evs)"
by (blast dest: PMS_lemma)
-(*Write keys are never sent if M (MASTER SECRET) is secure.
+text{*Write keys are never sent if M (MASTER SECRET) is secure.
Converse fails; betraying M doesn't force the keys to be sent!
The strong Oops condition can be weakened later by unicity reasoning,
with some effort.
- NO LONGER USED: see clientK_not_spied and serverK_not_spied*)
+ NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
lemma sessionK_not_spied:
"[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
Nonce M \<notin> analz (spies evs); evs \<in> tls |]
@@ -657,57 +655,57 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra)
apply (force, simp_all (no_asm_simp))
-(*Fake, SpyKeys*)
+txt{*Fake, SpyKeys*}
apply blast+
done
-(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
+text{*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*}
lemma Spy_not_see_PMS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce PMS \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*SpyKeys*)
+txt{*SpyKeys*}
apply force
apply (simp_all add: insert_absorb)
-(*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*)
+txt{*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*}
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
-(*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*)
+txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
apply force+
done
-(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
- will stay secret.*)
+text{*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
+ will stay secret.*}
lemma Spy_not_see_MS:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
+txt{*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*}
apply (blast dest!: Spy_not_see_PMS)
apply (simp_all add: insert_absorb)
-(*ClientAccepts and ServerAccepts: because PMS was already visible;
- others, freshness etc.*)
+txt{*ClientAccepts and ServerAccepts: because PMS was already visible;
+ others, freshness etc.*}
apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS
Notes_imp_knows_Spy [THEN analz.Inj])+
done
-(*** Weakening the Oops conditions for leakage of clientK ***)
+subsubsection{*Weakening the Oops conditions for leakage of clientK*}
-(*If A created PMS then nobody else (except the Spy in replays)
- would send a message using a clientK generated from that PMS.*)
+text{*If A created PMS then nobody else (except the Spy in replays)
+ would send a message using a clientK generated from that PMS.*}
lemma Says_clientK_unique:
"[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
Notes A {|Agent B, Nonce PMS|} \<in> set evs;
@@ -716,16 +714,16 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ClientFinished, ClientResume: by unicity of PMS*)
+txt{*ClientFinished, ClientResume: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Notes_PMS
intro: Notes_unique_PMS [THEN conjunct1])+
done
-(*If A created PMS and has not leaked her clientK to the Spy,
- then it is completely secure: not even in parts!*)
+text{*If A created PMS and has not leaked her clientK to the Spy,
+ then it is completely secure: not even in parts!*}
lemma clientK_not_spied:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
@@ -735,21 +733,21 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply blast
-(*SpyKeys*)
+txt{*SpyKeys*}
apply (blast dest!: Spy_not_see_MS)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_sessionK_not_spied)
-(*Oops*)
+txt{*Oops*}
apply (blast intro: Says_clientK_unique)
done
-(*** Weakening the Oops conditions for leakage of serverK ***)
+subsubsection{*Weakening the Oops conditions for leakage of serverK*}
-(*If A created PMS for B, then nobody other than B or the Spy would
- send a message using a serverK generated from that PMS.*)
+text{*If A created PMS for B, then nobody other than B or the Spy would
+ send a message using a serverK generated from that PMS.*}
lemma Says_serverK_unique:
"[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
Notes A {|Agent B, Nonce PMS|} \<in> set evs;
@@ -758,16 +756,16 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ServerResume, ServerFinished: by unicity of PMS*)
+txt{*ServerResume, ServerFinished: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Crypt_PMS
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done
-(*If A created PMS for B, and B has not leaked his serverK to the Spy,
- then it is completely secure: not even in parts!*)
+text{*If A created PMS for B, and B has not leaked his serverK to the Spy,
+ then it is completely secure: not even in parts!*}
lemma serverK_not_spied:
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
@@ -776,23 +774,23 @@
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake*)
+txt{*Fake*}
apply blast
-(*SpyKeys*)
+txt{*SpyKeys*}
apply (blast dest!: Spy_not_see_MS)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_sessionK_not_spied)
-(*Oops*)
+txt{*Oops*}
apply (blast intro: Says_serverK_unique)
done
-(*** Protocol goals: if A receives ServerFinished, then B is present
+subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
and has used the quoted values PA, PB, etc. Note that it is up to A
to compare PA with what she originally sent.
***)
-(*The mention of her name (A) in X assures A that B knows who she is.*)
+text{*The mention of her name (A) in X assures A that B knows who she is.*}
lemma TrustServerFinished [rule_format]:
"[| X = Crypt (serverK(Na,Nb,M))
(Hash{|Number SID, Nonce M,
@@ -806,17 +804,17 @@
apply (erule ssubst)+
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: serverK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
done
-(*This version refers not to ServerFinished but to any message from B.
+text{*This version refers not to ServerFinished but to any message from B.
We don't assume B has received CertVerify, 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 identity with PMS, then we could replace A' by A below.*)
+ to bind A's identity with PMS, then we could replace A' by A below.*}
lemma TrustServerMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
@@ -826,21 +824,22 @@
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp) add: ex_disj_distrib)
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: serverK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ServerResume, ServerFinished: by unicity of PMS*)
+txt{*ServerResume, ServerFinished: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Crypt_PMS
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done
-(*** Protocol goal: if B receives any message encrypted with clientK
- then A has sent it, ASSUMING that A chose PMS. Authentication is
+subsubsection{*Protocol goal: if B receives any message encrypted with clientK
+ then A has sent it*}
+
+text{*ASSUMING that A chose PMS. Authentication is
assumed here; B cannot verify it. But if the message is
- ClientFinished, then B can then check the quoted values PA, PB, etc.
-***)
+ ClientFinished, then B can then check the quoted values PA, PB, etc.*}
lemma TrustClientMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
@@ -851,19 +850,19 @@
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
-(*Fake: the Spy doesn't have the critical session key!*)
+txt{*Fake: the Spy doesn't have the critical session key!*}
apply (blast dest: clientK_not_spied)
-(*ClientKeyExch*)
+txt{*ClientKeyExch*}
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
-(*ClientFinished, ClientResume: by unicity of PMS*)
+txt{*ClientFinished, ClientResume: by unicity of PMS*}
apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+
done
-(*** Protocol goal: if B receives ClientFinished, and if B is able to
+subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
check a CertVerify from A, then A has used the quoted
values PA, PB, etc. Even this one requires A to be uncompromised.
- ***)
+*}
lemma AuthClientFinished:
"[| M = PRF(PMS,NA,NB);
Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;