src/HOL/Auth/NS_Shared.thy
author paulson
Tue Sep 23 15:41:33 2003 +0200 (2003-09-23)
changeset 14200 d8598e24f8fa
parent 13956 8fe7e12290e1
child 14207 f20fbb141673
permissions -rw-r--r--
Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
     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 all 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 text{*A "possibility property": there are traces that reach the end*}
    83 lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
    84        ==> \<exists>N. \<exists>evs \<in> ns_shared.
    85                     Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    86 apply (intro exI bexI)
    87 apply (rule_tac [2] ns_shared.Nil
    88        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    89 	THEN ns_shared.NS4, THEN ns_shared.NS5])
    90 apply (possibility, simp add: used_Cons) 
    91 done
    92 
    93 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    94 lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
    95                 Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
    96 *)
    97 
    98 
    99 subsection{*Inductive proofs about @{term ns_shared}*}
   100 
   101 subsubsection{*Forwarding lemmas, to aid simplification*}
   102 
   103 text{*For reasoning about the encrypted portion of message NS3*}
   104 lemma NS3_msg_in_parts_spies:
   105      "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   106 by blast
   107 
   108 text{*For reasoning about the Oops message*}
   109 lemma Oops_parts_spies:
   110      "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   111             \<Longrightarrow> K \<in> parts (spies evs)"
   112 by blast
   113 
   114 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
   115     sends messages containing @{term X}*}
   116 
   117 text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   118 lemma Spy_see_shrK [simp]:
   119      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   120 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
   121 done
   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 text{*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, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   132 txt{*Fake, NS2, NS4, NS5*}
   133 apply (force dest!: keysFor_parts_insert, blast+)
   134 done
   135 
   136 
   137 subsubsection{*Lemmas concerning the form of items passed in messages*}
   138 
   139 text{*Describes the form of K, X and K' when the Server sends this message.*}
   140 lemma Says_Server_message_form:
   141      "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   142        evs \<in> ns_shared\<rbrakk>
   143       \<Longrightarrow> K \<notin> range shrK \<and>
   144           X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   145           K' = shrK A"
   146 by (erule rev_mp, erule ns_shared.induct, auto)
   147 
   148 
   149 text{*If the encrypted message appears then it originated with the Server*}
   150 lemma A_trusts_NS2:
   151      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   152        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   153       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   154 apply (erule rev_mp)
   155 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   156 done
   157 
   158 lemma cert_A_form:
   159      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   160        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   161       \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   162 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   163 
   164 (*EITHER describes the form of X when the following message is sent,
   165   OR     reduces it to the Fake case.
   166   Use Says_Server_message_form if applicable.*)
   167 lemma Says_S_message_form:
   168      "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   169        evs \<in> ns_shared\<rbrakk>
   170       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   171           \<or> X \<in> analz (spies evs)"
   172 by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
   173 
   174 
   175 (*Alternative version also provable
   176 lemma Says_S_message_form2:
   177   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   178     evs \<in> ns_shared\<rbrakk>
   179    \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
   180        \<or> X \<in> analz (spies evs)"
   181 apply (case_tac "A \<in> bad")
   182 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
   183 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   184 *)
   185 
   186 
   187 (****
   188  SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
   189 
   190   Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
   191   Key K \<in> analz (spies evs)
   192 
   193  A more general formula must be proved inductively.
   194 ****)
   195 
   196 text{*NOT useful in this form, but it says that session keys are not used
   197   to encrypt messages containing other keys, in the actual protocol.
   198   We require that agents should behave like this subsequently also.*}
   199 lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   200          (Crypt KAB X) \<in> parts (spies evs) \<and>
   201          Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   202 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   203 txt{*Fake*}
   204 apply (blast dest: parts_insert_subset_Un)
   205 txt{*Base, NS4 and NS5*}
   206 apply auto
   207 done
   208 
   209 
   210 subsubsection{*Session keys are not used to encrypt other session keys*}
   211 
   212 text{*The equality makes the induction hypothesis easier to apply*}
   213 
   214 lemma analz_image_freshK [rule_format]:
   215  "evs \<in> ns_shared \<Longrightarrow>
   216    \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   217              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   218              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   219 apply (erule ns_shared.induct, force)
   220 apply (drule_tac [7] Says_Server_message_form)
   221 apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   222 done
   223 
   224 
   225 lemma analz_insert_freshK:
   226      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   227        (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   228        (K = KAB \<or> Key K \<in> analz (spies evs))"
   229 by (simp only: analz_image_freshK analz_image_freshK_simps)
   230 
   231 
   232 subsubsection{*The session key K uniquely identifies the message*}
   233 
   234 text{*In messages of this form, the session key uniquely identifies the rest*}
   235 lemma unique_session_keys:
   236      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   237        Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   238        evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   239 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   240 done
   241 
   242 
   243 subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
   244 
   245 text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
   246 lemma secrecy_lemma:
   247      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   248                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   249               \<in> set evs;
   250          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   251       \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   252          Key K \<notin> analz (spies evs)"
   253 apply (erule rev_mp)
   254 apply (erule ns_shared.induct, force)
   255 apply (frule_tac [7] Says_Server_message_form)
   256 apply (frule_tac [4] Says_S_message_form)
   257 apply (erule_tac [5] disjE)
   258 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  
   259 txt{*NS2*}
   260 apply blast
   261 txt{*NS3, Server sub-case*} 
   262 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   263 	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   264 txt{*NS3, Spy sub-case; also Oops*}
   265 apply (blast dest: unique_session_keys)+
   266 done
   267 
   268 
   269 
   270 text{*Final version: Server's message in the most abstract form*}
   271 lemma Spy_not_see_encrypted_key:
   272      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   273        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   274        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   275       \<Longrightarrow> Key K \<notin> analz (spies evs)"
   276 by (blast dest: Says_Server_message_form secrecy_lemma)
   277 
   278 
   279 subsection{*Guarantees available at various stages of protocol*}
   280 
   281 text{*If the encrypted message appears then it originated with the Server*}
   282 lemma B_trusts_NS3:
   283      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   284        B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   285       \<Longrightarrow> \<exists>NA. Says Server A
   286                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   287                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   288               \<in> set evs"
   289 apply (erule rev_mp)
   290 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   291 done
   292 
   293 
   294 lemma A_trusts_NS4_lemma [rule_format]:
   295    "evs \<in> ns_shared \<Longrightarrow>
   296       Key K \<notin> analz (spies evs) \<longrightarrow>
   297       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   298       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   299       Says B A (Crypt K (Nonce NB)) \<in> set evs"
   300 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   301 apply (analz_mono_contra, simp_all, blast) 
   302 (*NS2: contradiction from the assumptions
   303   Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   304 apply (force dest!: Crypt_imp_keysFor)     
   305 txt{*NS3*}
   306 apply blast 
   307 txt{*NS4*} 
   308 apply (blast dest: B_trusts_NS3
   309 	           Says_imp_knows_Spy [THEN analz.Inj]
   310                    Crypt_Spy_analz_bad unique_session_keys)
   311 done
   312 
   313 text{*This version no longer assumes that K is secure*}
   314 lemma A_trusts_NS4:
   315      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   316        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   317        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   318        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   319       \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   320 by (blast intro: A_trusts_NS4_lemma
   321           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   322 
   323 (*If the session key has been used in NS4 then somebody has forwarded
   324   component X in some instance of NS4.  Perhaps an interesting property,
   325   but not needed (after all) for the proofs below.*)
   326 theorem NS4_implies_NS3 [rule_format]:
   327   "evs \<in> ns_shared \<Longrightarrow>
   328      Key K \<notin> analz (spies evs) \<longrightarrow>
   329      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   330      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   331      (\<exists>A'. Says A' B X \<in> set evs)"
   332 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   333 apply (simp_all add: ex_disj_distrib, blast)
   334 txt{*NS2*}
   335 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   336 txt{*NS3*}
   337 apply blast
   338 txt{*NS4*}
   339 apply (blast dest: B_trusts_NS3
   340 	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   341                    unique_session_keys Crypt_Spy_analz_bad)
   342 done
   343 
   344 
   345 lemma B_trusts_NS5_lemma [rule_format]:
   346   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   347      Key K \<notin> analz (spies evs) \<longrightarrow>
   348      Says Server A
   349 	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   350 			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   351      Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   352      Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   353 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
   354 txt{*NS2*}
   355 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   356 txt{*NS3*}
   357 apply (blast dest!: cert_A_form) 
   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