src/HOL/Auth/Kerberos_BAN.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
wenzelm@37936
     1
(*  Title:      HOL/Auth/Kerberos_BAN.thy
paulson@5053
     2
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
paulson@5053
     3
    Copyright   1998  University of Cambridge
paulson@5053
     4
*)
paulson@5053
     5
wenzelm@58889
     6
section{*The Kerberos Protocol, BAN Version*}
paulson@14207
     7
haftmann@16417
     8
theory Kerberos_BAN imports Public begin
paulson@5053
     9
paulson@14207
    10
text{*From page 251 of
paulson@14207
    11
  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
paulson@14207
    12
  Proc. Royal Soc. 426
paulson@14207
    13
paulson@18886
    14
  Confidentiality (secrecy) and authentication properties are also
paulson@18886
    15
  given in a termporal version: strong guarantees in a little abstracted 
paulson@18886
    16
  - but very realistic - model.
paulson@14207
    17
*}
paulson@14207
    18
paulson@18886
    19
(* Temporal model of accidents: session keys can be leaked
paulson@18886
    20
                                ONLY when they have expired *)
paulson@5053
    21
paulson@5053
    22
consts
paulson@5053
    23
paulson@5053
    24
    (*Duration of the session key*)
paulson@18886
    25
    sesKlife   :: nat
paulson@5053
    26
paulson@5053
    27
    (*Duration of the authenticator*)
paulson@18886
    28
    authlife :: nat
paulson@5053
    29
paulson@14126
    30
text{*The ticket should remain fresh for two journeys on the network at least*}
paulson@18886
    31
specification (sesKlife)
paulson@18886
    32
  sesKlife_LB [iff]: "2 \<le> sesKlife"
paulson@14126
    33
    by blast
paulson@5053
    34
paulson@14126
    35
text{*The authenticator only for one journey*}
paulson@18886
    36
specification (authlife)
nipkow@25134
    37
  authlife_LB [iff]:    "authlife \<noteq> 0"
paulson@14126
    38
    by blast
paulson@14126
    39
wenzelm@20768
    40
abbreviation
wenzelm@21404
    41
  CT :: "event list=>nat" where
wenzelm@20768
    42
  "CT == length "
paulson@14207
    43
wenzelm@21404
    44
abbreviation
wenzelm@21404
    45
  expiredK :: "[nat, event list] => bool" where
wenzelm@20768
    46
  "expiredK T evs == sesKlife + T < CT evs"
paulson@18886
    47
wenzelm@21404
    48
abbreviation
wenzelm@21404
    49
  expiredA :: "[nat, event list] => bool" where
wenzelm@20768
    50
  "expiredA T evs == authlife + T < CT evs"
paulson@18886
    51
paulson@18886
    52
wenzelm@36866
    53
definition
paulson@18886
    54
 (* A is the true creator of X if she has sent X and X never appeared on
paulson@18886
    55
    the trace before this event. Recall that traces grow from head. *)
paulson@18886
    56
  Issues :: "[agent, agent, msg, event list] => bool"
wenzelm@36866
    57
             ("_ Issues _ with _ on _") where
wenzelm@36866
    58
   "A Issues B with X on evs =
wenzelm@36866
    59
      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
wenzelm@36866
    60
        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
paulson@5053
    61
wenzelm@36866
    62
definition
paulson@18886
    63
 (* Yields the subtrace of a given trace from its beginning to a given event *)
paulson@18886
    64
  before :: "[event, event list] => event list" ("before _ on _")
wenzelm@36866
    65
  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
paulson@18886
    66
wenzelm@36866
    67
definition
paulson@18886
    68
 (* States than an event really appears only once on a trace *)
paulson@18886
    69
  Unique :: "[event, event list] => bool" ("Unique _ on _")
wenzelm@36866
    70
  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
paulson@18886
    71
paulson@18886
    72
berghofe@23746
    73
inductive_set bankerberos :: "event list set"
berghofe@23746
    74
 where
paulson@13926
    75
paulson@18886
    76
   Nil:  "[] \<in> bankerberos"
paulson@13926
    77
berghofe@23746
    78
 | Fake: "\<lbrakk> evsf \<in> bankerberos;  X \<in> synth (analz (spies evsf)) \<rbrakk>
wenzelm@32960
    79
          \<Longrightarrow> Says Spy B X # evsf \<in> bankerberos"
paulson@13926
    80
paulson@13926
    81
berghofe@23746
    82
 | BK1:  "\<lbrakk> evs1 \<in> bankerberos \<rbrakk>
wenzelm@32960
    83
          \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1
wenzelm@32960
    84
                \<in>  bankerberos"
paulson@18886
    85
paulson@18886
    86
