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