src/HOL/Auth/NS_Shared.thy
author paulson
Thu Aug 27 15:49:45 2009 +0100 (2009-08-27)
changeset 32527 569e8d6729a1
parent 32404 da3ca3c6ec81
child 32960 69916a850301
permissions -rw-r--r--
More streamlining using metis.
paulson@1934
     1
(*  Title:      HOL/Auth/NS_Shared
paulson@1934
     2
    ID:         $Id$
paulson@18886
     3
    Author:     Lawrence C Paulson and Giampaolo Bella 
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
*)
paulson@1934
     6
paulson@18886
     7
header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
paulson@14207
     8
haftmann@16417
     9
theory NS_Shared imports Public begin
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@18886
    17
constdefs
paulson@18886
    18
paulson@18886
    19
 (* A is the true creator of X if she has sent X and X never appeared on
paulson@18886
    20
    the trace before this event. Recall that traces grow from head. *)
paulson@18886
    21
  Issues :: "[agent, agent, msg, event list] => bool"
paulson@18886
    22
             ("_ Issues _ with _ on _")
paulson@18886
    23
   "A Issues B with X on evs ==
paulson@18886
    24
      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
paulson@18886
    25
      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
paulson@18886
    26
paulson@18886
    27
berghofe@23746
    28
inductive_set ns_shared :: "event list set"
berghofe@23746
    29
 where
paulson@11104
    30
	(*Initial trace is empty*)
paulson@13926
    31
  Nil:  "[] \<in> ns_shared"
paulson@11104
    32
	(*The spy MAY say anything he CAN say.  We do not expect him to
paulson@11104
    33
	  invent new nonces here, but he can also use NS1.  Common to
paulson@11104
    34
	  all similar protocols.*)
berghofe@23746
    35
| Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
paulson@13926
    36
	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
paulson@11104
    37
paulson@11104
    38
	(*Alice initiates a protocol run, requesting to talk to any B*)
berghofe@23746
    39
| NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
paulson@13926
    40
	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
paulson@11104
    41
paulson@11104
    42
	(*Server's response to Alice's message.
paulson@11104
    43
	  !! It may respond more than once to A's request !!
paulson@11104
    44
	  Server doesn't know who the true sender is, hence the A' in
paulson@11104
    45
	      the sender field.*)
berghofe@23746
    46
| NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
paulson@13926
    47
	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
paulson@13926
    48
	 \<Longrightarrow> Says Server A
paulson@11104
    49
	       (Crypt (shrK A)
paulson@13926
    50
		  \<lbrace>Nonce NA, Agent B, Key KAB,
paulson@13926
    51
		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
paulson@13926
    52
	       # evs2 \<in> ns_shared"
paulson@11104
    53
paulson@11104
    54
	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
paulson@13926
    55
	   Need A \<noteq> Server because we allow messages to self.*)
berghofe@23746
    56
| NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
paulson@13926
    57
	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
paulson@13926
    58
	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
paulson@13926
    59
	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
paulson@11104
    60
paulson@11104
    61
	(*Bob's nonce exchange.  He does not know who the message came
paulson@11104
    62
	  from, but responds to A because she is mentioned inside.*)
berghofe@23746
    63
| NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
paulson@13926
    64
	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
paulson@13926
    65
	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
paulson@1934
    66
paulson@11104
    67
	(*Alice responds with Nonce NB if she has seen the key before.
paulson@11104
    68
	  Maybe should somehow check Nonce NA again.
paulson@11104
    69
	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
paulson@11465
    70
	  Letting the Spy add or subtract 1 lets him send all nonces.
paulson@11104
    71
	  Instead we distinguish the messages by sending the nonce twice.*)
berghofe@23746
    72
| NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
paulson@13926
    73
	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
paulson@13926
    74
	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
paulson@13926
    75
	    \<in> set evs5\<rbrakk>
paulson@13926
    76
	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
paulson@11104
    77
paulson@11104
    78
	(*This message models possible leaks of session keys.
paulson@11104
    79
	  The two Nonces identify the protocol run: the rule insists upon
paulson@11104
    80
	  the true senders in order to make them accurate.*)
berghofe@23746
    81
| Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
paulson@13926
    82
	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
paulson@13926
    83
	      \<in> set evso\<rbrakk>
paulson@13926
    84
	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
paulson@11104
    85
