src/HOL/Auth/NS_Shared.thy
changeset 18886 9f27383426db
parent 17778 93d7e524417a
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Feb 01 12:23:14 2006 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Feb 01 15:22:02 2006 +0100
     1.3 @@ -1,10 +1,10 @@
     1.4  (*  Title:      HOL/Auth/NS_Shared
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author:     Lawrence C Paulson and Giampaolo Bella 
     1.8      Copyright   1996  University of Cambridge
     1.9  *)
    1.10  
    1.11 -header{*The Needham-Schroeder Shared-Key Protocol*}
    1.12 +header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
    1.13  
    1.14  theory NS_Shared imports Public begin
    1.15  
    1.16 @@ -14,6 +14,17 @@
    1.17    Proc. Royal Soc. 426
    1.18  *}
    1.19  
    1.20 +constdefs
    1.21 +
    1.22 + (* A is the true creator of X if she has sent X and X never appeared on
    1.23 +    the trace before this event. Recall that traces grow from head. *)
    1.24 +  Issues :: "[agent, agent, msg, event list] => bool"
    1.25 +             ("_ Issues _ with _ on _")
    1.26 +   "A Issues B with X on evs ==
    1.27 +      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
    1.28 +      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
    1.29 +
    1.30 +
    1.31  consts  ns_shared   :: "event list set"
    1.32  inductive "ns_shared"
    1.33   intros
    1.34 @@ -242,11 +253,10 @@
    1.35       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
    1.36         Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
    1.37         evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
    1.38 -apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
    1.39 -done
    1.40 +by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
    1.41  
    1.42  
    1.43 -subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
    1.44 +subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
    1.45  
    1.46  text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
    1.47  lemma secrecy_lemma:
    1.48 @@ -333,7 +343,9 @@
    1.49       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
    1.50       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
    1.51       (\<exists>A'. Says A' B X \<in> set evs)"
    1.52 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
    1.53 +apply (erule ns_shared.induct, force)
    1.54 +apply (drule_tac [4] NS3_msg_in_parts_spies)
    1.55 +apply analz_mono_contra
    1.56  apply (simp_all add: ex_disj_distrib, blast)
    1.57  txt{*NS2*}
    1.58  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
    1.59 @@ -352,7 +364,9 @@
    1.60  			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
    1.61       Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
    1.62       Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
    1.63 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
    1.64 +apply (erule ns_shared.induct, force)
    1.65 +apply (drule_tac [4] NS3_msg_in_parts_spies)
    1.66 +apply (analz_mono_contra, simp_all, blast)
    1.67  txt{*NS2*}
    1.68  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
    1.69  txt{*NS5*}
    1.70 @@ -372,4 +386,143 @@
    1.71  by (blast intro: B_trusts_NS5_lemma
    1.72            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
    1.73  
    1.74 +text{*Unaltered so far wrt original version*}
    1.75 +
    1.76 +subsection{*Lemmas for reasoning about predicate "Issues"*}
    1.77 +
    1.78 +lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
    1.79 +apply (induct_tac "evs")
    1.80 +apply (induct_tac [2] "a", auto)
    1.81 +done
    1.82 +
    1.83 +lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
    1.84 +apply (induct_tac "evs")
    1.85 +apply (induct_tac [2] "a", auto)
    1.86 +done
    1.87 +
    1.88 +lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
    1.89 +          (if A:bad then insert X (spies evs) else spies evs)"
    1.90 +apply (induct_tac "evs")
    1.91 +apply (induct_tac [2] "a", auto)
    1.92 +done
    1.93 +
    1.94 +lemma spies_evs_rev: "spies evs = spies (rev evs)"
    1.95 +apply (induct_tac "evs")
    1.96 +apply (induct_tac [2] "a")
    1.97 +apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
    1.98 +done
    1.99 +
   1.100 +lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
   1.101 +
   1.102 +lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
   1.103 +apply (induct_tac "evs")
   1.104 +apply (induct_tac [2] "a", auto)
   1.105 +txt{* Resembles @{text"used_subset_append"} in theory Event.*}
   1.106 +done
   1.107 +
   1.108 +lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
   1.109 +
   1.110 +
   1.111 +subsection{*Guarantees of non-injective agreement on the session key, and
   1.112 +of key distribution. They also express forms of freshness of certain messages,
   1.113 +namely that agents were alive after something happened.*}
   1.114 +
   1.115 +lemma B_Issues_A:
   1.116 +     "\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs;
   1.117 +         Key K \<notin> analz (spies evs);
   1.118 +         A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   1.119 +      \<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs"
   1.120 +apply (simp (no_asm) add: Issues_def)
   1.121 +apply (rule exI)
   1.122 +apply (rule conjI, assumption)
   1.123 +apply (simp (no_asm))
   1.124 +apply (erule rev_mp)
   1.125 +apply (erule rev_mp)
   1.126 +apply (erule ns_shared.induct, analz_mono_contra)
   1.127 +apply (simp_all)
   1.128 +txt{*fake*}
   1.129 +apply blast
   1.130 +apply (simp_all add: takeWhile_tail)
   1.131 +txt{*NS3 remains by pure coincidence!*}
   1.132 +apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   1.133 +txt{*NS4 would be the non-trivial case can be solved by Nb being used*}
   1.134 +apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
   1.135 +                   parts_spies_evs_revD2 [THEN subsetD])
   1.136 +done
   1.137 +
   1.138 +text{*Tells A that B was alive after she sent him the session key.  The
   1.139 +session key must be assumed confidential for this deduction to be meaningful,
   1.140 +but that assumption can be relaxed by the appropriate argument.
   1.141 +
   1.142 +Precisely, the theorem guarantees (to A) key distribution of the session key
   1.143 +to B. It also guarantees (to A) non-injective agreement of B with A on the
   1.144 +session key. Both goals are available to A in the sense of Goal Availability.
   1.145 +*}
   1.146 +lemma A_authenticates_and_keydist_to_B:
   1.147 +     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   1.148 +       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   1.149 +       Key K \<notin> analz(knows Spy evs);
   1.150 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.151 +      \<Longrightarrow> B Issues A with (Crypt K (Nonce NB)) on evs"
   1.152 +by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)
   1.153 +
   1.154 +lemma A_trusts_NS5:
   1.155 +  "\<lbrakk> Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts(spies evs);
   1.156 +     Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
   1.157 +     Key K \<notin> analz (spies evs);
   1.158 +     A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   1.159 + \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
   1.160 +apply (erule rev_mp)
   1.161 +apply (erule rev_mp)
   1.162 +apply (erule rev_mp)
   1.163 +apply (erule ns_shared.induct, analz_mono_contra)
   1.164 +apply (frule_tac [5] Says_S_message_form)
   1.165 +apply (simp_all)
   1.166 +txt{*Fake*}
   1.167 +apply blast
   1.168 +txt{*NS2*}
   1.169 +apply (force dest!: Crypt_imp_keysFor)
   1.170 +txt{*NS3, much quicker having installed @{term Says_S_message_form} before simplication*}
   1.171 +apply fastsimp
   1.172 +txt{*NS5, the most important case, can be solved by unicity*}
   1.173 +apply (case_tac "Aa \<in> bad")
   1.174 +apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
   1.175 +apply (blast dest: A_trusts_NS2 unique_session_keys)
   1.176 +done
   1.177 +
   1.178 +lemma A_Issues_B:
   1.179 +     "\<lbrakk> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs;
   1.180 +        Key K \<notin> analz (spies evs);
   1.181 +        A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   1.182 +    \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
   1.183 +apply (simp (no_asm) add: Issues_def)
   1.184 +apply (rule exI)
   1.185 +apply (rule conjI, assumption)
   1.186 +apply (simp (no_asm))
   1.187 +apply (erule rev_mp)
   1.188 +apply (erule rev_mp)
   1.189 +apply (erule ns_shared.induct, analz_mono_contra)
   1.190 +apply (simp_all)
   1.191 +txt{*fake*}
   1.192 +apply blast
   1.193 +apply (simp_all add: takeWhile_tail)
   1.194 +txt{*NS3 remains by pure coincidence!*}
   1.195 +apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   1.196 +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.197 +apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
   1.198 +        parts_spies_evs_revD2 [THEN subsetD])
   1.199 +done
   1.200 +
   1.201 +text{*Tells B that A was alive after B issued NB.
   1.202 +
   1.203 +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.204 +*}
   1.205 +lemma B_authenticates_and_keydist_to_A:
   1.206 +     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   1.207 +       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   1.208 +       Key K \<notin> analz (spies evs);
   1.209 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.210 +   \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
   1.211 +by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)
   1.212 +
   1.213  end