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