Simplified SpyKeys to use sessionK instead of clientK and serverK
Proved and used analz_insert_key, shortening scripts
--- a/src/HOL/Auth/TLS.ML Fri Sep 19 18:27:31 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Mon Sep 22 13:17:29 1997 +0200
@@ -327,11 +327,12 @@
qed "UseCertVerify";
-(*No collection of keys can help the spy get new private keys*)
+(*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)";
+\ (priK B : KK | B : bad)";
by (etac tls.induct 1);
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
@@ -355,7 +356,16 @@
by (Blast_tac 1);
val range_sessionkeys_not_priK = result();
-(*Knowing some session keys is no help in getting new nonces*)
+(** 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 --> \
@@ -378,6 +388,14 @@
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);
@@ -417,10 +435,8 @@
by (etac rev_mp 1);
by (analz_induct_tac 1); (*30 seconds??*)
(*Oops*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 4);
by (Blast_tac 4);
(*SpyKeys*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
(*Fake*)
by (spy_analz_tac 2);
@@ -533,20 +549,15 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce PMS ~: analz (spies evs)";
by (analz_induct_tac 1); (*30 seconds??*)
-(*oops*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
-(*ServerHello, ClientCertKeyEx, ServerResume: mostly freshness reasoning*)
+(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume:
+ mostly freshness reasoning*)
by (REPEAT (blast_tac (!claset addSEs partsEs
addDs [Notes_Crypt_parts_spies,
impOfSubs analz_subset_parts,
- Says_imp_spies RS analz.Inj]) 4));
-(*ClientHello*)
-by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
- addSEs spies_partsEs) 3);
+ Says_imp_spies RS analz.Inj]) 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);
@@ -571,8 +582,6 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
by (analz_induct_tac 1); (*35 seconds*)
-(*Oops*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS,
Says_imp_spies RS analz.Inj,
@@ -580,7 +589,6 @@
(*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_spies RS analz.Inj]) 2);
(*Fake*)
@@ -712,3 +720,5 @@
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
addDs [Says_imp_spies RS parts.Inj]) 1);
qed "AuthClientFinished";
+
+(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
--- a/src/HOL/Auth/TLS.thy Fri Sep 19 18:27:31 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Mon Sep 22 13:17:29 1997 +0200
@@ -66,7 +66,8 @@
rules
inj_PRF "inj PRF"
- (*sessionK is collision-free and makes symmetric keys*)
+ (*sessionK is collision-free and makes symmetric keys. Also, no clientK
+ clashes with any serverK.*)
inj_sessionK "inj sessionK"
isSym_sessionK "isSymKey (sessionK x)"
@@ -75,9 +76,6 @@
inj_serverK "inj serverK"
isSym_serverK "isSymKey (serverK x)"
- (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
- clientK_range "range clientK <= Compl (range serverK)"
-
consts tls :: event list set
inductive tls
@@ -90,12 +88,11 @@
X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : tls"
- SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
+ SpyKeys (*The spy may apply PRF & sessionK 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"
+ Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
ClientHello
(*(7.4.1.2)
@@ -196,7 +193,8 @@
ClientAccepts
(*Having transmitted ClientFinished and received an identical
message encrypted with serverK, the client stores the parameters
- needed to resume this session.*)
+ needed to resume this session. The "Notes A ..." premise is
+ used to prove Notes_master_imp_Crypt_PMS.*)
"[| evsCA: tls;
Notes A {|Agent B, Nonce PMS|} : set evsCA;
M = PRF(PMS,NA,NB);
@@ -211,7 +209,8 @@
ServerAccepts
(*Having transmitted ServerFinished and received an identical
message encrypted with clientK, the server stores the parameters
- needed to resume this session.*)
+ 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;