berghofe@23746
    87
 | BK2:  "\<lbrakk> evs2 \<in> bankerberos;  Key K \<notin> used evs2; K \<in> symKeys;
wenzelm@32960
    88
             Says A' Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
wenzelm@32960
    89
          \<Longrightarrow> Says Server A
wenzelm@32960
    90
                (Crypt (shrK A)
wenzelm@32960
    91
                   \<lbrace>Number (CT evs2), Agent B, Key K,
wenzelm@32960
    92
                    (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>)
wenzelm@32960
    93
                # evs2 \<in> bankerberos"
paulson@13926
    94
paulson@13926
    95
berghofe@23746
    96
 | BK3:  "\<lbrakk> evs3 \<in> bankerberos;
wenzelm@32960
    97
             Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
wenzelm@32960
    98
               \<in> set evs3;
wenzelm@32960
    99
             Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
wenzelm@32960
   100
             \<not> expiredK Tk evs3 \<rbrakk>
wenzelm@32960
   101
          \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace>
wenzelm@32960
   102
               # evs3 \<in> bankerberos"
paulson@13926
   103
paulson@13926
   104
berghofe@23746
   105
 | BK4:  "\<lbrakk> evs4 \<in> bankerberos;
wenzelm@32960
   106
             Says A' B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>),
wenzelm@32960
   107
                         (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4;
wenzelm@32960
   108
             \<not> expiredK Tk evs4;  \<not> expiredA Ta evs4 \<rbrakk>
wenzelm@32960
   109
          \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4
wenzelm@32960
   110
                \<in> bankerberos"
paulson@5053
   111
wenzelm@32960
   112
        (*Old session keys may become compromised*)
berghofe@23746
   113
 | Oops: "\<lbrakk> evso \<in> bankerberos;
paulson@18886
   114
         Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
wenzelm@32960
   115
               \<in> set evso;
wenzelm@32960
   116
             expiredK Tk evso \<rbrakk>
wenzelm@32960
   117
          \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerberos"
paulson@13926
   118
paulson@13926
   119
paulson@14207
   120
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14200
   121
declare parts.Body [dest]
paulson@14200
   122
declare analz_into_parts [dest]
paulson@14200
   123
declare Fake_parts_insert_in_Un [dest]
paulson@13926
   124
paulson@14207
   125
text{*A "possibility property": there are traces that reach the end.*}
paulson@18886
   126
lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk>
paulson@18886
   127
       \<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerberos.
paulson@14207
   128
             Says B A (Crypt K (Number Timestamp))
paulson@13926
   129
                  \<in> set evs"
paulson@18886
   130
apply (cut_tac sesKlife_LB)
paulson@13926
   131
apply (intro exI bexI)
paulson@14207
   132
apply (rule_tac [2]
paulson@18886
   133
           bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
paulson@18886
   134
                             THEN bankerberos.BK3, THEN bankerberos.BK4])
nipkow@25134
   135
apply (possibility, simp_all (no_asm_simp) add: used_Cons)
paulson@13926
   136
done
paulson@13926
   137
paulson@18886
   138
subsection{*Lemmas for reasoning about predicate "Issues"*}
paulson@13926
   139
paulson@18886
   140
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
paulson@18886
   141
apply (induct_tac "evs")
blanchet@55417
   142
apply (rename_tac [2] a b)
paulson@18886
   143
apply (induct_tac [2] "a", auto)
paulson@18886
   144
done
paulson@18886
   145
paulson@18886
   146
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
paulson@18886
   147
apply (induct_tac "evs")
blanchet@55417
   148
apply (rename_tac [2] a b)
paulson@18886
   149
apply (induct_tac [2] "a", auto)
paulson@18886
   150
done
paulson@18886
   151
paulson@18886
   152
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
paulson@18886
   153
          (if A:bad then insert X (spies evs) else spies evs)"
paulson@18886
   154
apply (induct_tac "evs")
blanchet@55417
   155
apply (rename_tac [2] a b)
paulson@18886
   156
apply (induct_tac [2] "a", auto)
paulson@18886
   157
done
paulson@18886
   158
paulson@18886
   159
lemma spies_evs_rev: "spies evs = spies (rev evs)"
paulson@18886
   160
apply (induct_tac "evs")
blanchet@55417
   161
apply (rename_tac [2] a b)
paulson@18886
   162
apply (induct_tac [2] "a")
paulson@18886
   163
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
paulson@18886
   164
done
paulson@18886
   165
paulson@18886
   166
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
paulson@18886
   167
paulson@18886
   168
lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
paulson@18886
   169
apply (induct_tac "evs")
blanchet@55417
   170
apply (rename_tac [2] a b)
paulson@18886
   171
apply (induct_tac [2] "a", auto)
paulson@18886
   172
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
paulson@18886
   173
done
paulson@18886
   174
paulson@18886
   175
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
paulson@18886
   176
paulson@18886
   177
paulson@18886
   178
text{*Lemmas for reasoning about predicate "before"*}
paulson@39251
   179
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
paulson@18886
   180
apply (induct_tac "evs")
paulson@18886
   181
apply simp
blanchet@55417
   182
apply (rename_tac a b)
paulson@18886
   183
apply (induct_tac "a")
paulson@18886
   184
apply auto
paulson@18886
   185
done
paulson@13926
   186
paulson@39251
   187
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
paulson@18886
   188
apply (induct_tac "evs")
paulson@18886
   189
apply simp
blanchet@55417
   190
apply (rename_tac a b)
paulson@18886
   191
apply (induct_tac "a")
paulson@18886
   192
apply auto
paulson@18886
   193
done
paulson@18886
   194
paulson@39251
   195
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
paulson@18886
   196
apply (induct_tac "evs")
paulson@18886
   197
apply simp
blanchet@55417
   198
apply (rename_tac a b)
paulson@18886
   199
apply (induct_tac "a")
paulson@18886
   200
apply auto
paulson@18886
   201
done
paulson@18886
   202
paulson@18886
   203
lemma used_evs_rev: "used evs = used (rev evs)"
paulson@18886
   204
apply (induct_tac "evs")
paulson@18886
   205
apply simp
blanchet@55417
   206
apply (rename_tac a b)
paulson@18886
   207
apply (induct_tac "a")
paulson@18886
   208
apply (simp add: used_Says_rev)
paulson@18886
   209
apply (simp add: used_Gets_rev)
paulson@18886
   210
apply (simp add: used_Notes_rev)
paulson@18886
   211
done
paulson@18886
   212
paulson@18886
   213
lemma used_takeWhile_used [rule_format]: 
paulson@18886
   214
      "x : used (takeWhile P X) --> x : used X"
paulson@18886
   215
apply (induct_tac "X")
paulson@18886
   216
apply simp
blanchet@55417
   217
apply (rename_tac a b)
paulson@18886
   218
apply (induct_tac "a")
paulson@18886
   219
apply (simp_all add: used_Nil)
paulson@18886
   220
apply (blast dest!: initState_into_used)+
paulson@18886
   221
done
paulson@18886
   222
paulson@18886
   223
lemma set_evs_rev: "set evs = set (rev evs)"
paulson@18886
   224
apply auto
paulson@18886
   225
done
paulson@18886
   226
paulson@18886
   227
lemma takeWhile_void [rule_format]:
paulson@18886
   228
      "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
paulson@18886
   229
apply auto
paulson@18886
   230
done
paulson@18886
   231
paulson@18886
   232
(**** Inductive proofs about bankerberos ****)
paulson@18886
   233
paulson@18886
   234
text{*Forwarding Lemma for reasoning about the encrypted portion of message BK3*}
paulson@18886
   235
lemma BK3_msg_in_parts_spies:
paulson@18886
   236
     "Says S A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs
paulson@18886
   237
      \<Longrightarrow> X \<in> parts (spies evs)"
paulson@18886
   238
apply blast
paulson@18886
   239
done
paulson@14207
   240
paulson@13926
   241
lemma Oops_parts_spies:
paulson@18886
   242
     "Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs
paulson@18886
   243
      \<Longrightarrow> K \<in> parts (spies evs)"
paulson@18886
   244
apply blast
paulson@18886
   245
done
paulson@13926
   246
paulson@14207
   247
text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
paulson@13926
   248
lemma Spy_see_shrK [simp]:
paulson@18886
   249
     "evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@18886
   250
apply (erule bankerberos.induct)
paulson@14207
   251
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   252
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast+)
paulson@13926
   253
