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