--- a/src/HOL/Auth/TLS.ML Tue Feb 16 10:50:35 1999 +0100
+++ b/src/HOL/Auth/TLS.ML Tue Feb 16 10:54:55 1999 +0100
@@ -215,7 +215,7 @@
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*ServerAccepts*)
-by (Fast_tac 1); (*Blast_tac's very slow here*)
+by (Fast_tac 1);
qed "Notes_master_imp_Notes_PMS";
@@ -402,7 +402,7 @@
Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
Goal "[| Nonce PMS ~: parts (spies evs); \
-\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \
+\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); \
\ evs : tls |] \
\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
by (etac rev_mp 1);
@@ -420,13 +420,13 @@
Notes_master_imp_Crypt_PMS]) 1));
val lemma = result();
-Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \
+Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \
\ evs : tls |] \
\ ==> Nonce PMS : parts (spies evs)";
by (blast_tac (claset() addDs [lemma]) 1);
qed "PMS_sessionK_not_spied";
-Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y \
+Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y \
\ : parts (spies evs); evs : tls |] \
\ ==> Nonce PMS : parts (spies evs)";
by (blast_tac (claset() addDs [lemma]) 1);
@@ -437,12 +437,12 @@
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*)
-Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
+Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),role))) ~: set evs; \
\ Nonce M ~: analz (spies evs); evs : tls |] \
-\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
+\ ==> Key (sessionK((NA,NB,M),role)) ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*7 seconds*)
+by (analz_induct_tac 1); (*5 seconds*)
(*SpyKeys*)
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
(*Fake*)
@@ -456,7 +456,7 @@
Goal "[| evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Nonce PMS ~: analz (spies evs)";
-by (analz_induct_tac 1); (*11 seconds*)
+by (analz_induct_tac 1); (*4 seconds*)
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
by (REPEAT (fast_tac (claset() addss (simpset())) 6));
(*ClientHello, ServerHello, ClientKeyExch, ServerResume:
@@ -476,7 +476,7 @@
Goal "[| 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); (*13 seconds*)
+by (analz_induct_tac 1); (*4 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,
@@ -505,7 +505,7 @@
\ ==> A = A'";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*8 seconds*)
+by (analz_induct_tac 1);
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
by (REPEAT
@@ -526,7 +526,7 @@
\ ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*17 seconds*)
+by (analz_induct_tac 1); (*4 seconds*)
(*Oops*)
by (blast_tac (claset() addIs [Says_clientK_unique]) 4);
(*ClientKeyExch*)
@@ -548,7 +548,7 @@
\ ==> B = B'";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*9 seconds*)
+by (analz_induct_tac 1);
by (ALLGOALS Clarify_tac);
(*ServerResume, ServerFinished: by unicity of PMS*)
by (REPEAT
@@ -563,13 +563,13 @@
(*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!*)
-Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs; \
+Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs; \
\ Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs; \
-\ evs : tls; A ~: bad; B ~: bad |] \
+\ A ~: bad; B ~: bad; evs : tls |] \
\ ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
-by (analz_induct_tac 1); (*6 seconds*)
+by (analz_induct_tac 1);
(*Oops*)
by (blast_tac (claset() addIs [Says_serverK_unique]) 4);
(*ClientKeyExch*)
@@ -597,7 +597,7 @@
\ 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); (*10 seconds*)
+by (analz_induct_tac 1); (*7 seconds*)
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
by (ALLGOALS Clarify_tac);
(*ClientKeyExch*)
@@ -606,7 +606,6 @@
by (blast_tac (claset() addEs [serverK_not_spied RSN (2,rev_notE)]) 1);
qed_spec_mp "TrustServerFinished";
-
(*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
@@ -618,7 +617,7 @@
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
by (hyp_subst_tac 1);
-by (analz_induct_tac 1); (*20 seconds*)
+by (analz_induct_tac 1); (*6 seconds*)
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
by (ALLGOALS Clarify_tac);
(*ServerResume, ServerFinished: by unicity of PMS*)
@@ -646,7 +645,7 @@
\ 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 (analz_induct_tac 1); (*6 seconds*)
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
by (REPEAT (blast_tac (claset() delrules [conjI]
@@ -684,3 +683,6 @@
(*08/9/97: loads in 189s (pike), after much reorganization,
back to 621s on albatross?*)
+
+(*10/2/99: loads in 139s (pike)
+ down to 433s on albatross*)
--- a/src/HOL/Auth/TLS.thy Tue Feb 16 10:50:35 1999 +0100
+++ b/src/HOL/Auth/TLS.thy Tue Feb 16 10:54:55 1999 +0100
@@ -45,6 +45,8 @@
certificate :: "[agent,key] => msg"
"certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+datatype role = ClientRole | ServerRole
+
consts
(*Pseudo-random function of Section 5*)
PRF :: "nat*nat*nat => nat"
@@ -53,14 +55,14 @@
to avoid duplicating their properties. They are distinguished by a
tag (not a bool, to avoid the peculiarities of if-and-only-if).
Session keys implicitly include MAC secrets.*)
- sessionK :: "(nat*nat*nat) * (unit option) => key"
+ sessionK :: "(nat*nat*nat) * role => key"
syntax
clientK, serverK :: "nat*nat*nat => key"
translations
- "clientK X" == "sessionK(X,None)"
- "serverK X" == "sessionK(X,Some())"
+ "clientK X" == "sessionK(X, ClientRole)"
+ "serverK X" == "sessionK(X, ServerRole)"
rules
(*the pseudo-random function is collision-free*)
@@ -87,7 +89,7 @@
"[| evsSK: tls;
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
==> Notes Spy {| Nonce (PRF(M,NA,NB)),
- Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
+ Key (sessionK((NA,NB,M),role)) |} # evsSK : tls"
ClientHello
(*(7.4.1.2)
@@ -113,8 +115,7 @@
Certificate
(*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
- "[| evsC: tls |]
- ==> Says B A (certificate B (pubK B)) # evsC : tls"
+ "evsC: tls ==> Says B A (certificate B (pubK B)) # evsC : tls"
ClientKeyExch
(*CLIENT KEY EXCHANGE (7.4.7).
@@ -151,7 +152,7 @@
(*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 sent ClientFinished. One
+ Spy does not know PMS and could not send ClientFinished. One
could simply put A~=Spy into the rule, but one should not
expect the spy to be well-behaved.*)
"[| evsCF: tls;
@@ -246,7 +247,7 @@
rather unlikely. The assumption A ~= Spy is essential: otherwise
the Spy could learn session keys merely by replaying messages!*)
"[| evso: tls; A ~= Spy;
- Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
- ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso : tls"
+ Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso |]
+ ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso : tls"
end