done
paulson@5053
   254
paulson@5053
   255
paulson@13926
   256
lemma Spy_analz_shrK [simp]:
paulson@18886
   257
     "evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@18886
   258
apply auto
paulson@18886
   259
done
paulson@13926
   260
paulson@13926
   261
lemma Spy_see_shrK_D [dest!]:
paulson@18886
   262
     "\<lbrakk> Key (shrK A) \<in> parts (spies evs);
paulson@18886
   263
                evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A:bad"
paulson@18886
   264
apply (blast dest: Spy_see_shrK)
paulson@18886
   265
done
paulson@13926
   266
paulson@13926
   267
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D,  dest!]
paulson@13926
   268
paulson@13926
   269
paulson@14207
   270
text{*Nobody can have used non-existent keys!*}
paulson@14207
   271
lemma new_keys_not_used [simp]:
paulson@18886
   272
    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerberos\<rbrakk>
paulson@18886
   273
     \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
paulson@14207
   274
apply (erule rev_mp)
paulson@18886
   275
apply (erule bankerberos.induct)
paulson@14207
   276
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   277
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all)
paulson@14207
   278
txt{*Fake*}
paulson@13926
   279
apply (force dest!: keysFor_parts_insert)
paulson@18886
   280
txt{*BK2, BK3, BK4*}
paulson@14207
   281
