src/HOL/Auth/NS_Shared.thy
author blanchet
Fri Aug 20 16:44:48 2010 +0200 (2010-08-20)
changeset 38617 f7b32911340b
parent 37936 1e4c5015a72e
child 38628 baf9f06601e4
permissions -rw-r--r--
unbreak "only" option of Sledgehammer
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@38617
     8
theory NS_Shared imports Sledgehammer2d(*###*) 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
declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
paulson@11104
    90
paulson@11104
    91
paulson@13926
    92
text{*A "possibility property": there are traces that reach the end*}
paulson@14207
    93
lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
paulson@14200
    94
       ==> \<exists>N. \<exists>evs \<in> ns_shared.
paulson@14200
    95
                    Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
paulson@11104
    96
apply (intro exI bexI)
paulson@11104
    97
apply (rule_tac [2] ns_shared.Nil
paulson@11104
    98
       [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
wenzelm@32960
    99
        THEN ns_shared.NS4, THEN ns_shared.NS5])
paulson@14207
   100
apply (possibility, simp add: used_Cons)
paulson@11104
   101
done
paulson@11104
   102
paulson@11104
   103
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
paulson@13926
   104
lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
paulson@13926
   105
                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
paulson@11104
   106
*)
paulson@11104
   107
paulson@11104
   108
paulson@13926
   109
subsection{*Inductive proofs about @{term ns_shared}*}
paulson@11104
   110
paulson@13926
   111
subsubsection{*Forwarding lemmas, to aid simplification*}
paulson@1934
   112
paulson@13926
   113
text{*For reasoning about the encrypted portion of message NS3*}
paulson@11104
   114
lemma NS3_msg_in_parts_spies:
paulson@13926
   115
     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
paulson@11104
   116
by blast
paulson@11280
   117
paulson@13926
   118
text{*For reasoning about the Oops message*}
paulson@11104
   119
lemma Oops_parts_spies:
paulson@13926
   120
     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
paulson@13926
   121
            \<Longrightarrow> K \<in> parts (spies evs)"
paulson@11104
   122
by blast
paulson@11104
   123
paulson@13926
   124
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
paulson@13926
   125
    sends messages containing @{term X}*}
paulson@11104
   126
paulson@13926
   127
text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
paulson@11104
   128
lemma Spy_see_shrK [simp]:
paulson@13926
   129
     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@13507
   130
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
paulson@11104
   131
done
paulson@11104
   132
paulson@11104
   133
lemma Spy_analz_shrK [simp]:
paulson@13926
   134
     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@11104
   135
by auto
paulson@11104
   136
paulson@11104
   137
paulson@13926
   138
text{*Nobody can have used non-existent keys!*}
paulson@14207
   139
lemma new_keys_not_used [simp]:
paulson@14207
   140
    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
paulson@14207
   141
     ==> K \<notin> keysFor (parts (spies evs))"
paulson@14207
   142
apply (erule rev_mp)
paulson@13507
   143
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
paulson@13926
   144
txt{*Fake, NS2, NS4, NS5*}
paulson@13926
   145
apply (force dest!: keysFor_parts_insert, blast+)
paulson@11104
   146
done
paulson@11104
   147
paulson@11104
   148
paulson@13926
   149
subsubsection{*Lemmas concerning the form of items passed in messages*}
paulson@11104
   150
paulson@13926
   151