paulson@11150
    86
paulson@11150
    87
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@11150
    88
declare parts.Body  [dest]
paulson@11251
    89
declare Fake_parts_insert_in_Un  [dest]
paulson@11251
    90
declare analz_into_parts [dest]
paulson@11104
    91
declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
paulson@11104
    92
paulson@11104
    93
paulson@13926
    94
text{*A "possibility property": there are traces that reach the end*}
paulson@14207
    95
lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
paulson@14200
    96
       ==> \<exists>N. \<exists>evs \<in> ns_shared.
paulson@14200
    97
                    Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
paulson@11104
    98
apply (intro exI bexI)
paulson@11104
    99
apply (rule_tac [2] ns_shared.Nil
paulson@11104
   100
       [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
paulson@14200
   101
	THEN ns_shared.NS4, THEN ns_shared.NS5])
paulson@14207
   102
apply (possibility, simp add: used_Cons)
paulson@11104
   103
done
paulson@11104
   104
paulson@11104
   105
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
paulson@13926
   106
lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
paulson@13926
   107
                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
paulson@11104
   108
*)
paulson@11104
   109
paulson@11104
   110
paulson@13926
   111
subsection{*Inductive proofs about @{term ns_shared}*}
paulson@11104
   112
paulson@13926
   113
subsubsection{*Forwarding lemmas, to aid simplification*}
paulson@1934
   114
paulson@13926
   115
text{*For reasoning about the encrypted portion of message NS3*}
paulson@11104
   116
lemma NS3_msg_in_parts_spies:
paulson@13926
   117
     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
paulson@11104
   118
by blast
paulson@11280
   119
paulson@13926
   120
text{*For reasoning about the Oops message*}
paulson@11104
   121
lemma Oops_parts_spies:
paulson@13926
   122
     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
paulson@13926
   123
            \<Longrightarrow> K \<in> parts (spies evs)"
paulson@11104
   124
by blast
paulson@11104
   125
paulson@13926
   126
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
paulson@13926
   127
    sends messages containing @{term X}*}
paulson@11104
   128
paulson@13926
   129
text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
paulson@11104
   130
lemma Spy_see_shrK [simp]:
paulson@13926
   131
     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@13507
   132
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
paulson@11104
   133
done
paulson@11104
   134
paulson@11104
   135
lemma Spy_analz_shrK [simp]:
paulson@13926
   136
     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@11104
   137
by auto
paulson@11104
   138
paulson@11104
   139
paulson@13926
   140
text{*Nobody can have used non-existent keys!*}
paulson@14207
   141
lemma new_keys_not_used [simp]:
paulson@14207
   142
    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
paulson@14207
   143
     ==> K \<notin> keysFor (parts (spies evs))"
paulson@14207
   144
apply (erule rev_mp)
paulson@13507
   145
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
paulson@13926
   146
txt{*Fake, NS2, NS4, NS5*}
paulson@13926
   147
apply (force dest!: keysFor_parts_insert, blast+)
paulson@11104
   148
done
paulson@11104
   149
paulson@11104
   150
paulson@13926
   151
subsubsection{*Lemmas concerning the form of items passed in messages*}
paulson@11104
   152
paulson@13926
   153