apply (force dest!: analz_shrK_Decrypt)+
paulson@13926
   282
done
paulson@13926
   283
paulson@14207
   284
subsection{* Lemmas concerning the form of items passed in messages *}
paulson@13926
   285
paulson@14207
   286
text{*Describes the form of K, X and K' when the Server sends this message.*}
paulson@13926
   287
lemma Says_Server_message_form:
paulson@18886
   288
     "\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
paulson@18886
   289
         \<in> set evs; evs \<in> bankerberos \<rbrakk>
paulson@18886
   290
      \<Longrightarrow> K' = shrK A & K \<notin> range shrK &
paulson@18886
   291
          Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) &
paulson@18886
   292
          Key K \<notin> used(before
paulson@18886
   293
                  Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
paulson@18886
   294
                  on evs) &
paulson@18886
   295
          Tk = CT(before 
paulson@18886
   296
                  Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
paulson@18886
   297
                  on evs)"
paulson@18886
   298
apply (unfold before_def)
paulson@13926
   299
apply (erule rev_mp)
paulson@32406
   300
apply (erule bankerberos.induct, simp_all add: takeWhile_tail)
blanchet@42749
   301
apply auto
blanchet@42749
   302
 apply (metis length_rev set_rev takeWhile_void used_evs_rev)+
paulson@13926
   303
done
paulson@5053
   304
paulson@5053
   305
paulson@14207
   306
text{*If the encrypted message appears then it originated with the Server
paulson@13926
   307
  PROVIDED that A is NOT compromised!
paulson@18886
   308
  This allows A to verify freshness of the session key.
paulson@14207
   309
*}
paulson@18886
   310
lemma Kab_authentic:
paulson@18886
   311
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>
paulson@14207
   312
           \<in> parts (spies evs);
paulson@18886
   313
         A \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   314
       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
paulson@13926
   315
             \<in> set evs"
paulson@13926
   316
apply (erule rev_mp)
paulson@18886
   317
apply (erule bankerberos.induct)
paulson@14207
   318
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   319
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast)
paulson@13926
   320
done
paulson@13926
   321
paulson@13926
   322
paulson@14207
   323
text{*If the TICKET appears then it originated with the Server*}
paulson@14207
   324
text{*FRESHNESS OF THE SESSION KEY to B*}
paulson@18886
   325
lemma ticket_authentic:
paulson@18886
   326
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs);
paulson@18886
   327
         B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   328
       \<Longrightarrow> Says Server A
paulson@18886
   329
            (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
paulson@18886
   330
                          Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
paulson@13926
   331
           \<in> set evs"
paulson@13926
   332
apply (erule rev_mp)
paulson@18886
   333
apply (erule bankerberos.induct)
paulson@14207
   334
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   335
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast)
paulson@13926
   336
done
paulson@13926
   337
paulson@13926
   338
paulson@14207
   339
text{*EITHER describes the form of X when the following message is sent,
paulson@13926
   340
  OR     reduces it to the Fake case.
paulson@14207
   341
  Use @{text Says_Server_message_form} if applicable.*}
paulson@13926
   342
lemma Says_S_message_form:
paulson@18886
   343
     "\<lbrakk> Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
paulson@14207
   344
            \<in> set evs;
paulson@18886
   345
         evs \<in> bankerberos \<rbrakk>
paulson@18886
   346
 \<Longrightarrow> (K \<notin> range shrK & X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>))
paulson@13926
   347
          | X \<in> analz (spies evs)"
paulson@13926
   348
apply (case_tac "A \<in> bad")
paulson@13926
   349
apply (force dest!: Says_imp_spies [THEN analz.Inj])
paulson@13926
   350
apply (frule Says_imp_spies [THEN parts.Inj])
paulson@18886
   351
apply (blast dest!: Kab_authentic Says_Server_message_form)
paulson@13926
   352
done
paulson@13926
   353
paulson@5053
   354
paulson@5053
   355
paulson@13926
   356
(****
paulson@13926
   357
 The following is to prove theorems of the form
paulson@13926
   358
paulson@18886
   359
  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
paulson@13926
   360
  Key K \<in> analz (spies evs)
paulson@13926
   361
paulson@13926
   362
 A more general formula must be proved inductively.
paulson@13926
   363
paulson@13926
   364
****)
paulson@13926
   365
