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