src/HOL/Auth/NS_Shared.thy
changeset 61830 4f5ab843cf5b
parent 58889 5b7a9633cfa8
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Dec 10 21:31:24 2015 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Dec 10 21:39:33 2015 +0100
     1.3 @@ -3,15 +3,15 @@
     1.4      Copyright   1996  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
     1.8 +section\<open>Needham-Schroeder Shared-Key Protocol and the Issues Property\<close>
     1.9  
    1.10  theory NS_Shared imports Public begin
    1.11  
    1.12 -text{*
    1.13 +text\<open>
    1.14  From page 247 of
    1.15    Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    1.16    Proc. Royal Soc. 426
    1.17 -*}
    1.18 +\<close>
    1.19  
    1.20  definition
    1.21   (* A is the true creator of X if she has sent X and X never appeared on
    1.22 @@ -88,7 +88,7 @@
    1.23  declare analz_into_parts [dest]
    1.24  
    1.25  
    1.26 -text{*A "possibility property": there are traces that reach the end*}
    1.27 +text\<open>A "possibility property": there are traces that reach the end\<close>
    1.28  lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
    1.29         ==> \<exists>N. \<exists>evs \<in> ns_shared.
    1.30                      Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    1.31 @@ -105,25 +105,25 @@
    1.32  *)
    1.33  
    1.34  
    1.35 -subsection{*Inductive proofs about @{term ns_shared}*}
    1.36 +subsection\<open>Inductive proofs about @{term ns_shared}\<close>
    1.37  
    1.38 -subsubsection{*Forwarding lemmas, to aid simplification*}
    1.39 +subsubsection\<open>Forwarding lemmas, to aid simplification\<close>
    1.40  
    1.41 -text{*For reasoning about the encrypted portion of message NS3*}
    1.42 +text\<open>For reasoning about the encrypted portion of message NS3\<close>
    1.43  lemma NS3_msg_in_parts_spies:
    1.44       "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
    1.45  by blast
    1.46  
    1.47 -text{*For reasoning about the Oops message*}
    1.48 +text\<open>For reasoning about the Oops message\<close>
    1.49  lemma Oops_parts_spies:
    1.50       "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
    1.51              \<Longrightarrow> K \<in> parts (spies evs)"
    1.52  by blast
    1.53  
    1.54 -text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
    1.55 -    sends messages containing @{term X}*}
    1.56 +text\<open>Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
    1.57 +    sends messages containing @{term X}\<close>
    1.58  
    1.59 -text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
    1.60 +text\<open>Spy never sees another agent's shared key! (unless it's bad at start)\<close>
    1.61  lemma Spy_see_shrK [simp]:
    1.62       "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.63  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
    1.64 @@ -134,20 +134,20 @@
    1.65  by auto
    1.66  
    1.67  
    1.68 -text{*Nobody can have used non-existent keys!*}
    1.69 +text\<open>Nobody can have used non-existent keys!\<close>
    1.70  lemma new_keys_not_used [simp]:
    1.71      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
    1.72       ==> K \<notin> keysFor (parts (spies evs))"
    1.73  apply (erule rev_mp)
    1.74  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    1.75 -txt{*Fake, NS2, NS4, NS5*}
    1.76 +txt\<open>Fake, NS2, NS4, NS5\<close>
    1.77  apply (force dest!: keysFor_parts_insert, blast+)
    1.78  done
    1.79  
    1.80  
    1.81 -subsubsection{*Lemmas concerning the form of items passed in messages*}
    1.82 +subsubsection\<open>Lemmas concerning the form of items passed in messages\<close>
    1.83  
    1.84 -text{*Describes the form of K, X and K' when the Server sends this message.*}
    1.85 +text\<open>Describes the form of K, X and K' when the Server sends this message.\<close>
    1.86  lemma Says_Server_message_form:
    1.87       "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
    1.88         evs \<in> ns_shared\<rbrakk>
    1.89 @@ -157,7 +157,7 @@
    1.90  by (erule rev_mp, erule ns_shared.induct, auto)
    1.91  
    1.92  
    1.93 -text{*If the encrypted message appears then it originated with the Server*}
    1.94 +text\<open>If the encrypted message appears then it originated with the Server\<close>
    1.95  lemma A_trusts_NS2:
    1.96       "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
    1.97         A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
    1.98 @@ -172,9 +172,9 @@
    1.99        \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   1.100  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   1.101  
   1.102 -text{*EITHER describes the form of X when the following message is sent,
   1.103 +text\<open>EITHER describes the form of X when the following message is sent,
   1.104    OR     reduces it to the Fake case.
   1.105 -  Use @{text Says_Server_message_form} if applicable.*}
   1.106 +  Use \<open>Says_Server_message_form\<close> if applicable.\<close>
   1.107  lemma Says_S_message_form:
   1.108       "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.109         evs \<in> ns_shared\<rbrakk>
   1.110 @@ -204,23 +204,23 @@
   1.111   A more general formula must be proved inductively.
   1.112  ****)
   1.113  
   1.114 -text{*NOT useful in this form, but it says that session keys are not used
   1.115 +text\<open>NOT useful in this form, but it says that session keys are not used
   1.116    to encrypt messages containing other keys, in the actual protocol.
   1.117 -  We require that agents should behave like this subsequently also.*}
   1.118 +  We require that agents should behave like this subsequently also.\<close>
   1.119  lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   1.120           (Crypt KAB X) \<in> parts (spies evs) \<and>
   1.121           Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   1.122  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   1.123 -txt{*Fake*}
   1.124 +txt\<open>Fake\<close>
   1.125  apply (blast dest: parts_insert_subset_Un)
   1.126 -txt{*Base, NS4 and NS5*}
   1.127 +txt\<open>Base, NS4 and NS5\<close>
   1.128  apply auto
   1.129  done
   1.130  
   1.131  
   1.132 -subsubsection{*Session keys are not used to encrypt other session keys*}
   1.133 +subsubsection\<open>Session keys are not used to encrypt other session keys\<close>
   1.134  
   1.135 -text{*The equality makes the induction hypothesis easier to apply*}
   1.136 +text\<open>The equality makes the induction hypothesis easier to apply\<close>
   1.137  
   1.138  lemma analz_image_freshK [rule_format]:
   1.139   "evs \<in> ns_shared \<Longrightarrow>
   1.140 @@ -230,7 +230,7 @@
   1.141  apply (erule ns_shared.induct)
   1.142  apply (drule_tac [8] Says_Server_message_form)
   1.143  apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   1.144 -txt{*NS2, NS3*}
   1.145 +txt\<open>NS2, NS3\<close>
   1.146  apply blast+ 
   1.147  done
   1.148  
   1.149 @@ -242,9 +242,9 @@
   1.150  by (simp only: analz_image_freshK analz_image_freshK_simps)
   1.151  
   1.152  
   1.153 -subsubsection{*The session key K uniquely identifies the message*}
   1.154 +subsubsection\<open>The session key K uniquely identifies the message\<close>
   1.155  
   1.156 -text{*In messages of this form, the session key uniquely identifies the rest*}
   1.157 +text\<open>In messages of this form, the session key uniquely identifies the rest\<close>
   1.158  lemma unique_session_keys:
   1.159       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.160         Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   1.161 @@ -252,9 +252,9 @@
   1.162  by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   1.163  
   1.164  
   1.165 -subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
   1.166 +subsubsection\<open>Crucial secrecy property: Spy doesn't see the keys sent in NS2\<close>
   1.167  
   1.168 -text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
   1.169 +text\<open>Beware of \<open>[rule_format]\<close> and the universal quantifier!\<close>
   1.170  lemma secrecy_lemma:
   1.171       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   1.172                                        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   1.173 @@ -268,18 +268,18 @@
   1.174  apply (frule_tac [4] Says_S_message_form)
   1.175  apply (erule_tac [5] disjE)
   1.176  apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
   1.177 -txt{*NS2*}
   1.178 +txt\<open>NS2\<close>
   1.179  apply blast
   1.180 -txt{*NS3*}
   1.181 +txt\<open>NS3\<close>
   1.182  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   1.183               dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   1.184 -txt{*Oops*}
   1.185 +txt\<open>Oops\<close>
   1.186  apply (blast dest: unique_session_keys)
   1.187  done
   1.188  
   1.189  
   1.190  
   1.191 -text{*Final version: Server's message in the most abstract form*}
   1.192 +text\<open>Final version: Server's message in the most abstract form\<close>
   1.193  lemma Spy_not_see_encrypted_key:
   1.194       "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   1.195         \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.196 @@ -288,9 +288,9 @@
   1.197  by (blast dest: Says_Server_message_form secrecy_lemma)
   1.198  
   1.199  
   1.200 -subsection{*Guarantees available at various stages of protocol*}
   1.201 +subsection\<open>Guarantees available at various stages of protocol\<close>
   1.202  
   1.203 -text{*If the encrypted message appears then it originated with the Server*}
   1.204 +text\<open>If the encrypted message appears then it originated with the Server\<close>
   1.205  lemma B_trusts_NS3:
   1.206       "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.207         B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.208 @@ -311,14 +311,14 @@
   1.209        Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.210  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.211  apply (analz_mono_contra, simp_all, blast)
   1.212 -txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   1.213 -    @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
   1.214 +txt\<open>NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   1.215 +    @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"}\<close> 
   1.216  apply (force dest!: Crypt_imp_keysFor)
   1.217 -txt{*NS4*}
   1.218 +txt\<open>NS4\<close>
   1.219  apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   1.220  done
   1.221  
   1.222 -text{*This version no longer assumes that K is secure*}
   1.223 +text\<open>This version no longer assumes that K is secure\<close>
   1.224  lemma A_trusts_NS4:
   1.225       "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   1.226         Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.227 @@ -328,9 +328,9 @@
   1.228  by (blast intro: A_trusts_NS4_lemma
   1.229            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   1.230  
   1.231 -text{*If the session key has been used in NS4 then somebody has forwarded
   1.232 +text\<open>If the session key has been used in NS4 then somebody has forwarded
   1.233    component X in some instance of NS4.  Perhaps an interesting property,
   1.234 -  but not needed (after all) for the proofs below.*}
   1.235 +  but not needed (after all) for the proofs below.\<close>
   1.236  theorem NS4_implies_NS3 [rule_format]:
   1.237    "evs \<in> ns_shared \<Longrightarrow>
   1.238       Key K \<notin> analz (spies evs) \<longrightarrow>
   1.239 @@ -341,9 +341,9 @@
   1.240  apply (drule_tac [4] NS3_msg_in_parts_spies)
   1.241  apply analz_mono_contra
   1.242  apply (simp_all add: ex_disj_distrib, blast)
   1.243 -txt{*NS2*}
   1.244 +txt\<open>NS2\<close>
   1.245  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   1.246 -txt{*NS4*}
   1.247 +txt\<open>NS4\<close>
   1.248  apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   1.249  done
   1.250  
   1.251 @@ -359,16 +359,16 @@
   1.252  apply (erule ns_shared.induct, force)
   1.253  apply (drule_tac [4] NS3_msg_in_parts_spies)
   1.254  apply (analz_mono_contra, simp_all, blast)
   1.255 -txt{*NS2*}
   1.256 +txt\<open>NS2\<close>
   1.257  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   1.258 -txt{*NS5*}
   1.259 +txt\<open>NS5\<close>
   1.260  apply (blast dest!: A_trusts_NS2
   1.261               dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.262                     unique_session_keys Crypt_Spy_analz_bad)
   1.263  done
   1.264  
   1.265  
   1.266 -text{*Very strong Oops condition reveals protocol's weakness*}
   1.267 +text\<open>Very strong Oops condition reveals protocol's weakness\<close>
   1.268  lemma B_trusts_NS5:
   1.269       "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   1.270         Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.271 @@ -378,9 +378,9 @@
   1.272  by (blast intro: B_trusts_NS5_lemma
   1.273            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   1.274  
   1.275 -text{*Unaltered so far wrt original version*}
   1.276 +text\<open>Unaltered so far wrt original version\<close>
   1.277  
   1.278 -subsection{*Lemmas for reasoning about predicate "Issues"*}
   1.279 +subsection\<open>Lemmas for reasoning about predicate "Issues"\<close>
   1.280  
   1.281  lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
   1.282  apply (induct_tac "evs")
   1.283 @@ -414,15 +414,15 @@
   1.284  apply (induct_tac "evs")
   1.285  apply (rename_tac [2] a b)
   1.286  apply (induct_tac [2] "a", auto)
   1.287 -txt{* Resembles @{text"used_subset_append"} in theory Event.*}
   1.288 +txt\<open>Resembles \<open>used_subset_append\<close> in theory Event.\<close>
   1.289  done
   1.290  
   1.291  lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
   1.292  
   1.293  
   1.294 -subsection{*Guarantees of non-injective agreement on the session key, and
   1.295 +subsection\<open>Guarantees of non-injective agreement on the session key, and
   1.296  of key distribution. They also express forms of freshness of certain messages,
   1.297 -namely that agents were alive after something happened.*}
   1.298 +namely that agents were alive after something happened.\<close>
   1.299  
   1.300  lemma B_Issues_A:
   1.301       "\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs;
   1.302 @@ -437,24 +437,24 @@
   1.303  apply (erule rev_mp)
   1.304  apply (erule ns_shared.induct, analz_mono_contra)
   1.305  apply (simp_all)
   1.306 -txt{*fake*}
   1.307 +txt\<open>fake\<close>
   1.308  apply blast
   1.309  apply (simp_all add: takeWhile_tail)
   1.310 -txt{*NS3 remains by pure coincidence!*}
   1.311 +txt\<open>NS3 remains by pure coincidence!\<close>
   1.312  apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   1.313 -txt{*NS4 would be the non-trivial case can be solved by Nb being used*}
   1.314 +txt\<open>NS4 would be the non-trivial case can be solved by Nb being used\<close>
   1.315  apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
   1.316                     parts_spies_evs_revD2 [THEN subsetD])
   1.317  done
   1.318  
   1.319 -text{*Tells A that B was alive after she sent him the session key.  The
   1.320 +text\<open>Tells A that B was alive after she sent him the session key.  The
   1.321  session key must be assumed confidential for this deduction to be meaningful,
   1.322  but that assumption can be relaxed by the appropriate argument.
   1.323  
   1.324  Precisely, the theorem guarantees (to A) key distribution of the session key
   1.325  to B. It also guarantees (to A) non-injective agreement of B with A on the
   1.326  session key. Both goals are available to A in the sense of Goal Availability.
   1.327 -*}
   1.328 +\<close>
   1.329  lemma A_authenticates_and_keydist_to_B:
   1.330       "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   1.331         Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.332 @@ -474,13 +474,13 @@
   1.333  apply (erule rev_mp)
   1.334  apply (erule ns_shared.induct, analz_mono_contra)
   1.335  apply (simp_all)
   1.336 -txt{*Fake*}
   1.337 +txt\<open>Fake\<close>
   1.338  apply blast
   1.339 -txt{*NS2*}
   1.340 +txt\<open>NS2\<close>
   1.341  apply (force dest!: Crypt_imp_keysFor)
   1.342 -txt{*NS3*}
   1.343 +txt\<open>NS3\<close>
   1.344  apply (metis NS3_msg_in_parts_spies parts_cut_eq)
   1.345 -txt{*NS5, the most important case, can be solved by unicity*}
   1.346 +txt\<open>NS5, the most important case, can be solved by unicity\<close>
   1.347  apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
   1.348  done
   1.349  
   1.350 @@ -497,20 +497,20 @@
   1.351  apply (erule rev_mp)
   1.352  apply (erule ns_shared.induct, analz_mono_contra)
   1.353  apply (simp_all)
   1.354 -txt{*fake*}
   1.355 +txt\<open>fake\<close>
   1.356  apply blast
   1.357  apply (simp_all add: takeWhile_tail)
   1.358 -txt{*NS3 remains by pure coincidence!*}
   1.359 +txt\<open>NS3 remains by pure coincidence!\<close>
   1.360  apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   1.361 -txt{*NS5 is the non-trivial case and cannot be solved as in @{term B_Issues_A}! because NB is not fresh. We need @{term A_trusts_NS5}, proved for this very purpose*}
   1.362 +txt\<open>NS5 is the non-trivial case and cannot be solved as in @{term B_Issues_A}! because NB is not fresh. We need @{term A_trusts_NS5}, proved for this very purpose\<close>
   1.363  apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
   1.364          parts_spies_evs_revD2 [THEN subsetD])
   1.365  done
   1.366  
   1.367 -text{*Tells B that A was alive after B issued NB.
   1.368 +text\<open>Tells B that A was alive after B issued NB.
   1.369  
   1.370  Precisely, the theorem guarantees (to B) key distribution of the session key to A. It also guarantees (to B) non-injective agreement of A with B on the session key. Both goals are available to B in the sense of Goal Availability.
   1.371 -*}
   1.372 +\<close>
   1.373  lemma B_authenticates_and_keydist_to_A:
   1.374       "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   1.375         Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);