paulson@14207
   366
text{* Session keys are not used to encrypt other session keys *}
paulson@13926
   367
lemma analz_image_freshK [rule_format (no_asm)]:
paulson@18886
   368
     "evs \<in> bankerberos \<Longrightarrow>
paulson@18886
   369
   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
paulson@14207
   370
          (Key K \<in> analz (Key`KK Un (spies evs))) =
paulson@13926
   371
          (K \<in> KK | Key K \<in> analz (spies evs))"
paulson@18886
   372
apply (erule bankerberos.induct)
paulson@13926
   373
apply (drule_tac [7] Says_Server_message_form)
paulson@14207
   374
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) 
paulson@13926
   375
done
paulson@13926
   376
paulson@13926
   377
paulson@13926
   378
lemma analz_insert_freshK:
paulson@18886
   379
     "\<lbrakk> evs \<in> bankerberos;  KAB \<notin> range shrK \<rbrakk> \<Longrightarrow>
paulson@14207
   380
      (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@13926
   381
      (K = KAB | Key K \<in> analz (spies evs))"
paulson@18886
   382
apply (simp only: analz_image_freshK analz_image_freshK_simps)
paulson@18886
   383
done
paulson@13926
   384
paulson@14207
   385
text{* The session key K uniquely identifies the message *}
paulson@13926
   386
lemma unique_session_keys:
paulson@18886
   387
     "\<lbrakk> Says Server A
paulson@18886
   388
           (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@14207
   389
         Says Server A'
paulson@18886
   390
          (Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs;
paulson@18886
   391
         evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A=A' & Tk=Tk' & B=B' & X = X'"
paulson@13926
   392
apply (erule rev_mp)
paulson@13926
   393
apply (erule rev_mp)
paulson@18886
   394
apply (erule bankerberos.induct)
paulson@14207
   395
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   396
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all)
paulson@18886
   397
txt{*BK2: it can't be a new key*}
paulson@18886
   398
apply blast
paulson@18886
   399
done
paulson@18886
   400
paulson@18886
   401
lemma Server_Unique:
paulson@18886
   402
     "\<lbrakk> Says Server A
paulson@18886
   403
            (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
paulson@18886
   404
        evs \<in> bankerberos \<rbrakk> \<Longrightarrow> 
paulson@18886
   405
   Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
paulson@18886
   406
   on evs"
paulson@18886
   407
apply (erule rev_mp, erule bankerberos.induct, simp_all add: Unique_def)
paulson@13926
   408
apply blast
paulson@13926
   409
done
paulson@13926
   410
paulson@13926
   411
paulson@18886
   412
subsection{*Non-temporal guarantees, explicitly relying on non-occurrence of
paulson@18886
   413
oops events - refined below by temporal guarantees*}
paulson@18886
   414
paulson@18886
   415
text{*Non temporal treatment of confidentiality*}
paulson@18886
   416
paulson@18886
   417
text{* Lemma: the session key sent in msg BK2 would be lost by oops
paulson@14207
   418
    if the spy could see it! *}
paulson@18886
   419
lemma lemma_conf [rule_format (no_asm)]:
paulson@18886
   420
     "\<lbrakk> A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   421
  \<Longrightarrow> Says Server A
paulson@18886
   422
          (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
paulson@18886
   423
                            Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
paulson@18886
   424
         \<in> set evs \<longrightarrow>
paulson@18886
   425
      Key K \<in> analz (spies evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs"
paulson@18886
   426
apply (erule bankerberos.induct)
paulson@18886
   427
apply (frule_tac [7] Says_Server_message_form)
paulson@18886
   428
apply (frule_tac [5] Says_S_message_form [THEN disjE])
paulson@18886
   429
apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes)
paulson@18886
   430
txt{*Fake*}
paulson@18886
   431
apply spy_analz
paulson@18886
   432
txt{*BK2*}
paulson@18886
   433
apply (blast intro: parts_insertI)
paulson@18886
   434
txt{*BK3*}
paulson@18886
   435
apply (case_tac "Aa \<in> bad")
paulson@18886
   436
 prefer 2 apply (blast dest: Kab_authentic unique_session_keys)
paulson@18886
   437
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz)
paulson@18886
   438
txt{*Oops*}
paulson@18886
   439
apply (blast dest: unique_session_keys)
paulson@18886
   440
done
paulson@18886
   441
paulson@18886
   442
paulson@18886
   443
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2
paulson@18886
   444
as long as they have not expired.*}
paulson@18886
   445
lemma Confidentiality_S:
paulson@18886
   446
     "\<lbrakk> Says Server A
paulson@18886
   447
          (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
paulson@18886
   448
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
paulson@18886
   449
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   450
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@18886
   451
apply (frule Says_Server_message_form, assumption)
paulson@18886
   452
apply (blast intro: lemma_conf)
paulson@18886
   453
done
paulson@18886
   454
paulson@18886
   455
text{*Confidentiality for Alice*}
paulson@18886
   456
lemma Confidentiality_A:
paulson@18886
   457
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   458
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
paulson@18886
   459
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   460
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@18886
   461
apply (blast dest!: Kab_authentic Confidentiality_S)
paulson@18886
   462
done
paulson@18886
   463
paulson@18886
   464
text{*Confidentiality for Bob*}
paulson@18886
   465
lemma Confidentiality_B:
paulson@18886
   466
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
paulson@18886
   467
          \<in> parts (spies evs);
paulson@18886
   468
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
paulson@18886
   469
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   470
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@18886
   471
apply (blast dest!: ticket_authentic Confidentiality_S)
paulson@18886
   472
done
paulson@18886
   473
paulson@18886
   474
text{*Non temporal treatment of authentication*}
paulson@13926
   475
paulson@18886
   476
text{*Lemmas @{text lemma_A} and @{text lemma_B} in fact are common to both temporal and non-temporal treatments*}
paulson@18886
   477
lemma lemma_A [rule_format]:
paulson@18886
   478
     "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk>
paulson@18886
   479
      \<Longrightarrow>
paulson@18886
   480
         Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@18886
   481
         Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
paulson@18886
   482
         \<in> set evs \<longrightarrow>
paulson@18886
   483
          Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs) \<longrightarrow>
paulson@18886
   484
         Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace>
paulson@18886
   485
             \<in> set evs"
paulson@18886
   486
apply (erule bankerberos.induct)
paulson@18886
   487
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   488
apply (frule_tac [5] Says_S_message_form)
paulson@18886
   489
apply (frule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra)
paulson@18886
   490
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
   491
txt{*Fake*}
paulson@18886
   492
apply blast
paulson@18886
   493
txt{*BK2*}
paulson@18886
   494
apply (force dest: Crypt_imp_invKey_keysFor)
paulson@18886
   495
txt{*BK3*}
paulson@18886
   496
apply (blast dest: Kab_authentic unique_session_keys)
paulson@18886
   497
done
paulson@32406
   498
paulson@18886
   499
lemma lemma_B [rule_format]:
paulson@18886
   500
     "\<lbrakk> B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   501
      \<Longrightarrow> Key K \<notin> analz (spies evs) \<longrightarrow>
paulson@18886
   502
          Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
paulson@18886
   503
          \<in> set evs \<longrightarrow>
paulson@18886
   504
          Crypt K (Number Ta) \<in> parts (spies evs) \<longrightarrow>
paulson@18886
   505
          Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@18886
   506
apply (erule bankerberos.induct)
paulson@18886
   507
apply (frule_tac [7] Oops_parts_spies)
paulson@18886
   508
apply (frule_tac [5] Says_S_message_form)
paulson@18886
   509
apply (drule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra)
paulson@18886
   510
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
   511
txt{*Fake*}
paulson@18886
   512
apply blast
paulson@18886
   513
txt{*BK2*} 
paulson@18886
   514
apply (force dest: Crypt_imp_invKey_keysFor)
paulson@18886
   515
txt{*BK4*}
paulson@18886
   516
apply (blast dest: ticket_authentic unique_session_keys
paulson@18886
   517
                   Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
paulson@18886
   518
done
paulson@18886
   519
paulson@18886
   520
paulson@18886
   521
text{*The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
paulson@18886
   522
paulson@18886
   523
paulson@18886
   524
text{*Authentication of A to B*}
paulson@18886
   525
lemma B_authenticates_A_r:
paulson@18886
   526
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs);
paulson@18886
   527
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>  \<in> parts (spies evs);
paulson@18886
   528
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
paulson@18886
   529
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   530
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
paulson@18886
   531
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   532
apply (blast dest!: ticket_authentic
paulson@18886
   533
          intro!: lemma_A
paulson@18886
   534
          elim!: Confidentiality_S [THEN [2] rev_notE])
paulson@18886
   535
done
paulson@18886
   536
paulson@18886
   537
paulson@18886
   538
text{*Authentication of B to A*}
paulson@18886
   539
lemma A_authenticates_B_r:
paulson@18886
   540
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs);
paulson@18886
   541
        Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   542
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
paulson@18886
   543
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   544
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@18886
   545
apply (blast dest!: Kab_authentic
paulson@18886
   546
          intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
paulson@18886
   547
done
paulson@18886
   548
paulson@18886
   549
lemma B_authenticates_A:
paulson@18886
   550
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs);
paulson@18886
   551
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>  \<in> parts (spies evs);
paulson@18886
   552
        Key K \<notin> analz (spies evs);
paulson@18886
   553
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   554
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
paulson@18886
   555
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   556
apply (blast dest!: ticket_authentic intro!: lemma_A)
paulson@18886
   557
done
paulson@18886
   558
paulson@18886
   559
lemma A_authenticates_B:
paulson@18886
   560
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs);
paulson@18886
   561
        Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   562
        Key K \<notin> analz (spies evs);
paulson@18886
   563
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   564
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@18886
   565
apply (blast dest!: Kab_authentic intro!: lemma_B)
paulson@18886
   566
done
paulson@18886
   567
paulson@18886
   568
subsection{*Temporal guarantees, relying on a temporal check that insures that
paulson@18886
   569
no oops event occurred. These are available in the sense of goal availability*}
paulson@18886
   570
paulson@18886
   571
paulson@18886
   572
text{*Temporal treatment of confidentiality*}
paulson@18886
   573
paulson@18886
   574
text{* Lemma: the session key sent in msg BK2 would be EXPIRED
paulson@18886
   575
    if the spy could see it! *}
paulson@18886
   576
lemma lemma_conf_temporal [rule_format (no_asm)]:
paulson@18886
   577
     "\<lbrakk> A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   578
  \<Longrightarrow> Says Server A
paulson@18886
   579
          (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
paulson@18886
   580
                            Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
paulson@18886
   581
         \<in> set evs \<longrightarrow>
paulson@18886
   582
      Key K \<in> analz (spies evs) \<longrightarrow> expiredK Tk evs"
paulson@18886
   583
apply (erule bankerberos.induct)
paulson@13926
   584
apply (frule_tac [7] Says_Server_message_form)
paulson@13926
   585
apply (frule_tac [5] Says_S_message_form [THEN disjE])
paulson@13926
   586
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
paulson@13926
   587
txt{*Fake*}
paulson@13926
   588
apply spy_analz
paulson@18886
   589
txt{*BK2*}
paulson@13926
   590
apply (blast intro: parts_insertI less_SucI)
paulson@18886
   591
txt{*BK3*}
paulson@32406
   592
apply (metis Crypt_Spy_analz_bad Kab_authentic Says_imp_analz_Spy 
paulson@32406
   593
          Says_imp_parts_knows_Spy analz.Snd less_SucI unique_session_keys)
paulson@18886
   594
txt{*Oops: PROOF FAILS if unsafe intro below*}
paulson@13926
   595
apply (blast dest: unique_session_keys intro!: less_SucI)
paulson@13926
   596
done
paulson@5053
   597
paulson@5053
   598
paulson@18886
   599
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2
paulson@14207
   600
as long as they have not expired.*}
paulson@18886
   601
lemma Confidentiality_S_temporal:
paulson@18886
   602
     "\<lbrakk> Says Server A
paulson@18886
   603
          (Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs;
paulson@18886
   604
         \<not> expiredK T evs;
paulson@18886
   605
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   606
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@13926
   607
apply (frule Says_Server_message_form, assumption)
paulson@18886
   608
apply (blast intro: lemma_conf_temporal)
paulson@13926
   609
done
paulson@13926
   610
paulson@14207
   611
text{*Confidentiality for Alice*}
paulson@18886
   612
lemma Confidentiality_A_temporal:
paulson@18886
   613
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   614
         \<not> expiredK T evs;
paulson@18886
   615
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   616
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@18886
   617
apply (blast dest!: Kab_authentic Confidentiality_S_temporal)
paulson@18886
   618
done
paulson@13926
   619
paulson@14207
   620
text{*Confidentiality for Bob*}
paulson@18886
   621
lemma Confidentiality_B_temporal:
paulson@18886
   622
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
paulson@14207
   623
          \<in> parts (spies evs);
paulson@18886
   624
        \<not> expiredK Tk evs;
paulson@18886
   625
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos
paulson@18886
   626
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)"
paulson@18886
   627
apply (blast dest!: ticket_authentic Confidentiality_S_temporal)
paulson@18886
   628
done
paulson@18886
   629
paulson@18886
   630
text{*Temporal treatment of authentication*}
paulson@18886
   631
paulson@18886
   632
text{*Authentication of A to B*}
paulson@18886
   633
lemma B_authenticates_A_temporal:
paulson@18886
   634
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs);
paulson@18886
   635
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
paulson@18886
   636
         \<in> parts (spies evs);
paulson@18886
   637
         \<not> expiredK Tk evs;
paulson@18886
   638
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   639
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
paulson@18886
   640
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   641
apply (blast dest!: ticket_authentic
paulson@18886
   642
          intro!: lemma_A
paulson@18886
   643
          elim!: Confidentiality_S_temporal [THEN [2] rev_notE])
paulson@18886
   644
done
paulson@18886
   645
paulson@18886
   646
text{*Authentication of B to A*}
paulson@18886
   647
lemma A_authenticates_B_temporal:
paulson@18886
   648
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs);
paulson@18886
   649
         Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>
paulson@18886
   650
         \<in> parts (spies evs);
paulson@18886
   651
         \<not> expiredK Tk evs;
paulson@18886
   652
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   653
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@18886
   654
apply (blast dest!: Kab_authentic
paulson@18886
   655
          intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE])
paulson@18886
   656
done
paulson@18886
   657
paulson@18886
   658
subsection{*Treatment of the key distribution goal using trace inspection. All
paulson@18886
   659
guarantees are in non-temporal form, hence non available, though their temporal
paulson@18886
   660
form is trivial to derive. These guarantees also convey a stronger form of 
paulson@18886
   661
authentication - non-injective agreement on the session key*}
paulson@13926
   662
paulson@5053
   663
paulson@18886
   664
lemma B_Issues_A:
paulson@18886
   665
     "\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs;
paulson@18886
   666
         Key K \<notin> analz (spies evs);
paulson@18886
   667
         A \<notin> bad;  B \<notin> bad; evs \<in> bankerberos \<rbrakk>
paulson@18886
   668
      \<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs"
paulson@18886
   669
apply (simp (no_asm) add: Issues_def)
paulson@18886
   670
apply (rule exI)
paulson@18886
   671
apply (rule conjI, assumption)
paulson@18886
   672
apply (simp (no_asm))
paulson@18886
   673
apply (erule rev_mp)
paulson@18886
   674
apply (erule rev_mp)
paulson@18886
   675
apply (erule bankerberos.induct, analz_mono_contra)
paulson@18886
   676
apply (simp_all (no_asm_simp))
paulson@18886
   677
txt{*fake*}
paulson@13926
   678
apply blast
paulson@18886
   679
txt{*K4 obviously is the non-trivial case*}
paulson@18886
   680
apply (simp add: takeWhile_tail)
paulson@18886
   681
apply (blast dest: ticket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: A_authenticates_B_temporal)
paulson@18886
   682
done
paulson@18886
   683
paulson@18886
   684
lemma A_authenticates_and_keydist_to_B:
paulson@18886
   685
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs);
paulson@18886
   686
        Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
paulson@18886
   687
         Key K \<notin> analz (spies evs);
paulson@18886
   688
         A \<notin> bad;  B \<notin> bad; evs \<in> bankerberos \<rbrakk>
paulson@18886
   689
      \<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs"
paulson@18886
   690
apply (blast dest!: A_authenticates_B B_Issues_A)
paulson@13926
   691
done
paulson@13926
   692
paulson@13926
   693
paulson@18886
   694
lemma A_Issues_B:
paulson@18886
   695
     "\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace>
paulson@18886
   696
           \<in> set evs;
paulson@18886
   697
         Key K \<notin> analz (spies evs);
paulson@18886
   698
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   699
   \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs"
paulson@18886
   700
apply (simp (no_asm) add: Issues_def)
paulson@18886
   701
apply (rule exI)
paulson@18886
   702
apply (rule conjI, assumption)
paulson@18886
   703
apply (simp (no_asm))
paulson@18886
   704
apply (erule rev_mp)
paulson@18886
   705
apply (erule rev_mp)
paulson@18886
   706
apply (erule bankerberos.induct, analz_mono_contra)
paulson@18886
   707
apply (simp_all (no_asm_simp))
paulson@18886
   708
txt{*fake*}
paulson@13926
   709
apply blast
paulson@18886
   710
txt{*K3 is the non trivial case*}
paulson@18886
   711
apply (simp add: takeWhile_tail)
paulson@18886
   712
apply auto (*Technically unnecessary, merely clarifies the subgoal as it is presemted in the book*)
paulson@18886
   713
apply (blast dest: Kab_authentic Says_Server_message_form parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] 
paulson@18886
   714
             intro!: B_authenticates_A)
paulson@13926
   715
done
paulson@13926
   716
paulson@18886
   717
paulson@18886
   718
lemma B_authenticates_and_keydist_to_A:
paulson@18886
   719
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs);
paulson@18886
   720
        Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>  \<in> parts (spies evs);
paulson@18886
   721
        Key K \<notin> analz (spies evs);
paulson@18886
   722
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerberos \<rbrakk>
paulson@18886
   723
   \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs"
paulson@18886
   724
apply (blast dest: B_authenticates_A A_Issues_B)
paulson@18886
   725
done
paulson@18886
   726
paulson@18886
   727
paulson@18886
   728
paulson@5053
   729
paulson@5053
   730
end