text{*Describes the form of K, X and K' when the Server sends this message.*}
paulson@11104
   152
lemma Says_Server_message_form:
paulson@13926
   153
     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   154
       evs \<in> ns_shared\<rbrakk>
paulson@13926
   155
      \<Longrightarrow> K \<notin> range shrK \<and>
paulson@13926
   156
          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
paulson@11104
   157
          K' = shrK A"
paulson@11104
   158
by (erule rev_mp, erule ns_shared.induct, auto)
paulson@11104
   159
paulson@1934
   160
paulson@13926
   161
text{*If the encrypted message appears then it originated with the Server*}
paulson@11104
   162
lemma A_trusts_NS2:
paulson@13926
   163
     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@13926
   164
       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   165
      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
paulson@11104
   166
apply (erule rev_mp)
paulson@13507
   167
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
paulson@11104
   168
done
paulson@11104
   169
paulson@11104
   170
lemma cert_A_form:
paulson@13926
   171
     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@13926
   172
       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   173
      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
paulson@11104
   174
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
paulson@11104
   175
paulson@14207
   176
text{*EITHER describes the form of X when the following message is sent,
paulson@11104
   177
  OR     reduces it to the Fake case.
paulson@14207
   178
  Use @{text Says_Server_message_form} if applicable.*}
paulson@11104
   179
lemma Says_S_message_form:
paulson@13926
   180
     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   181
       evs \<in> ns_shared\<rbrakk>
paulson@13926
   182
      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
paulson@13926
   183
          \<or> X \<in> analz (spies evs)"
paulson@14207
   184
by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
paulson@11150
   185
paulson@11104
   186
paulson@11104
   187
(*Alternative version also provable
paulson@11104
   188
lemma Says_S_message_form2:
paulson@13926
   189
  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   190
    evs \<in> ns_shared\<rbrakk>
paulson@13926
   191
   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
paulson@13926
   192
       \<or> X \<in> analz (spies evs)"
paulson@13926
   193
apply (case_tac "A \<in> bad")
paulson@13507
   194
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
paulson@11104
   195
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
paulson@11104
   196
*)
paulson@11104
   197
paulson@11104
   198
paulson@11104
   199
(****
paulson@11104
   200
 SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
paulson@11104
   201
paulson@13926
   202
  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
paulson@13926
   203
  Key K \<in> analz (spies evs)
paulson@11104
   204
paulson@11104
   205
 A more general formula must be proved inductively.
paulson@11104
   206
****)
paulson@1934
   207
paulson@13926
   208
text{*NOT useful in this form, but it says that session keys are not used
paulson@11104
   209
  to encrypt messages containing other keys, in the actual protocol.
paulson@13926
   210
  We require that agents should behave like this subsequently also.*}
paulson@13926
   211
lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
paulson@13926
   212
         (Crypt KAB X) \<in> parts (spies evs) \<and>
paulson@13926
   213
         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
paulson@13507
   214
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
paulson@13926
   215
txt{*Fake*}
paulson@11104
   216
apply (blast dest: parts_insert_subset_Un)
paulson@13926
   217
txt{*Base, NS4 and NS5*}
paulson@11104
   218
apply auto
paulson@11104
   219
done
paulson@11104
   220
paulson@11104
   221
paulson@13926
   222
subsubsection{*Session keys are not used to encrypt other session keys*}
paulson@11104
   223
paulson@13926
   224
text{*The equality makes the induction hypothesis easier to apply*}
paulson@11104
   225
paulson@11104
   226
lemma analz_image_freshK [rule_format]:
paulson@13926
   227
 "evs \<in> ns_shared \<Longrightarrow>
paulson@13926
   228
   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
paulson@13926
   229
             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
paulson@13926
   230
             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
paulson@14207
   231
apply (erule ns_shared.induct)
paulson@14207
   232
apply (drule_tac [8] Says_Server_message_form)
paulson@14207
   233
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
paulson@14207
   234
txt{*NS2, NS3*}
paulson@14207
   235
apply blast+; 
paulson@11104
   236
done
paulson@11104
   237
paulson@11104
   238
paulson@11104
   239
lemma analz_insert_freshK:
paulson@13926
   240
     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
paulson@13926
   241
       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@13926
   242
       (K = KAB \<or> Key K \<in> analz (spies evs))"
paulson@11104
   243
by (simp only: analz_image_freshK analz_image_freshK_simps)
paulson@11104
   244
paulson@11104
   245
paulson@13926
   246
subsubsection{*The session key K uniquely identifies the message*}
paulson@1934
   247
paulson@13926
   248
text{*In messages of this form, the session key uniquely identifies the rest*}
paulson@11104
   249
lemma unique_session_keys:
paulson@13926
   250
     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   251
       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
paulson@13926
   252
       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
paulson@18886
   253
by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
paulson@11104
   254
paulson@11104
   255
paulson@18886
   256
subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
paulson@11104
   257
paulson@13956
   258
text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
paulson@11150
   259
lemma secrecy_lemma:
paulson@13926
   260
     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
paulson@13926
   261
                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
paulson@13926
   262
              \<in> set evs;
paulson@13926
   263
         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   264
      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
paulson@13926
   265
         Key K \<notin> analz (spies evs)"
paulson@11104
   266
apply (erule rev_mp)
paulson@11104
   267
apply (erule ns_shared.induct, force)
paulson@11104
   268
apply (frule_tac [7] Says_Server_message_form)
paulson@11104
   269
apply (frule_tac [4] Says_S_message_form)
paulson@11104
   270
apply (erule_tac [5] disjE)
paulson@14207
   271
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
paulson@13926
   272
txt{*NS2*}
paulson@13926
   273
apply blast
paulson@32404
   274
txt{*NS3*}
paulson@11188
   275
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
wenzelm@32960
   276
             dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
paulson@32404
   277
txt{*Oops*}
paulson@32404
   278
apply (blast dest: unique_session_keys)
paulson@11104
   279
done
paulson@11104
   280
paulson@11104
   281
paulson@11188
   282
paulson@13926
   283
text{*Final version: Server's message in the most abstract form*}
paulson@11104
   284
lemma Spy_not_see_encrypted_key:
paulson@13926
   285
     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@13926
   286
       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
paulson@13926
   287
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   288
      \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@11150
   289
by (blast dest: Says_Server_message_form secrecy_lemma)
paulson@11104
   290
paulson@11104
   291
paulson@13926
   292
subsection{*Guarantees available at various stages of protocol*}
paulson@1934
   293
paulson@13926
   294
text{*If the encrypted message appears then it originated with the Server*}
paulson@11104
   295
lemma B_trusts_NS3:
paulson@13926
   296
     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
paulson@13926
   297
       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
paulson@13926
   298
      \<Longrightarrow> \<exists>NA. Says Server A
paulson@13926
   299
               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
paulson@13926
   300
                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
paulson@13926
   301
              \<in> set evs"
paulson@11104
   302
apply (erule rev_mp)
paulson@13507
   303
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
paulson@11104
   304
done
paulson@11104
   305
paulson@11104
   306
paulson@11104
   307
lemma A_trusts_NS4_lemma [rule_format]:
paulson@13926
   308
   "evs \<in> ns_shared \<Longrightarrow>
paulson@13926
   309
      Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@13926
   310
      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
paulson@13926
   311
      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
paulson@13926
   312
      Says B A (Crypt K (Nonce NB)) \<in> set evs"
paulson@11104
   313
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
blanchet@38617
   314
sledgehammer [atp = e, overlord] (Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
blanchet@38617
   315
apply (metis Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
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
wenzelm@32960
   358
          (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
wenzelm@32960
   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
wenzelm@32960
   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