# HG changeset patch
# User paulson
# Date 919158895 -3600
# Node ID 147db42c10091aed86a9fbb9b2d7095e0a2e6345
# Parent  e3096df443264ae7cfd25da2012dfc8eb7dc83a9
tidying in conjuntion with the TISSEC paper; replaced (unit option)
by a new datatype (role)

diff -r e3096df44326 -r 147db42c1009 src/HOL/Auth/TLS.ML
--- 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*)
diff -r e3096df44326 -r 147db42c1009 src/HOL/Auth/TLS.thy
--- 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