tidying in conjuntion with the TISSEC paper; replaced (unit option)
authorpaulson
Tue Feb 16 10:54:55 1999 +0100 (1999-02-16)
changeset 6284147db42c1009
parent 6283 e3096df44326
child 6285 112a15c311f0
tidying in conjuntion with the TISSEC paper; replaced (unit option)
by a new datatype (role)
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Feb 16 10:50:35 1999 +0100
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Feb 16 10:54:55 1999 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  by (etac rev_mp 1);
     1.5  by (parts_induct_tac 1);
     1.6  (*ServerAccepts*)
     1.7 -by (Fast_tac 1);	(*Blast_tac's very slow here*)
     1.8 +by (Fast_tac 1);
     1.9  qed "Notes_master_imp_Notes_PMS";
    1.10  
    1.11  
    1.12 @@ -402,7 +402,7 @@
    1.13    Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
    1.14    THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
    1.15  Goal "[| Nonce PMS ~: parts (spies evs);  \
    1.16 -\        K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
    1.17 +\        K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);  \
    1.18  \        evs : tls |]             \
    1.19  \  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
    1.20  by (etac rev_mp 1);
    1.21 @@ -420,13 +420,13 @@
    1.22  				 Notes_master_imp_Crypt_PMS]) 1));
    1.23  val lemma = result();
    1.24  
    1.25 -Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \
    1.26 +Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \
    1.27  \        evs : tls |]             \
    1.28  \     ==> Nonce PMS : parts (spies evs)";
    1.29  by (blast_tac (claset() addDs [lemma]) 1);
    1.30  qed "PMS_sessionK_not_spied";
    1.31  
    1.32 -Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y  \
    1.33 +Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y  \
    1.34  \          : parts (spies evs);  evs : tls |]             \
    1.35  \     ==> Nonce PMS : parts (spies evs)";
    1.36  by (blast_tac (claset() addDs [lemma]) 1);
    1.37 @@ -437,12 +437,12 @@
    1.38    The strong Oops condition can be weakened later by unicity reasoning, 
    1.39    with some effort.  
    1.40    NO LONGER USED: see clientK_not_spied and serverK_not_spied*)
    1.41 -Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
    1.42 +Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),role))) ~: set evs; \
    1.43  \        Nonce M ~: analz (spies evs);  evs : tls |]   \
    1.44 -\     ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
    1.45 +\     ==> Key (sessionK((NA,NB,M),role)) ~: parts (spies evs)";
    1.46  by (etac rev_mp 1);
    1.47  by (etac rev_mp 1);
    1.48 -by (analz_induct_tac 1);        (*7 seconds*)
    1.49 +by (analz_induct_tac 1);        (*5 seconds*)
    1.50  (*SpyKeys*)
    1.51  by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
    1.52  (*Fake*) 
    1.53 @@ -456,7 +456,7 @@
    1.54  Goal "[| evs : tls;  A ~: bad;  B ~: bad |]           \
    1.55  \     ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.56  \         Nonce PMS ~: analz (spies evs)";
    1.57 -by (analz_induct_tac 1);   (*11 seconds*)
    1.58 +by (analz_induct_tac 1);   (*4 seconds*)
    1.59  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
    1.60  by (REPEAT (fast_tac (claset() addss (simpset())) 6));
    1.61  (*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
    1.62 @@ -476,7 +476,7 @@
    1.63  Goal "[| evs : tls;  A ~: bad;  B ~: bad |]           \
    1.64  \     ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.65  \         Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
    1.66 -by (analz_induct_tac 1);   (*13 seconds*)
    1.67 +by (analz_induct_tac 1);   (*4 seconds*)
    1.68  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
    1.69  by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
    1.70  				       Says_imp_spies RS analz.Inj,
    1.71 @@ -505,7 +505,7 @@
    1.72  \     ==> A = A'";
    1.73  by (etac rev_mp 1);
    1.74  by (etac rev_mp 1);
    1.75 -by (analz_induct_tac 1);	(*8 seconds*)
    1.76 +by (analz_induct_tac 1); 
    1.77  by (ALLGOALS Clarify_tac);
    1.78  (*ClientFinished, ClientResume: by unicity of PMS*)
    1.79  by (REPEAT 
    1.80 @@ -526,7 +526,7 @@
    1.81  \     ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
    1.82  by (etac rev_mp 1);
    1.83  by (etac rev_mp 1);
    1.84 -by (analz_induct_tac 1);        (*17 seconds*)
    1.85 +by (analz_induct_tac 1);        (*4 seconds*)
    1.86  (*Oops*)
    1.87  by (blast_tac (claset() addIs [Says_clientK_unique]) 4);
    1.88  (*ClientKeyExch*)
    1.89 @@ -548,7 +548,7 @@
    1.90  \     ==> B = B'";
    1.91  by (etac rev_mp 1);
    1.92  by (etac rev_mp 1);
    1.93 -by (analz_induct_tac 1);	(*9 seconds*)
    1.94 +by (analz_induct_tac 1);
    1.95  by (ALLGOALS Clarify_tac);
    1.96  (*ServerResume, ServerFinished: by unicity of PMS*)
    1.97  by (REPEAT
    1.98 @@ -563,13 +563,13 @@
    1.99  
   1.100  (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   1.101    then it is completely secure: not even in parts!*)
   1.102 -Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs;  \
   1.103 +Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs;                   \
   1.104  \        Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs; \
   1.105 -\        evs : tls;  A ~: bad;  B ~: bad |]                        \
   1.106 +\        A ~: bad;  B ~: bad;  evs : tls |]                          \
   1.107  \     ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
   1.108  by (etac rev_mp 1);
   1.109  by (etac rev_mp 1);
   1.110 -by (analz_induct_tac 1);        (*6 seconds*)
   1.111 +by (analz_induct_tac 1);
   1.112  (*Oops*)
   1.113  by (blast_tac (claset() addIs [Says_serverK_unique]) 4);
   1.114  (*ClientKeyExch*)
   1.115 @@ -597,7 +597,7 @@
   1.116  \         Notes A {|Agent B, Nonce PMS|} : set evs --> \
   1.117  \         X : parts (spies evs) --> Says B A X : set evs";
   1.118  by (hyp_subst_tac 1);
   1.119 -by (analz_induct_tac 1);        (*10 seconds*)
   1.120 +by (analz_induct_tac 1);        (*7 seconds*)
   1.121  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.122  by (ALLGOALS Clarify_tac);
   1.123  (*ClientKeyExch*)
   1.124 @@ -606,7 +606,6 @@
   1.125  by (blast_tac (claset() addEs [serverK_not_spied RSN (2,rev_notE)]) 1);
   1.126  qed_spec_mp "TrustServerFinished";
   1.127  
   1.128 -
   1.129  (*This version refers not to ServerFinished but to any message from B.
   1.130    We don't assume B has received CertVerify, and an intruder could
   1.131    have changed A's identity in all other messages, so we can't be sure
   1.132 @@ -618,7 +617,7 @@
   1.133  \         Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   1.134  \         (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   1.135  by (hyp_subst_tac 1);
   1.136 -by (analz_induct_tac 1);	(*20 seconds*)
   1.137 +by (analz_induct_tac 1);	(*6 seconds*)
   1.138  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   1.139  by (ALLGOALS Clarify_tac);
   1.140  (*ServerResume, ServerFinished: by unicity of PMS*)
   1.141 @@ -646,7 +645,7 @@
   1.142  \         Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
   1.143  \         Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   1.144  by (hyp_subst_tac 1);
   1.145 -by (analz_induct_tac 1);	(*15 seconds*)
   1.146 +by (analz_induct_tac 1);	(*6 seconds*)
   1.147  by (ALLGOALS Clarify_tac);
   1.148  (*ClientFinished, ClientResume: by unicity of PMS*)
   1.149  by (REPEAT (blast_tac (claset() delrules [conjI]
   1.150 @@ -684,3 +683,6 @@
   1.151  
   1.152  (*08/9/97: loads in 189s (pike), after much reorganization, 
   1.153             back to 621s on albatross?*)
   1.154 +
   1.155 +(*10/2/99: loads in 139s (pike)
   1.156 +           down to 433s on albatross*)
     2.1 --- a/src/HOL/Auth/TLS.thy	Tue Feb 16 10:50:35 1999 +0100
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Feb 16 10:54:55 1999 +0100
     2.3 @@ -45,6 +45,8 @@
     2.4    certificate      :: "[agent,key] => msg"
     2.5      "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
     2.6  
     2.7 +datatype role = ClientRole | ServerRole
     2.8 +
     2.9  consts
    2.10    (*Pseudo-random function of Section 5*)
    2.11    PRF  :: "nat*nat*nat => nat"
    2.12 @@ -53,14 +55,14 @@
    2.13      to avoid duplicating their properties.  They are distinguished by a
    2.14      tag (not a bool, to avoid the peculiarities of if-and-only-if).
    2.15      Session keys implicitly include MAC secrets.*)
    2.16 -  sessionK :: "(nat*nat*nat) * (unit option) => key"
    2.17 +  sessionK :: "(nat*nat*nat) * role => key"
    2.18  
    2.19  syntax
    2.20      clientK, serverK :: "nat*nat*nat => key"
    2.21  
    2.22  translations
    2.23 -  "clientK X" == "sessionK(X,None)"
    2.24 -  "serverK X" == "sessionK(X,Some())"
    2.25 +  "clientK X" == "sessionK(X, ClientRole)"
    2.26 +  "serverK X" == "sessionK(X, ServerRole)"
    2.27  
    2.28  rules
    2.29    (*the pseudo-random function is collision-free*)
    2.30 @@ -87,7 +89,7 @@
    2.31           "[| evsSK: tls;
    2.32  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
    2.33            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    2.34 -			   Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    2.35 +			   Key (sessionK((NA,NB,M),role)) |} # evsSK : tls"
    2.36  
    2.37      ClientHello
    2.38  	 (*(7.4.1.2)
    2.39 @@ -113,8 +115,7 @@
    2.40  
    2.41      Certificate
    2.42           (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    2.43 -         "[| evsC: tls |]
    2.44 -          ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    2.45 +         "evsC: tls ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    2.46  
    2.47      ClientKeyExch
    2.48           (*CLIENT KEY EXCHANGE (7.4.7).
    2.49 @@ -151,7 +152,7 @@
    2.50          (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
    2.51            rule's applying when the Spy has satisfied the "Says A B" by
    2.52            repaying messages sent by the true client; in that case, the
    2.53 -          Spy does not know PMS and could not sent ClientFinished.  One
    2.54 +          Spy does not know PMS and could not send ClientFinished.  One
    2.55            could simply put A~=Spy into the rule, but one should not
    2.56            expect the spy to be well-behaved.*)
    2.57           "[| evsCF: tls;  
    2.58 @@ -246,7 +247,7 @@
    2.59             rather unlikely.  The assumption A ~= Spy is essential: otherwise
    2.60             the Spy could learn session keys merely by replaying messages!*)
    2.61           "[| evso: tls;  A ~= Spy;
    2.62 -	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
    2.63 -          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
    2.64 +	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso |]
    2.65 +          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  :  tls"
    2.66  
    2.67  end