text{*Describes the form of K, X and K' when the Server sends this message.*}
paulson@11104
   154
lemma Says_Server_message_form:
paulson@13926
   155
     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   156
       evs \<in> ns_shared\<rbrakk>
paulson@13926
   157
      \<Longrightarrow> K \<notin> range shrK \<and>
paulson@13926
   158
          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
paulson@11104
   159
          K' = shrK A"
paulson@11104
   160
by (erule rev_mp, erule ns_shared.induct, auto)
paulson@11104
   161
paulson@1934
   162
paulson@13926
   163
text{*If the encrypted message appears then it originated with the Server*}
paulson@11104
   164
lemma A_trusts_NS2:
paulson@13926
   165
     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@13926
   166
       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   167
      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
paulson@11104
   168
apply (erule rev_mp)
paulson@13507
   169
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
paulson@11104
   170
done
paulson@11104
   171
paulson@11104
   172
lemma cert_A_form:
paulson@13926
   173
     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@13926
   174
       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   175
      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
paulson@11104
   176
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
paulson@11104
   177
paulson@14207
   178
text{*EITHER describes the form of X when the following message is sent,
paulson@11104
   179
  OR     reduces it to the Fake case.
paulson@14207
   180
  Use @{text Says_Server_message_form} if applicable.*}
paulson@11104
   181
lemma Says_S_message_form:
paulson@13926
   182
     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   183
       evs \<in> ns_shared\<rbrakk>
paulson@13926
   184
      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
paulson@13926
   185
          \<or> X \<in> analz (spies evs)"
paulson@14207
   186
by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
paulson@11150
   187
paulson@11104
   188
paulson@11104
   189
(*Alternative version also provable
paulson@11104
   190
lemma Says_S_message_form2:
paulson@13926
   191
  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   192
    evs \<in> ns_shared\<rbrakk>
paulson@13926
   193
   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
paulson@13926
   194
       \<or> X \<in> analz (spies evs)"
paulson@13926
   195
apply (case_tac "A \<in> bad")
paulson@13507
   196
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
paulson@11104
   197
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
paulson@11104
   198
*)
paulson@11104
   199
paulson@11104
   200
paulson@11104
   201
(****
paulson@11104
   202
 SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
paulson@11104
   203
paulson@13926
   204
  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
paulson@13926
   205
  Key K \<in> analz (spies evs)
paulson@11104
   206
paulson@11104
   207
 A more general formula must be proved inductively.
paulson@11104
   208
****)
paulson@1934
   209
paulson@13926
   210
text{*NOT useful in this form, but it says that session keys are not used
paulson@11104
   211
  to encrypt messages containing other keys, in the actual protocol.
paulson@13926
   212
  We require that agents should behave like this subsequently also.*}
paulson@13926
   213
lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
paulson@13926
   214
         (Crypt KAB X) \<in> parts (spies evs) \<and>
paulson@13926
   215
         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
paulson@13507
   216
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
paulson@13926
   217
txt{*Fake*}
paulson@11104
   218
apply (blast dest: parts_insert_subset_Un)
paulson@13926
   219
txt{*Base, NS4 and NS5*}
paulson@11104
   220
apply auto
paulson@11104
   221
done
paulson@11104
   222
paulson@11104
   223
paulson@13926
   224
subsubsection{*Session keys are not used to encrypt other session keys*}
paulson@11104
   225
paulson@13926
   226
text{*The equality makes the induction hypothesis easier to apply*}
paulson@11104
   227
paulson@11104
   228
lemma analz_image_freshK [rule_format]:
paulson@13926
   229
 "evs \<in> ns_shared \<Longrightarrow>
paulson@13926
   230
   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
paulson@13926
   231
             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
paulson@13926
   232
             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
paulson@14207
   233
apply (erule ns_shared.induct)
paulson@14207
   234
apply (drule_tac [8] Says_Server_message_form)
paulson@14207
   235
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
paulson@14207
   236
txt{*NS2, NS3*}
paulson@14207
   237
apply blast+; 
paulson@11104
   238
done
paulson@11104
   239
paulson@11104
   240
paulson@11104
   241
lemma analz_insert_freshK:
paulson@13926
   242
     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
paulson@13926
   243
       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@13926
   244
       (K = KAB \<or> Key K \<in> analz (spies evs))"
paulson@11104
   245
by (simp only: analz_image_freshK analz_image_freshK_simps)
paulson@11104
   246
paulson@11104
   247
paulson@13926
   248
subsubsection{*The session key K uniquely identifies the message*}
paulson@1934
   249
paulson@13926
   250
text{*In messages of this form, the session key uniquely identifies the rest*}
paulson@11104
   251
lemma unique_session_keys:
paulson@13926
   252
     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   253
       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
paulson@13926
   254
       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
paulson@18886
   255
by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
paulson@11104
   256
paulson@11104
   257
paulson@18886
   258
subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
paulson@11104
   259
paulson@13956
   260
text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
paulson@11150
   261
lemma secrecy_lemma:
paulson@13926
   262
     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
paulson@13926
   263
                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
paulson@13926
   264
              \<in> set evs;
paulson@13926
   265
         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   266
      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
paulson@13926
   267
         Key K \<notin> analz (spies evs)"
paulson@11104
   268
apply (erule rev_mp)
paulson@11104
   269
apply (erule ns_shared.induct, force)
paulson@11104
   270
apply (frule_tac [7] Says_Server_message_form)
paulson@11104
   271
apply (frule_tac [4] Says_S_message_form)
paulson@11104
   272
apply (erule_tac [5] disjE)
paulson@14207
   273
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
paulson@13926
   274
txt{*NS2*}
paulson@13926
   275
apply blast
paulson@32404
   276
txt{*NS3*}
paulson@11188
   277
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
paulson@11188
   278
	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
paulson@32404
   279
txt{*Oops*}
paulson@32404
   280
apply (blast dest: unique_session_keys)
paulson@11104
   281
done
paulson@11104
   282
paulson@11104
   283
paulson@11188
   284
paulson@13926
   285
text{*Final version: Server's message in the most abstract form*}
paulson@11104
   286
lemma Spy_not_see_encrypted_key:
paulson@13926
   287
     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   288
       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
paulson@13926
   289
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   290
      \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@11150
   291
by (blast dest: Says_Server_message_form secrecy_lemma)
paulson@11104
   292
paulson@11104
   293
paulson@13926
   294
subsection{*Guarantees available at various stages of protocol*}
paulson@1934
   295
paulson@13926
   296
text{*If the encrypted message appears then it originated with the Server*}
paulson@11104
   297
lemma B_trusts_NS3:
paulson@13926
   298
     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
paulson@13926
   299
       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   300
      \<Longrightarrow> \<exists>NA. Says Server A
paulson@13926
   301
               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
paulson@13926
   302
                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
paulson@13926
   303
              \<in> set evs"
paulson@11104
   304
apply (erule rev_mp)
paulson@13507
   305
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
paulson@11104
   306
done
paulson@11104
   307
paulson@11104
   308
paulson@11104
   309
lemma A_trusts_NS4_lemma [rule_format]:
paulson@13926
   310
   "evs \<in> ns_shared \<Longrightarrow>
paulson@13926
   311
      Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@13926
   312
      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
paulson@13926
   313
      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
paulson@13926
   314
      Says B A (Crypt K (Nonce NB)) \<in> set evs"
paulson@11104
   315
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
paulson@14207
   316
apply (analz_mono_contra, simp_all, blast)
paulson@14207
   317
txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
paulson@14207
   318
    @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
paulson@14207
   319
apply (force dest!: Crypt_imp_keysFor)
paulson@14207
   320
txt{*NS4*}
paulson@32527
   321
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
paulson@11104
   322
done
paulson@11104
   323
paulson@13926
   324
text{*This version no longer assumes that K is secure*}
paulson@11104
   325
lemma A_trusts_NS4:
paulson@13926
   326
     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
paulson@13926
   327
       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@13926
   328
       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
paulson@13926
   329
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   330
      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
paulson@11280
   331
by (blast intro: A_trusts_NS4_lemma
paulson@11104
   332
          dest: A_trusts_NS2 Spy_not_see_encrypted_key)
paulson@11104
   333
paulson@14207
   334
text{*If the session key has been used in NS4 then somebody has forwarded
paulson@11280
   335
  component X in some instance of NS4.  Perhaps an interesting property,
paulson@14207
   336
  but not needed (after all) for the proofs below.*}
paulson@11104
   337
theorem NS4_implies_NS3 [rule_format]:
paulson@13926
   338
  "evs \<in> ns_shared \<Longrightarrow>
paulson@13926
   339
     Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@13926
   340
     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
paulson@13926
   341
     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
paulson@13926
   342
     (\<exists>A'. Says A' B X \<in> set evs)"
paulson@18886
   343
apply (erule ns_shared.induct, force)
paulson@18886
   344
apply (drule_tac [4] NS3_msg_in_parts_spies)
paulson@18886
   345
apply analz_mono_contra
paulson@13926
   346
apply (simp_all add: ex_disj_distrib, blast)
paulson@13926
   347
txt{*NS2*}
paulson@14207
   348
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
paulson@13926
   349
txt{*NS4*}
paulson@32527
   350
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
paulson@11104
   351
done
paulson@11104
   352
paulson@11104
   353
paulson@11104
   354
lemma B_trusts_NS5_lemma [rule_format]:
paulson@13926
   355
  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
paulson@13926
   356
     Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@11104
   357
     Says Server A
paulson@13926
   358
	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
paulson@13926
   359
			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
paulson@13926
   360
     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
paulson@13926
   361
     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
paulson@18886
   362
apply (erule ns_shared.induct, force)
paulson@18886
   363
apply (drule_tac [4] NS3_msg_in_parts_spies)
paulson@18886
   364
apply (analz_mono_contra, simp_all, blast)
paulson@13926
   365
txt{*NS2*}
paulson@14207
   366
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
paulson@13926
   367
txt{*NS5*}
paulson@11150
   368
apply (blast dest!: A_trusts_NS2
paulson@11280
   369
	     dest: Says_imp_knows_Spy [THEN analz.Inj]
paulson@11150
   370
                   unique_session_keys Crypt_Spy_analz_bad)
paulson@11104
   371
done
paulson@11104
   372
paulson@11104
   373
paulson@13926
   374
text{*Very strong Oops condition reveals protocol's weakness*}
paulson@11104
   375
lemma B_trusts_NS5:
paulson@13926
   376
     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
paulson@13926
   377
       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
paulson@13926
   378
       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
paulson@13926
   379
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   380
      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
paulson@11280
   381
by (blast intro: B_trusts_NS5_lemma
paulson@11150
   382
          dest: B_trusts_NS3 Spy_not_see_encrypted_key)
paulson@1934
   383
paulson@18886
   384
text{*Unaltered so far wrt original version*}
paulson@18886
   385
paulson@18886
   386
subsection{*Lemmas for reasoning about predicate "Issues"*}
paulson@18886
   387
paulson@18886
   388
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
paulson@18886
   389
apply (induct_tac "evs")
paulson@18886
   390
apply (induct_tac [2] "a", auto)
paulson@18886
   391
done
paulson@18886
   392
paulson@18886
   393
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
paulson@18886
   394
apply (induct_tac "evs")
paulson@18886
   395
apply (induct_tac [2] "a", auto)
paulson@18886
   396
done
paulson@18886
   397
paulson@18886
   398
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
paulson@18886
   399
          (if A:bad then insert X (spies evs) else spies evs)"
paulson@18886
   400
apply (induct_tac "evs")
paulson@18886
   401
apply (induct_tac [2] "a", auto)
paulson@18886
   402
done
paulson@18886
   403
paulson@18886
   404
lemma spies_evs_rev: "spies evs = spies (rev evs)"
paulson@18886
   405
apply (induct_tac "evs")
paulson@18886
   406
apply (induct_tac [2] "a")
paulson@18886
   407
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
paulson@18886
   408
done
paulson@18886
   409
paulson@18886
   410
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
paulson@18886
   411
paulson@18886
   412
lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
paulson@18886
   413
apply (induct_tac "evs")
paulson@18886
   414
apply (induct_tac [2] "a", auto)
paulson@18886
   415
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
paulson@18886
   416
done
paulson@18886
   417
paulson@18886
   418
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
paulson@18886
   419
paulson@18886
   420
paulson@18886
   421
subsection{*Guarantees of non-injective agreement on the session key, and
paulson@18886
   422
of key distribution. They also express forms of freshness of certain messages,
paulson@18886
   423
namely that agents were alive after something happened.*}
paulson@18886
   424
paulson@18886
   425
lemma B_Issues_A:
paulson@18886
   426
     "\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs;
paulson@18886
   427
         Key K \<notin> analz (spies evs);
paulson@18886
   428
         A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
paulson@18886
   429
      \<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs"
paulson@18886
   430
apply (simp (no_asm) add: Issues_def)
paulson@18886
   431
apply (rule exI)
paulson@18886
   432
apply (rule conjI, assumption)
paulson@18886
   433
apply (simp (no_asm))
paulson@18886
   434
apply (erule rev_mp)
paulson@18886
   435
apply (erule rev_mp)
paulson@18886
   436
apply (erule ns_shared.induct, analz_mono_contra)
paulson@18886
   437
apply (simp_all)
paulson@18886
   438
txt{*fake*}
paulson@18886
   439
apply blast
paulson@18886
   440
apply (simp_all add: takeWhile_tail)
paulson@18886
   441
txt{*NS3 remains by pure coincidence!*}
paulson@18886
   442
apply (force dest!: A_trusts_NS2 Says_Server_message_form)
paulson@18886
   443
txt{*NS4 would be the non-trivial case can be solved by Nb being used*}
paulson@18886
   444
apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
paulson@18886
   445
                   parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
   446
done
paulson@18886
   447
paulson@18886
   448
text{*Tells A that B was alive after she sent him the session key.  The
paulson@18886
   449
session key must be assumed confidential for this deduction to be meaningful,
paulson@18886
   450
but that assumption can be relaxed by the appropriate argument.
paulson@18886
   451
paulson@18886
   452
Precisely, the theorem guarantees (to A) key distribution of the session key
paulson@18886
   453
to B. It also guarantees (to A) non-injective agreement of B with A on the
paulson@18886
   454
session key. Both goals are available to A in the sense of Goal Availability.
paulson@18886
   455
*}
paulson@18886
   456
lemma A_authenticates_and_keydist_to_B:
paulson@18886
   457
     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
paulson@18886
   458
       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   459
       Key K \<notin> analz(knows Spy evs);
paulson@18886
   460
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@18886
   461
      \<Longrightarrow> B Issues A with (Crypt K (Nonce NB)) on evs"
paulson@18886
   462
by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)
paulson@18886
   463
paulson@18886
   464
lemma A_trusts_NS5:
paulson@18886
   465
  "\<lbrakk> Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts(spies evs);
paulson@18886
   466
     Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
paulson@18886
   467
     Key K \<notin> analz (spies evs);
paulson@18886
   468
     A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
paulson@18886
   469
 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
paulson@18886
   470
apply (erule rev_mp)
paulson@18886
   471
apply (erule rev_mp)
paulson@18886
   472
apply (erule rev_mp)
paulson@18886
   473
apply (erule ns_shared.induct, analz_mono_contra)
paulson@18886
   474
apply (simp_all)
paulson@18886
   475
txt{*Fake*}
paulson@18886
   476
apply blast
paulson@18886
   477
txt{*NS2*}
paulson@18886
   478
apply (force dest!: Crypt_imp_keysFor)
paulson@32527
   479
txt{*NS3*}
paulson@32527
   480
apply (metis NS3_msg_in_parts_spies parts_cut_eq)
paulson@18886
   481
txt{*NS5, the most important case, can be solved by unicity*}
paulson@32527
   482
apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
paulson@18886
   483
done
paulson@18886
   484
paulson@18886
   485
lemma A_Issues_B:
paulson@18886
   486
     "\<lbrakk> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs;
paulson@18886
   487
        Key K \<notin> analz (spies evs);
paulson@18886
   488
        A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
paulson@18886
   489
    \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
paulson@18886
   490
apply (simp (no_asm) add: Issues_def)
paulson@18886
   491
apply (rule exI)
paulson@18886
   492
apply (rule conjI, assumption)
paulson@18886
   493
apply (simp (no_asm))
paulson@18886
   494
apply (erule rev_mp)
paulson@18886
   495
apply (erule rev_mp)
paulson@18886
   496
apply (erule ns_shared.induct, analz_mono_contra)
paulson@18886
   497
apply (simp_all)
paulson@18886
   498
txt{*fake*}
paulson@18886
   499
apply blast
paulson@18886
   500
apply (simp_all add: takeWhile_tail)
paulson@18886
   501
txt{*NS3 remains by pure coincidence!*}
paulson@18886
   502
apply (force dest!: A_trusts_NS2 Says_Server_message_form)
paulson@18886
   503
txt{*NS5 is the non-trivial case and cannot be solved as in @{term B_Issues_A}! because NB is not fresh. We need @{term A_trusts_NS5}, proved for this very purpose*}
paulson@18886
   504
apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
paulson@18886
   505
        parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
   506
done
paulson@18886
   507
paulson@18886
   508
text{*Tells B that A was alive after B issued NB.
paulson@18886
   509
paulson@18886
   510
Precisely, the theorem guarantees (to B) key distribution of the session key to A. It also guarantees (to B) non-injective agreement of A with B on the session key. Both goals are available to B in the sense of Goal Availability.
paulson@18886
   511
*}
paulson@18886
   512
lemma B_authenticates_and_keydist_to_A:
paulson@18886
   513
     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
paulson@18886
   514
       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
paulson@18886
   515
       Key K \<notin> analz (spies evs);
paulson@18886
   516
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@18886
   517
   \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
paulson@18886
   518
by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)
paulson@18886
   519
paulson@1934
   520
end