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