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