improved presentation of HOL/Auth theories
authorpaulson
Mon May 05 18:22:01 2003 +0200 (2003-05-05)
changeset 139568fe7e12290e1
parent 13955 8ab1d3e73bb1
child 13957 10dbf16be15f
improved presentation of HOL/Auth theories
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
src/HOL/Auth/document/root.tex
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Mon May 05 15:55:56 2003 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Mon May 05 18:22:01 2003 +0200
     1.3 @@ -1,27 +1,19 @@
     1.4  (*  Title:      HOL/Auth/CertifiedEmail
     1.5      ID:         $Id$
     1.6      Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
     1.7 +*)
     1.8  
     1.9 -The certified electronic mail protocol by Abadi et al.
    1.10 -*)
    1.11 +header{*The Certified Electronic Mail Protocol by Abadi et al.*}
    1.12  
    1.13  theory CertifiedEmail = Public:
    1.14  
    1.15  syntax
    1.16    TTP        :: agent
    1.17    RPwd       :: "agent => key"
    1.18 -  TTPDecKey  :: key
    1.19 -  TTPEncKey  :: key
    1.20 -  TTPSigKey  :: key
    1.21 -  TTPVerKey  :: key
    1.22  
    1.23  translations
    1.24    "TTP"   == "Server "
    1.25    "RPwd"  == "shrK "
    1.26 -  "TTPDecKey" == "priEK Server"
    1.27 -  "TTPEncKey" == "pubEK Server" 
    1.28 -  "TTPSigKey" == "priSK Server"
    1.29 -  "TTPVerKey" == "pubSK Server" 
    1.30  
    1.31   
    1.32  (*FIXME: the four options should be represented by pairs of 0 or 1.
    1.33 @@ -48,7 +40,7 @@
    1.34  Fake: --{*The Spy may say anything he can say.  The sender field is correct,
    1.35            but agents don't use that information.*}
    1.36        "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|] 
    1.37 -       ==> Says Spy B X #evsf \<in> certified_mail"
    1.38 +       ==> Says Spy B X # evsf \<in> certified_mail"
    1.39  
    1.40  FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
    1.41      equipped with the necessary credentials to serve as an SSL server.*}
    1.42 @@ -61,7 +53,7 @@
    1.43     K \<in> symKeys;
    1.44     Nonce q \<notin> used evs1;
    1.45     hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
    1.46 -   S2TTP = Crypt TTPEncKey {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
    1.47 +   S2TTP = Crypt (pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
    1.48   ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
    1.49                  Number cleartext, Nonce q, S2TTP|} # evs1 
    1.50         \<in> certified_mail"
    1.51 @@ -84,13 +76,13 @@
    1.52           He replies over the established SSL channel.*}
    1.53   "[|evs3 \<in> certified_mail;
    1.54      Notes TTP {|Agent R', Agent TTP, S2TTP'', Key(RPwd R'), hr'|} \<in> set evs3;
    1.55 -    S2TTP'' = Crypt TTPEncKey 
    1.56 +    S2TTP'' = Crypt (pubEK TTP) 
    1.57                       {|Agent S, Number BothAuth, Key k', Agent R', hs'|};
    1.58      TTP \<noteq> R';  hs' = hr';  k' \<in> symKeys|]
    1.59   ==> 
    1.60    Notes R' {|Agent TTP, Agent R', Key k', hr'|} # 
    1.61 -  Gets S (Crypt TTPSigKey S2TTP'') # 
    1.62 -  Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
    1.63 +  Gets S (Crypt (priSK TTP) S2TTP'') # 
    1.64 +  Says TTP S (Crypt (priSK TTP) S2TTP'') # evs3 \<in> certified_mail"
    1.65  
    1.66  Reception:
    1.67   "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
    1.68 @@ -99,7 +91,7 @@
    1.69  
    1.70  (*A "possibility property": there are traces that reach the end*)
    1.71  lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
    1.72 -           Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
    1.73 +           Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
    1.74  apply (rule bexE [OF Key_supply1]) 
    1.75  apply (intro exI bexI)
    1.76  apply (rule_tac [2] certified_mail.Nil
    1.77 @@ -176,33 +168,23 @@
    1.78       ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.79  by (blast intro: Spy_dont_know_private_keys parts.Inj)
    1.80  
    1.81 -lemma Spy_dont_know_TTPDecKey [simp]:
    1.82 -     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
    1.83 -by auto
    1.84 +lemma Spy_dont_know_TTPKey_parts [simp]:
    1.85 +     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)" 
    1.86 +by simp
    1.87  
    1.88 -lemma Spy_dont_know_TTPDecKey_analz [simp]:
    1.89 -     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)" 
    1.90 -by (force dest!: analz_subset_parts[THEN subsetD])
    1.91 -
    1.92 -lemma Spy_dont_know_TTPSigKey [simp]:
    1.93 -     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> parts(knows Spy evs)"
    1.94 -by auto
    1.95 -
    1.96 -lemma Spy_dont_know_TTPSigKey_analz [simp]:
    1.97 -     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> analz(knows Spy evs)" 
    1.98 +lemma Spy_dont_know_TTPKey_analz [simp]:
    1.99 +     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)" 
   1.100  by (force dest!: analz_subset_parts[THEN subsetD])
   1.101  
   1.102  text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
   1.103  belonging to @{term TTP}*}
   1.104 -declare Spy_dont_know_TTPDecKey [THEN [2] rev_notE, elim!]
   1.105 -declare Spy_dont_know_TTPSigKey [THEN [2] rev_notE, elim!]
   1.106 -
   1.107 +declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]
   1.108  
   1.109  
   1.110  lemma CM3_k_parts_knows_Spy:
   1.111   "[| evs \<in> certified_mail;
   1.112       Notes TTP {|Agent A, Agent TTP,
   1.113 -                 Crypt TTPEncKey {|Agent S, Number AO, Key K, 
   1.114 +                 Crypt (pubEK TTP) {|Agent S, Number AO, Key K, 
   1.115                   Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
   1.116    ==> Key K \<in> parts(spies evs)"
   1.117  apply (rotate_tac 1)
   1.118 @@ -250,8 +232,8 @@
   1.119  
   1.120  text{*Unused, but a guarantee of sorts*}
   1.121  theorem CertAutenticity:
   1.122 -     "[|Crypt TTPSigKey X \<in> parts (spies evs); evs \<in> certified_mail|] 
   1.123 -      ==> \<exists>A. Says TTP A (Crypt TTPSigKey X) \<in> set evs"
   1.124 +     "[|Crypt (priSK TTP) X \<in> parts (spies evs); evs \<in> certified_mail|] 
   1.125 +      ==> \<exists>A. Says TTP A (Crypt (priSK TTP) X) \<in> set evs"
   1.126  apply (erule rev_mp)
   1.127  apply (erule certified_mail.induct, simp_all) 
   1.128  txt{*Fake*}
   1.129 @@ -272,7 +254,7 @@
   1.130  
   1.131  lemma analz_image_freshK [rule_format]:
   1.132   "evs \<in> certified_mail ==>
   1.133 -   \<forall>K KK. invKey TTPEncKey \<notin> KK -->
   1.134 +   \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
   1.135            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   1.136            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   1.137  apply (erule certified_mail.induct)
   1.138 @@ -289,7 +271,7 @@
   1.139  
   1.140  
   1.141  lemma analz_insert_freshK:
   1.142 -  "[| evs \<in> certified_mail;  KAB \<noteq> invKey TTPEncKey |] ==>
   1.143 +  "[| evs \<in> certified_mail;  KAB \<noteq> invKey (pubEK TTP) |] ==>
   1.144        (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   1.145        (K = KAB | Key K \<in> analz (knows Spy evs))"
   1.146  by (simp only: analz_image_freshK analz_image_freshK_simps)
   1.147 @@ -307,14 +289,14 @@
   1.148  lemma S2TTP_sender_lemma [rule_format]:
   1.149   "evs \<in> certified_mail ==>
   1.150      Key K \<notin> analz (knows Spy evs) -->
   1.151 -    (\<forall>AO. Crypt TTPEncKey
   1.152 +    (\<forall>AO. Crypt (pubEK TTP)
   1.153  	   {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
   1.154      (\<exists>m ctxt q. 
   1.155          hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
   1.156  	Says S R
   1.157  	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
   1.158  	     Number ctxt, Nonce q,
   1.159 -	     Crypt TTPEncKey
   1.160 +	     Crypt (pubEK TTP)
   1.161  	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" 
   1.162  apply (erule certified_mail.induct, analz_mono_contra)
   1.163  apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
   1.164 @@ -324,10 +306,9 @@
   1.165               dest!: analz_subset_parts[THEN subsetD])  
   1.166  txt{*Fake SSL*}
   1.167  apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.168 -            dest: analz_subset_parts[THEN subsetD])  
   1.169 +             dest: analz_subset_parts[THEN subsetD])  
   1.170  txt{*Message 1*}
   1.171 -apply clarsimp
   1.172 -apply blast 
   1.173 +apply (clarsimp, blast)
   1.174  txt{*Message 2*}
   1.175  apply (simp add: parts_insert2, clarify) 
   1.176  apply (drule parts_cut, assumption, simp) 
   1.177 @@ -337,7 +318,7 @@
   1.178  done 
   1.179  
   1.180  lemma S2TTP_sender:
   1.181 - "[|Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
   1.182 + "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
   1.183      Key K \<notin> analz (knows Spy evs);
   1.184      evs \<in> certified_mail|]
   1.185    ==> \<exists>m ctxt q. 
   1.186 @@ -345,7 +326,7 @@
   1.187  	Says S R
   1.188  	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
   1.189  	     Number ctxt, Nonce q,
   1.190 -	     Crypt TTPEncKey
   1.191 +	     Crypt (pubEK TTP)
   1.192  	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" 
   1.193  by (blast intro: S2TTP_sender_lemma) 
   1.194  
   1.195 @@ -377,13 +358,13 @@
   1.196          Says S R
   1.197             {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
   1.198               Number cleartext, Nonce q,
   1.199 -             Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
   1.200 +             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
   1.201            \<in> set evs -->
   1.202         (\<forall>m' cleartext' q' hs'.
   1.203         Says S' R'
   1.204             {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
   1.205               Number cleartext', Nonce q',
   1.206 -             Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.207 +             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.208            \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
   1.209  apply (erule certified_mail.induct, analz_mono_contra, simp_all)
   1.210  txt{*Fake*} 
   1.211 @@ -397,12 +378,12 @@
   1.212        "[|Says S R
   1.213             {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
   1.214               Number cleartext, Nonce q,
   1.215 -             Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|}|}
   1.216 +             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
   1.217            \<in> set evs;
   1.218           Says S' R'
   1.219             {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
   1.220               Number cleartext', Nonce q',
   1.221 -             Crypt TTPEncKey {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.222 +             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.223            \<in> set evs;
   1.224           Key K \<notin> analz (knows Spy evs);
   1.225           evs \<in> certified_mail|]
   1.226 @@ -418,14 +399,14 @@
   1.227  theorem Spy_see_encrypted_key_imp:
   1.228        "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
   1.229                       Number cleartext, Nonce q, S2TTP|} \<in> set evs;
   1.230 +         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
   1.231           Key K \<in> analz(knows Spy evs);
   1.232 -         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
   1.233  	 evs \<in> certified_mail;
   1.234           S\<noteq>Spy|]
   1.235 -      ==> R \<in> bad & Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
   1.236 -apply (erule rev_mp)
   1.237 +      ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
   1.238  apply (erule rev_mp)
   1.239  apply (erule ssubst)
   1.240 +apply (erule rev_mp)
   1.241  apply (erule certified_mail.induct, simp_all)
   1.242  txt{*Fake*}
   1.243  apply spy_analz
   1.244 @@ -446,7 +427,7 @@
   1.245  theorem Spy_not_see_encrypted_key:
   1.246        "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
   1.247                       Number cleartext, Nonce q, S2TTP|} \<in> set evs;
   1.248 -         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
   1.249 +         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
   1.250  	 evs \<in> certified_mail;
   1.251           S\<noteq>Spy; R \<notin> bad|]
   1.252        ==> Key K \<notin> analz(knows Spy evs)"
   1.253 @@ -456,18 +437,15 @@
   1.254  text{*Agent @{term R}, who may be the Spy, doesn't receive the key
   1.255   until @{term S} has access to the return receipt.*} 
   1.256  theorem S_guarantee:
   1.257 -      "[|Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
   1.258 -         Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
   1.259 +      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
   1.260                       Number cleartext, Nonce q, S2TTP|} \<in> set evs;
   1.261 -         S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
   1.262 -         hs = Hash {|Number cleartext, Nonce q, response S R q, 
   1.263 -                     Crypt K (Number m)|};
   1.264 +         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
   1.265 +         Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
   1.266           S\<noteq>Spy;  evs \<in> certified_mail|]
   1.267 -      ==> Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
   1.268 -apply (erule rev_mp)
   1.269 +      ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
   1.270  apply (erule rev_mp)
   1.271  apply (erule ssubst)
   1.272 -apply (erule ssubst)
   1.273 +apply (erule rev_mp)
   1.274  apply (erule certified_mail.induct, simp_all)
   1.275  txt{*Message 1*}
   1.276  apply (blast dest: Notes_imp_used) 
   1.277 @@ -481,8 +459,8 @@
   1.278       a delivery certificate exists, then @{term R}
   1.279       receives the necessary key.*}
   1.280  theorem R_guarantee:
   1.281 -  "[|Crypt TTPSigKey S2TTP \<in> used evs;
   1.282 -     S2TTP = Crypt TTPEncKey
   1.283 +  "[|Crypt (priSK TTP) S2TTP \<in> used evs;
   1.284 +     S2TTP = Crypt (pubEK TTP)
   1.285                 {|Agent S, Number AO, Key K, Agent R, 
   1.286                   Hash {|Number cleartext, Nonce q, r, em|}|};
   1.287       hr = Hash {|Number cleartext, Nonce q, r, em|};
     2.1 --- a/src/HOL/Auth/Event.thy	Mon May 05 15:55:56 2003 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Mon May 05 18:22:01 2003 +0200
     2.3 @@ -3,14 +3,14 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1996  University of Cambridge
     2.6  
     2.7 -Theory of events for security protocols
     2.8 -
     2.9  Datatype of events; function "spies"; freshness
    2.10  
    2.11  "bad" agents have been broken by the Spy; their private keys and internal
    2.12      stores are visible to him
    2.13  *)
    2.14  
    2.15 +header{*Theory of Events for Security Protocols*}
    2.16 +
    2.17  theory Event = Message:
    2.18  
    2.19  consts  (*Initial states of agents -- parameter of the construction*)
    2.20 @@ -99,10 +99,9 @@
    2.21  
    2.22  subsection{*Function @{term knows}*}
    2.23  
    2.24 -text{*Simplifying   @term{"parts (insert X (knows Spy evs))
    2.25 -      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
    2.26 -
    2.27 -text{*This version won't loop with the simplifier.*}
    2.28 +(*Simplifying   
    2.29 + parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
    2.30 +  This version won't loop with the simplifier.*)
    2.31  lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    2.32  
    2.33  lemma knows_Spy_Says [simp]:
     3.1 --- a/src/HOL/Auth/Message.thy	Mon May 05 15:55:56 2003 +0200
     3.2 +++ b/src/HOL/Auth/Message.thy	Mon May 05 18:22:01 2003 +0200
     3.3 @@ -7,6 +7,8 @@
     3.4  Inductive relations "parts", "analz" and "synth"
     3.5  *)
     3.6  
     3.7 +header{*Theory of Agents and Messages for Security Protocols*}
     3.8 +
     3.9  theory Message = Main:
    3.10  
    3.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
     4.1 --- a/src/HOL/Auth/NS_Public.thy	Mon May 05 15:55:56 2003 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.thy	Mon May 05 18:22:01 2003 +0200
     4.3 @@ -7,6 +7,8 @@
     4.4  Version incorporating Lowe's fix (inclusion of B's identity in round 2).
     4.5  *)
     4.6  
     4.7 +header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}
     4.8 +
     4.9  theory NS_Public = Public:
    4.10  
    4.11  consts  ns_public  :: "event list set"
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Mon May 05 15:55:56 2003 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Mon May 05 18:22:01 2003 +0200
     5.3 @@ -11,6 +11,8 @@
     5.4    Proc. Royal Soc. 426 (1989)
     5.5  *)
     5.6  
     5.7 +header{*Verifying the Needham-Schroeder Public-Key Protocol*}
     5.8 +
     5.9  theory NS_Public_Bad = Public:
    5.10  
    5.11  consts  ns_public  :: "event list set"
     6.1 --- a/src/HOL/Auth/NS_Shared.thy	Mon May 05 15:55:56 2003 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon May 05 18:22:01 2003 +0200
     6.3 @@ -240,7 +240,7 @@
     6.4  
     6.5  subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
     6.6  
     6.7 -text{*Beware of [rule_format] and the universal quantifier!*}
     6.8 +text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
     6.9  lemma secrecy_lemma:
    6.10       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
    6.11                                        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
     7.1 --- a/src/HOL/Auth/Public.thy	Mon May 05 15:55:56 2003 +0200
     7.2 +++ b/src/HOL/Auth/Public.thy	Mon May 05 18:22:01 2003 +0200
     7.3 @@ -314,7 +314,7 @@
     7.4  apply (rule someI, fast)
     7.5  done
     7.6  
     7.7 -subsection{*Specialized rewriting for the analz_image_... theorems*}
     7.8 +subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
     7.9  
    7.10  lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
    7.11  by blast
     8.1 --- a/src/HOL/Auth/Recur.thy	Mon May 05 15:55:56 2003 +0200
     8.2 +++ b/src/HOL/Auth/Recur.thy	Mon May 05 18:22:01 2003 +0200
     8.3 @@ -392,7 +392,8 @@
     8.4  apply blast
     8.5  txt{*Inductive step of respond*}
     8.6  apply (intro allI conjI impI, simp_all)
     8.7 -txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}   
     8.8 +txt{*by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
     8.9 +     if @{term "B \<in> bad"}*}   
    8.10  apply (blast dest: unique_session_keys respond_certificate)
    8.11  apply (blast dest!: respond_certificate)
    8.12  apply (blast dest!: resp_analz_insert)
     9.1 --- a/src/HOL/Auth/Shared.thy	Mon May 05 15:55:56 2003 +0200
     9.2 +++ b/src/HOL/Auth/Shared.thy	Mon May 05 18:22:01 2003 +0200
     9.3 @@ -242,7 +242,7 @@
     9.4       REPEAT_FIRST (resolve_tac [refl, conjI]))
     9.5  *}
     9.6  
     9.7 -subsection{*Specialized rewriting for analz_insert_freshK*}
     9.8 +subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
     9.9  
    9.10  lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
    9.11  by blast
    9.12 @@ -250,7 +250,7 @@
    9.13  lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
    9.14  by blast
    9.15  
    9.16 -lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
    9.17 +lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
    9.18  by blast
    9.19  
    9.20  (** Reverse the normal simplification of "image" to build up (not break down)
    10.1 --- a/src/HOL/Auth/TLS.thy	Mon May 05 15:55:56 2003 +0200
    10.2 +++ b/src/HOL/Auth/TLS.thy	Mon May 05 18:22:01 2003 +0200
    10.3 @@ -39,6 +39,8 @@
    10.4  	Notes A {|Agent B, Nonce PMS|}.
    10.5  *)
    10.6  
    10.7 +header{*The TLS Protocol: Transport Layer Security*}
    10.8 +
    10.9  theory TLS = Public:
   10.10  
   10.11  constdefs
   10.12 @@ -95,7 +97,8 @@
   10.13           "[| evsf \<in> tls;  X \<in> synth (analz (spies evsf)) |]
   10.14            ==> Says Spy B X # evsf \<in> tls"
   10.15  
   10.16 -   SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*}
   10.17 +   SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK}
   10.18 +                to available nonces*}
   10.19           "[| evsSK \<in> tls;
   10.20  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
   10.21            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
   10.22 @@ -103,21 +106,21 @@
   10.23  
   10.24     ClientHello:
   10.25  	 --{*(7.4.1.2)
   10.26 -	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
   10.27 +	   PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}.
   10.28  	   It is uninterpreted but will be confirmed in the FINISHED messages.
   10.29 -	   NA is CLIENT RANDOM, while SID is SESSION_ID.
   10.30 +	   NA is CLIENT RANDOM, while SID is @{text SESSION_ID}.
   10.31             UNIX TIME is omitted because the protocol doesn't use it.
   10.32 -           May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes
   10.33 -	   while MASTER SECRET is 48 bytes*}
   10.34 +           May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is 
   10.35 +           28 bytes while MASTER SECRET is 48 bytes*}
   10.36           "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
   10.37            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
   10.38  	        # evsCH  \<in>  tls"
   10.39  
   10.40     ServerHello:
   10.41           --{*7.4.1.3 of the TLS Internet-Draft
   10.42 -	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   10.43 +	   PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}.
   10.44             SERVER CERTIFICATE (7.4.2) is always present.
   10.45 -           CERTIFICATE_REQUEST (7.4.4) is implied.*}
   10.46 +           @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*}
   10.47           "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
   10.48               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   10.49  	       \<in> set evsSH |]
   10.50 @@ -131,7 +134,7 @@
   10.51           --{*CLIENT KEY EXCHANGE (7.4.7).
   10.52             The client, A, chooses PMS, the PREMASTER SECRET.
   10.53             She encrypts PMS using the supplied KB, which ought to be pubK B.
   10.54 -           We assume PMS \<notin> range PRF because a clash betweem the PMS
   10.55 +           We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS
   10.56             and another MASTER SECRET is highly unlikely (even though
   10.57  	   both items have the same length, 48 bytes).
   10.58             The Note event records in the trace that she knows PMS
   10.59 @@ -163,7 +166,7 @@
   10.60            rule's applying when the Spy has satisfied the "Says A B" by
   10.61            repaying messages sent by the true client; in that case, the
   10.62            Spy does not know PMS and could not send ClientFinished.  One
   10.63 -          could simply put A\<noteq>Spy into the rule, but one should not
   10.64 +          could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
   10.65            expect the spy to be well-behaved.*}
   10.66           "[| evsCF \<in> tls;
   10.67  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   10.68 @@ -196,7 +199,7 @@
   10.69  	--{*Having transmitted ClientFinished and received an identical
   10.70            message encrypted with serverK, the client stores the parameters
   10.71            needed to resume this session.  The "Notes A ..." premise is
   10.72 -          used to prove Notes_master_imp_Crypt_PMS.*}
   10.73 +          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
   10.74           "[| evsCA \<in> tls;
   10.75  	     Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
   10.76  	     M = PRF(PMS,NA,NB);
   10.77 @@ -212,7 +215,7 @@
   10.78  	--{*Having transmitted ServerFinished and received an identical
   10.79            message encrypted with clientK, the server stores the parameters
   10.80            needed to resume this session.  The "Says A'' B ..." premise is
   10.81 -          used to prove Notes_master_imp_Crypt_PMS.*}
   10.82 +          used to prove @{text Notes_master_imp_Crypt_PMS}.*}
   10.83           "[| evsSA \<in> tls;
   10.84  	     A \<noteq> B;
   10.85               Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
   10.86 @@ -226,8 +229,8 @@
   10.87               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
   10.88  
   10.89     ClientResume:
   10.90 -         --{*If A recalls the SESSION_ID, then she sends a FINISHED message
   10.91 -           using the new nonces and stored MASTER SECRET.*}
   10.92 +         --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED
   10.93 +             message using the new nonces and stored MASTER SECRET.*}
   10.94           "[| evsCR \<in> tls;
   10.95  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
   10.96               Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
   10.97 @@ -239,8 +242,8 @@
   10.98                # evsCR  \<in>  tls"
   10.99  
  10.100     ServerResume:
  10.101 -         --{*Resumption (7.3):  If B finds the SESSION_ID then he can send
  10.102 -           a FINISHED message using the recovered MASTER SECRET*}
  10.103 +         --{*Resumption (7.3):  If B finds the @{text SESSION_ID} then he can 
  10.104 +             send a FINISHED message using the recovered MASTER SECRET*}
  10.105           "[| evsSR \<in> tls;
  10.106  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
  10.107  	     Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
  10.108 @@ -254,8 +257,9 @@
  10.109     Oops:
  10.110           --{*The most plausible compromise is of an old session key.  Losing
  10.111             the MASTER SECRET or PREMASTER SECRET is more serious but
  10.112 -           rather unlikely.  The assumption A \<noteq> Spy is essential: otherwise
  10.113 -           the Spy could learn session keys merely by replaying messages!*}
  10.114 +           rather unlikely.  The assumption @{term "A\<noteq>Spy"} is essential: 
  10.115 +           otherwise the Spy could learn session keys merely by 
  10.116 +           replaying messages!*}
  10.117           "[| evso \<in> tls;  A \<noteq> Spy;
  10.118  	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |]
  10.119            ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  \<in>  tls"
  10.120 @@ -546,7 +550,7 @@
  10.121  
  10.122  subsection{*Secrecy Theorems*}
  10.123  
  10.124 -text{*Key compromise lemma needed to prove analz_image_keys.
  10.125 +text{*Key compromise lemma needed to prove @{term analz_image_keys}.
  10.126    No collection of keys can help the spy get new private keys.*}
  10.127  lemma analz_image_priK [rule_format]:
  10.128       "evs \<in> tls
  10.129 @@ -647,7 +651,7 @@
  10.130    Converse fails; betraying M doesn't force the keys to be sent!
  10.131    The strong Oops condition can be weakened later by unicity reasoning,
  10.132    with some effort.
  10.133 -  NO LONGER USED: see clientK_not_spied and serverK_not_spied*}
  10.134 +  NO LONGER USED: see @{text clientK_not_spied} and @{text serverK_not_spied}*}
  10.135  lemma sessionK_not_spied:
  10.136       "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
  10.137           Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
  10.138 @@ -676,7 +680,7 @@
  10.139  apply (blast dest: Notes_Crypt_parts_spies)
  10.140  apply (blast dest: Notes_Crypt_parts_spies)
  10.141  apply (blast dest: Notes_Crypt_parts_spies)
  10.142 -txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*}
  10.143 +txt{*ClientAccepts and ServerAccepts: because @{term "PMS \<notin> range PRF"}*}
  10.144  apply force+
  10.145  done
  10.146  
  10.147 @@ -787,8 +791,7 @@
  10.148  
  10.149  subsubsection{*Protocol goals: if A receives ServerFinished, then B is present
  10.150       and has used the quoted values PA, PB, etc.  Note that it is up to A
  10.151 -     to compare PA with what she originally sent.
  10.152 -***)
  10.153 +     to compare PA with what she originally sent.*}
  10.154  
  10.155  text{*The mention of her name (A) in X assures A that B knows who she is.*}
  10.156  lemma TrustServerFinished [rule_format]:
  10.157 @@ -861,8 +864,7 @@
  10.158  
  10.159  subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to
  10.160       check a CertVerify from A, then A has used the quoted
  10.161 -     values PA, PB, etc.  Even this one requires A to be uncompromised.
  10.162 -*}
  10.163 +     values PA, PB, etc.  Even this one requires A to be uncompromised.*}
  10.164  lemma AuthClientFinished:
  10.165       "[| M = PRF(PMS,NA,NB);
  10.166           Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
    11.1 --- a/src/HOL/Auth/Yahalom.thy	Mon May 05 15:55:56 2003 +0200
    11.2 +++ b/src/HOL/Auth/Yahalom.thy	Mon May 05 18:22:01 2003 +0200
    11.3 @@ -12,6 +12,8 @@
    11.4  This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
    11.5  *)
    11.6  
    11.7 +header{*The Yahalom Protocol*}
    11.8 +
    11.9  theory Yahalom = Shared:
   11.10  
   11.11  consts  yahalom   :: "event list set"
    12.1 --- a/src/HOL/Auth/Yahalom2.thy	Mon May 05 15:55:56 2003 +0200
    12.2 +++ b/src/HOL/Auth/Yahalom2.thy	Mon May 05 18:22:01 2003 +0200
    12.3 @@ -11,7 +11,7 @@
    12.4    Proc. Royal Soc. 426 (1989)
    12.5  *)
    12.6  
    12.7 -header{*Inductive Analysis of the Yahalom protocol, Variant 2*}
    12.8 +header{*The Yahalom Protocol, Variant 2*}
    12.9  
   12.10  theory Yahalom2 = Shared:
   12.11  
    13.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Mon May 05 15:55:56 2003 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Mon May 05 18:22:01 2003 +0200
    13.3 @@ -10,6 +10,8 @@
    13.4  The issues are discussed in lcp's LICS 2000 invited lecture.
    13.5  *)
    13.6  
    13.7 +header{*The Yahalom Protocol: A Flawed Version*}
    13.8 +
    13.9  theory Yahalom_Bad = Shared:
   13.10  
   13.11  consts  yahalom   :: "event list set"
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Auth/document/root.tex	Mon May 05 18:22:01 2003 +0200
    14.3 @@ -0,0 +1,27 @@
    14.4 +\documentclass[10pt,a4paper,twoside]{article}
    14.5 +\usepackage{graphicx}
    14.6 +\usepackage{latexsym,theorem}
    14.7 +\usepackage{isabelle,isabellesym}
    14.8 +\usepackage{pdfsetup}\urlstyle{rm}
    14.9 +
   14.10 +\begin{document}
   14.11 +
   14.12 +\pagestyle{headings}
   14.13 +\pagenumbering{arabic}
   14.14 +
   14.15 +\title{Security Protocols}
   14.16 +\author{Giampaolo Bella, Frederic Blanqui, Lawrence C. Paulson et al.}
   14.17 +\maketitle
   14.18 +
   14.19 +\tableofcontents
   14.20 +
   14.21 +\begin{center}
   14.22 +  \includegraphics[scale=0.5]{session_graph}  
   14.23 +\end{center}
   14.24 +
   14.25 +\newpage
   14.26 +
   14.27 +\parindent 0pt\parskip 0.5ex
   14.28 +
   14.29 +\input{session}
   14.30 +\end{document}