src/HOL/Auth/NS_Shared.thy
author paulson
Wed Feb 14 13:01:02 2001 +0100 (2001-02-14)
changeset 11117 55358999077d
parent 11104 f2024fed9f0c
child 11150 67387142225e
permissions -rw-r--r--
tidying
     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>evs \<in> ns_shared;  X \<in> synth (analz (spies evs))\<rbrakk>
    24 	 \<Longrightarrow> Says Spy B X # evs \<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 declare knows_Spy_partsEs [elim]
    75 declare analz_subset_parts [THEN subsetD, dest]
    76 declare Fake_parts_insert [THEN subsetD, dest]
    77 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    78 
    79 
    80 (*A "possibility property": there are traces that reach the end*)
    81 lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
    82                               Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    83 apply (intro exI bexI)
    84 apply (rule_tac [2] ns_shared.Nil
    85        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    86 	THEN ns_shared.NS4, THEN ns_shared.NS5])
    87 apply possibility
    88 done
    89 
    90 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    91 lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
    92                 Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
    93 *)
    94 
    95 
    96 (**** Inductive proofs about ns_shared ****)
    97 
    98 (*Forwarding lemmas, to aid simplification*)
    99 
   100 (*For reasoning about the encrypted portion of message NS3*)
   101 lemma NS3_msg_in_parts_spies:
   102      "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   103 by blast
   104                               
   105 (*For reasoning about the Oops message*)
   106 lemma Oops_parts_spies:
   107      "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   108             \<Longrightarrow> K \<in> parts (spies evs)"
   109 by blast
   110 
   111 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   112     sends messages containing X! **)
   113 
   114 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
   115 lemma Spy_see_shrK [simp]:
   116      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   117 apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
   118 apply simp_all
   119 apply blast+;
   120 done
   121 
   122 
   123 lemma Spy_analz_shrK [simp]:
   124      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   125 by auto
   126 
   127 
   128 (*Nobody can have used non-existent keys!*)
   129 lemma new_keys_not_used [rule_format, simp]:
   130     "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
   131 apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
   132 apply simp_all
   133 (*Fake, NS2, NS4, NS5*)
   134 apply (blast dest!: keysFor_parts_insert)+
   135 done
   136 
   137 
   138 (** Lemmas concerning the form of items passed in messages **)
   139 
   140 (*Describes the form of K, X and K' when the Server sends this message.*)
   141 lemma Says_Server_message_form:
   142      "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   143        evs \<in> ns_shared\<rbrakk>
   144       \<Longrightarrow> K \<notin> range shrK \<and>
   145           X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   146           K' = shrK A"
   147 by (erule rev_mp, erule ns_shared.induct, auto)
   148 
   149 
   150 (*If the encrypted message appears then it originated with the Server*)
   151 lemma A_trusts_NS2:
   152      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   153        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   154       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   155 apply (erule rev_mp)
   156 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   157 apply auto
   158 done
   159 
   160 lemma cert_A_form:
   161      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   162        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   163       \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   164 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   165 
   166 (*EITHER describes the form of X when the following message is sent,
   167   OR     reduces it to the Fake case.
   168   Use Says_Server_message_form if applicable.*)
   169 lemma Says_S_message_form:
   170      "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   171        evs \<in> ns_shared\<rbrakk>
   172       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   173           \<or> X \<in> analz (spies evs)"
   174 apply (frule Says_imp_knows_Spy)
   175 (*mystery: why is this frule needed?*)
   176 apply (blast dest: cert_A_form analz.Inj)
   177 done
   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 (*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, frule_tac [4] NS3_msg_in_parts_spies)
   207 apply simp_all
   208 (*Fake*)
   209 apply (blast dest: parts_insert_subset_Un)
   210 (*Base, NS4 and NS5*)
   211 apply auto
   212 done
   213 
   214 
   215 (** Session keys are not used to encrypt other session keys **)
   216 
   217 (*The equality makes the induction hypothesis easier to apply*)
   218 
   219 lemma analz_image_freshK [rule_format]:
   220  "evs \<in> ns_shared \<Longrightarrow>
   221    \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   222              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   223              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   224 apply (erule ns_shared.induct, force)
   225 apply (frule_tac [7] Says_Server_message_form)
   226 apply (erule_tac [4] Says_S_message_form [THEN disjE])
   227 apply analz_freshK
   228 apply spy_analz
   229 done
   230 
   231 
   232 lemma analz_insert_freshK:
   233      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   234        Key K \<in> analz (insert (Key KAB) (spies evs)) =
   235        (K = KAB \<or> Key K \<in> analz (spies evs))"
   236 by (simp only: analz_image_freshK analz_image_freshK_simps)
   237 
   238 
   239 (** The session key K uniquely identifies the message **)
   240 
   241 (*In messages of this form, the session key uniquely identifies the rest*)
   242 lemma unique_session_keys:
   243      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   244        Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   245        evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   246 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
   247 apply simp_all
   248 apply blast+
   249 done
   250 
   251 
   252 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   253 
   254 lemma secrecy_lemma [rule_format]:
   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 6 **)
   270 apply clarify
   271 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
   272 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
   273 apply assumption
   274 apply (blast dest: unique_session_keys)+ (*also proves Oops*)
   275 done
   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 apply (frule Says_Server_message_form, assumption)
   285 apply (auto dest: Says_Server_message_form secrecy_lemma)
   286 done
   287 
   288 
   289 (**** Guarantees available at various stages of protocol ***)
   290 
   291 (*If the encrypted message appears then it originated with the Server*)
   292 lemma B_trusts_NS3:
   293      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   294             B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   295           \<Longrightarrow> \<exists>NA. Says Server A
   296                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   297                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   298               \<in> set evs"
   299 apply (erule rev_mp)
   300 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   301 apply auto
   302 done
   303 
   304 
   305 lemma A_trusts_NS4_lemma [rule_format]:
   306    "evs \<in> ns_shared \<Longrightarrow>
   307       Key K \<notin> analz (spies evs) \<longrightarrow>
   308       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   309       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   310       Says B A (Crypt K (Nonce NB)) \<in> set evs"
   311 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   312 apply analz_mono_contra
   313 apply simp_all
   314 apply blast     (*Fake*)
   315 (*NS2: contradiction from the assumptions  
   316   Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   317 apply (force dest!: Crypt_imp_keysFor) 
   318 apply blast     (*NS3*)
   319 (*NS4*)
   320 apply clarify;
   321 apply (frule Says_imp_knows_Spy [THEN analz.Inj])
   322 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
   323                    B_trusts_NS3 unique_session_keys)
   324 done
   325 
   326 (*This version no longer assumes that K is secure*)
   327 lemma A_trusts_NS4:
   328      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   329        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   330        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   331        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   332       \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   333 by (blast intro: A_trusts_NS4_lemma 
   334           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   335 
   336 (*If the session key has been used in NS4 then somebody has forwarded
   337   component X in some instance of NS4.  Perhaps an interesting property, 
   338   but not needed (after all) for the proofs below.*)
   339 theorem NS4_implies_NS3 [rule_format]:
   340   "evs \<in> ns_shared \<Longrightarrow> 
   341      Key K \<notin> analz (spies evs) \<longrightarrow>
   342      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   343      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   344      (\<exists>A'. Says A' B X \<in> set evs)"
   345 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   346 apply analz_mono_contra
   347 apply (simp_all add: ex_disj_distrib)
   348 apply blast  (*Fake*)
   349 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   350 apply blast  (*NS3*)
   351 (*NS4*)
   352 apply (case_tac "Ba \<in> bad")
   353 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
   354 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], 
   355        assumption+)
   356 apply (blast dest: unique_session_keys)
   357 done
   358 
   359 
   360 lemma B_trusts_NS5_lemma [rule_format]:
   361   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   362      Key K \<notin> analz (spies evs) \<longrightarrow>
   363      Says Server A
   364 	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   365 			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   366      Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   367      Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   368 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   369 apply analz_mono_contra
   370 apply simp_all 
   371 apply blast  (*Fake*)
   372 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   373 apply (blast dest!: cert_A_form) (*NS3*)
   374 (**LEVEL 5**)
   375 (*NS5*)
   376 apply clarify
   377 apply (case_tac "Aa \<in> bad")
   378 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
   379 apply (blast dest: A_trusts_NS2 unique_session_keys)
   380 done
   381 
   382 
   383 (*Very strong Oops condition reveals protocol's weakness*)
   384 lemma B_trusts_NS5:
   385      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   386        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   387        \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   388        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   389       \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   390 apply (drule B_trusts_NS3, clarify+)
   391 apply (blast intro: B_trusts_NS5_lemma 
   392              dest: dest: Spy_not_see_encrypted_key)
   393 (*surprisingly delicate proof due to quantifier interactions*)
   394 done
   395 
   396 end