src/HOL/Auth/NS_Shared.thy
author nipkow
Fri Oct 07 20:41:10 2005 +0200 (2005-10-07)
changeset 17778 93d7e524417a
parent 16417 9bc16273c2d4
child 18886 9f27383426db
permissions -rw-r--r--
changes due to new neq_simproc in simpdata.ML
     1 (*  Title:      HOL/Auth/NS_Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header{*The Needham-Schroeder Shared-Key Protocol*}
     8 
     9 theory NS_Shared imports Public begin
    10 
    11 text{*
    12 From page 247 of
    13   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    14   Proc. Royal Soc. 426
    15 *}
    16 
    17 consts  ns_shared   :: "event list set"
    18 inductive "ns_shared"
    19  intros
    20 	(*Initial trace is empty*)
    21   Nil:  "[] \<in> ns_shared"
    22 	(*The spy MAY say anything he CAN say.  We do not expect him to
    23 	  invent new nonces here, but he can also use NS1.  Common to
    24 	  all similar protocols.*)
    25   Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    26 	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    27 
    28 	(*Alice initiates a protocol run, requesting to talk to any B*)
    29   NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    30 	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    31 
    32 	(*Server's response to Alice's message.
    33 	  !! It may respond more than once to A's request !!
    34 	  Server doesn't know who the true sender is, hence the A' in
    35 	      the sender field.*)
    36   NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    37 	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    38 	 \<Longrightarrow> Says Server A
    39 	       (Crypt (shrK A)
    40 		  \<lbrace>Nonce NA, Agent B, Key KAB,
    41 		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
    42 	       # evs2 \<in> ns_shared"
    43 
    44 	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    45 	   Need A \<noteq> Server because we allow messages to self.*)
    46   NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    47 	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    48 	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    49 	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    50 
    51 	(*Bob's nonce exchange.  He does not know who the message came
    52 	  from, but responds to A because she is mentioned inside.*)
    53   NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
    54 	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    55 	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    56 
    57 	(*Alice responds with Nonce NB if she has seen the key before.
    58 	  Maybe should somehow check Nonce NA again.
    59 	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    60 	  Letting the Spy add or subtract 1 lets him send all nonces.
    61 	  Instead we distinguish the messages by sending the nonce twice.*)
    62   NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
    63 	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    64 	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    65 	    \<in> set evs5\<rbrakk>
    66 	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    67 
    68 	(*This message models possible leaks of session keys.
    69 	  The two Nonces identify the protocol run: the rule insists upon
    70 	  the true senders in order to make them accurate.*)
    71   Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    72 	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    73 	      \<in> set evso\<rbrakk>
    74 	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    75 
    76 
    77 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    78 declare parts.Body  [dest]
    79 declare Fake_parts_insert_in_Un  [dest]
    80 declare analz_into_parts [dest]
    81 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    82 
    83 
    84 text{*A "possibility property": there are traces that reach the end*}
    85 lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
    86        ==> \<exists>N. \<exists>evs \<in> ns_shared.
    87                     Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    88 apply (intro exI bexI)
    89 apply (rule_tac [2] ns_shared.Nil
    90        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    91 	THEN ns_shared.NS4, THEN ns_shared.NS5])
    92 apply (possibility, simp add: used_Cons)
    93 done
    94 
    95 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    96 lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
    97                 Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
    98 *)
    99 
   100 
   101 subsection{*Inductive proofs about @{term ns_shared}*}
   102 
   103 subsubsection{*Forwarding lemmas, to aid simplification*}
   104 
   105 text{*For reasoning about the encrypted portion of message NS3*}
   106 lemma NS3_msg_in_parts_spies:
   107      "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   108 by blast
   109 
   110 text{*For reasoning about the Oops message*}
   111 lemma Oops_parts_spies:
   112      "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   113             \<Longrightarrow> K \<in> parts (spies evs)"
   114 by blast
   115 
   116 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
   117     sends messages containing @{term X}*}
   118 
   119 text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   120 lemma Spy_see_shrK [simp]:
   121      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   122 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
   123 done
   124 
   125 lemma Spy_analz_shrK [simp]:
   126      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   127 by auto
   128 
   129 
   130 text{*Nobody can have used non-existent keys!*}
   131 lemma new_keys_not_used [simp]:
   132     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
   133      ==> K \<notin> keysFor (parts (spies evs))"
   134 apply (erule rev_mp)
   135 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   136 txt{*Fake, NS2, NS4, NS5*}
   137 apply (force dest!: keysFor_parts_insert, blast+)
   138 done
   139 
   140 
   141 subsubsection{*Lemmas concerning the form of items passed in messages*}
   142 
   143 text{*Describes the form of K, X and K' when the Server sends this message.*}
   144 lemma Says_Server_message_form:
   145      "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   146        evs \<in> ns_shared\<rbrakk>
   147       \<Longrightarrow> K \<notin> range shrK \<and>
   148           X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   149           K' = shrK A"
   150 by (erule rev_mp, erule ns_shared.induct, auto)
   151 
   152 
   153 text{*If the encrypted message appears then it originated with the Server*}
   154 lemma A_trusts_NS2:
   155      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   156        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   157       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   158 apply (erule rev_mp)
   159 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   160 done
   161 
   162 lemma cert_A_form:
   163      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   164        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   165       \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   166 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   167 
   168 text{*EITHER describes the form of X when the following message is sent,
   169   OR     reduces it to the Fake case.
   170   Use @{text Says_Server_message_form} if applicable.*}
   171 lemma Says_S_message_form:
   172      "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   173        evs \<in> ns_shared\<rbrakk>
   174       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   175           \<or> X \<in> analz (spies evs)"
   176 by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
   177 
   178 
   179 (*Alternative version also provable
   180 lemma Says_S_message_form2:
   181   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   182     evs \<in> ns_shared\<rbrakk>
   183    \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
   184        \<or> X \<in> analz (spies evs)"
   185 apply (case_tac "A \<in> bad")
   186 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
   187 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   188 *)
   189 
   190 
   191 (****
   192  SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
   193 
   194   Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
   195   Key K \<in> analz (spies evs)
   196 
   197  A more general formula must be proved inductively.
   198 ****)
   199 
   200 text{*NOT useful in this form, but it says that session keys are not used
   201   to encrypt messages containing other keys, in the actual protocol.
   202   We require that agents should behave like this subsequently also.*}
   203 lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   204          (Crypt KAB X) \<in> parts (spies evs) \<and>
   205          Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   206 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   207 txt{*Fake*}
   208 apply (blast dest: parts_insert_subset_Un)
   209 txt{*Base, NS4 and NS5*}
   210 apply auto
   211 done
   212 
   213 
   214 subsubsection{*Session keys are not used to encrypt other session keys*}
   215 
   216 text{*The equality makes the induction hypothesis easier to apply*}
   217 
   218 lemma analz_image_freshK [rule_format]:
   219  "evs \<in> ns_shared \<Longrightarrow>
   220    \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   221              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   222              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   223 apply (erule ns_shared.induct)
   224 apply (drule_tac [8] Says_Server_message_form)
   225 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   226 txt{*NS2, NS3*}
   227 apply blast+; 
   228 done
   229 
   230 
   231 lemma analz_insert_freshK:
   232      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   233        (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   234        (K = KAB \<or> Key K \<in> analz (spies evs))"
   235 by (simp only: analz_image_freshK analz_image_freshK_simps)
   236 
   237 
   238 subsubsection{*The session key K uniquely identifies the message*}
   239 
   240 text{*In messages of this form, the session key uniquely identifies the rest*}
   241 lemma unique_session_keys:
   242      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   243        Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   244        evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   245 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   246 done
   247 
   248 
   249 subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
   250 
   251 text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
   252 lemma secrecy_lemma:
   253      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   254                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   255               \<in> set evs;
   256          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   257       \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   258          Key K \<notin> analz (spies evs)"
   259 apply (erule rev_mp)
   260 apply (erule ns_shared.induct, force)
   261 apply (frule_tac [7] Says_Server_message_form)
   262 apply (frule_tac [4] Says_S_message_form)
   263 apply (erule_tac [5] disjE)
   264 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
   265 txt{*NS2*}
   266 apply blast
   267 txt{*NS3, Server sub-case*}
   268 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   269 	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   270 txt{*NS3, Spy sub-case; also Oops*}
   271 apply (blast dest: unique_session_keys)+
   272 done
   273 
   274 
   275 
   276 text{*Final version: Server's message in the most abstract form*}
   277 lemma Spy_not_see_encrypted_key:
   278      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   279        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   280        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   281       \<Longrightarrow> Key K \<notin> analz (spies evs)"
   282 by (blast dest: Says_Server_message_form secrecy_lemma)
   283 
   284 
   285 subsection{*Guarantees available at various stages of protocol*}
   286 
   287 text{*If the encrypted message appears then it originated with the Server*}
   288 lemma B_trusts_NS3:
   289      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   290        B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   291       \<Longrightarrow> \<exists>NA. Says Server A
   292                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   293                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   294               \<in> set evs"
   295 apply (erule rev_mp)
   296 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   297 done
   298 
   299 
   300 lemma A_trusts_NS4_lemma [rule_format]:
   301    "evs \<in> ns_shared \<Longrightarrow>
   302       Key K \<notin> analz (spies evs) \<longrightarrow>
   303       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   304       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   305       Says B A (Crypt K (Nonce NB)) \<in> set evs"
   306 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   307 apply (analz_mono_contra, simp_all, blast)
   308 txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   309     @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
   310 apply (force dest!: Crypt_imp_keysFor)
   311 txt{*NS4*}
   312 apply (blast dest: B_trusts_NS3
   313 	           Says_imp_knows_Spy [THEN analz.Inj]
   314                    Crypt_Spy_analz_bad unique_session_keys)
   315 done
   316 
   317 text{*This version no longer assumes that K is secure*}
   318 lemma A_trusts_NS4:
   319      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   320        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   321        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   322        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   323       \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   324 by (blast intro: A_trusts_NS4_lemma
   325           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   326 
   327 text{*If the session key has been used in NS4 then somebody has forwarded
   328   component X in some instance of NS4.  Perhaps an interesting property,
   329   but not needed (after all) for the proofs below.*}
   330 theorem NS4_implies_NS3 [rule_format]:
   331   "evs \<in> ns_shared \<Longrightarrow>
   332      Key K \<notin> analz (spies evs) \<longrightarrow>
   333      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   334      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   335      (\<exists>A'. Says A' B X \<in> set evs)"
   336 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   337 apply (simp_all add: ex_disj_distrib, blast)
   338 txt{*NS2*}
   339 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   340 txt{*NS4*}
   341 apply (blast dest: B_trusts_NS3
   342 	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   343                    unique_session_keys Crypt_Spy_analz_bad)
   344 done
   345 
   346 
   347 lemma B_trusts_NS5_lemma [rule_format]:
   348   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   349      Key K \<notin> analz (spies evs) \<longrightarrow>
   350      Says Server A
   351 	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   352 			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   353      Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   354      Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   355 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
   356 txt{*NS2*}
   357 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   358 txt{*NS5*}
   359 apply (blast dest!: A_trusts_NS2
   360 	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   361                    unique_session_keys Crypt_Spy_analz_bad)
   362 done
   363 
   364 
   365 text{*Very strong Oops condition reveals protocol's weakness*}
   366 lemma B_trusts_NS5:
   367      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   368        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   369        \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   370        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   371       \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   372 by (blast intro: B_trusts_NS5_lemma
   373           dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   374 
   375 end