src/HOL/Auth/KerberosIV.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 61830 4f5ab843cf5b
child 67443 3abf6a722518
permissions -rw-r--r--
tuned;
wenzelm@37936
     1
(*  Title:      HOL/Auth/KerberosIV.thy
paulson@6452
     2
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
paulson@6452
     3
    Copyright   1998  University of Cambridge
paulson@6452
     4
*)
paulson@6452
     5
wenzelm@61830
     6
section\<open>The Kerberos Protocol, Version IV\<close>
paulson@14207
     7
haftmann@16417
     8
theory KerberosIV imports Public begin
paulson@6452
     9
wenzelm@61830
    10
text\<open>The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.\<close>
paulson@18886
    11
wenzelm@20768
    12
abbreviation
wenzelm@21404
    13
  Kas :: agent where "Kas == Server"
paulson@6452
    14
wenzelm@21404
    15
abbreviation
wenzelm@21404
    16
  Tgs :: agent where "Tgs == Friend 0"
paulson@6452
    17
paulson@6452
    18
wenzelm@41774
    19
axiomatization where
paulson@14182
    20
  Tgs_not_bad [iff]: "Tgs \<notin> bad"
wenzelm@61830
    21
   \<comment>\<open>Tgs is secure --- we already know that Kas is secure\<close>
paulson@14182
    22
wenzelm@36866
    23
definition
paulson@18886
    24
 (* authKeys are those contained in an authTicket *)
wenzelm@36866
    25
    authKeys :: "event list => key set" where
wenzelm@36866
    26
    "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
paulson@18886
    27
                        (Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
paulson@18886
    28
               (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
paulson@18886
    29
                  \<rbrace>) \<in> set evs}"
paulson@14182
    30
wenzelm@36866
    31
definition
paulson@6452
    32
 (* A is the true creator of X if she has sent X and X never appeared on
paulson@6452
    33
    the trace before this event. Recall that traces grow from head. *)
paulson@14182
    34
  Issues :: "[agent, agent, msg, event list] => bool"
paulson@37811
    35
             ("_ Issues _ with _ on _" [50, 0, 0, 50] 50) where
paulson@37811
    36
   "(A Issues B with X on evs) =
wenzelm@36866
    37
      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
wenzelm@36866
    38
        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
paulson@6452
    39
wenzelm@36866
    40
definition
paulson@18886
    41
 (* Yields the subtrace of a given trace from its beginning to a given event *)
paulson@37811
    42
  before :: "[event, event list] => event list" ("before _ on _" [0, 50] 50)
paulson@37811
    43
  where "(before ev on evs) = takeWhile (% z. z ~= ev) (rev evs)"
paulson@18886
    44
wenzelm@36866
    45
definition
paulson@18886
    46
 (* States than an event really appears only once on a trace *)
paulson@37811
    47
  Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50)
paulson@37811
    48
  where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
paulson@18886
    49
paulson@6452
    50
paulson@6452
    51
consts
paulson@6452
    52
    (*Duration of the authentication key*)
paulson@18886
    53
    authKlife   :: nat
paulson@6452
    54
paulson@6452
    55
    (*Duration of the service key*)
paulson@18886
    56
    servKlife   :: nat
paulson@6452
    57
paulson@6452
    58
    (*Duration of an authenticator*)
paulson@18886
    59
    authlife   :: nat
paulson@6452
    60
paulson@6452
    61
    (*Upper bound on the time of reaction of a server*)
paulson@18886
    62
    replylife   :: nat
paulson@14182
    63
paulson@18886
    64
specification (authKlife)
paulson@18886
    65
  authKlife_LB [iff]: "2 \<le> authKlife"
paulson@14182
    66
    by blast
paulson@6452
    67
paulson@18886
    68
specification (servKlife)
paulson@18886
    69
  servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
paulson@14182
    70
    by blast
paulson@14182
    71
paulson@18886
    72
specification (authlife)
paulson@18886
    73
  authlife_LB [iff]: "Suc 0 \<le> authlife"
paulson@14182
    74
    by blast
paulson@14182
    75
paulson@18886
    76
specification (replylife)
paulson@18886
    77
  replylife_LB [iff]: "Suc 0 \<le> replylife"
paulson@14182
    78
    by blast
paulson@6452
    79
wenzelm@20768
    80
abbreviation
wenzelm@20768
    81
  (*The current time is the length of the trace*)
wenzelm@21404
    82
  CT :: "event list=>nat" where
wenzelm@20768
    83
  "CT == length"
paulson@6452
    84
wenzelm@21404
    85
abbreviation
wenzelm@21404
    86
  expiredAK :: "[nat, event list] => bool" where
wenzelm@20768
    87
  "expiredAK Ta evs == authKlife + Ta < CT evs"
paulson@6452
    88
wenzelm@21404
    89
abbreviation
wenzelm@21404
    90
  expiredSK :: "[nat, event list] => bool" where
wenzelm@20768
    91
  "expiredSK Ts evs == servKlife + Ts < CT evs"
paulson@6452
    92
wenzelm@21404
    93
abbreviation
wenzelm@21404
    94
  expiredA :: "[nat, event list] => bool" where
wenzelm@20768
    95
  "expiredA T evs == authlife + T < CT evs"
paulson@6452
    96
wenzelm@21404
    97
abbreviation
paulson@37811
    98
  valid :: "[nat, nat] => bool" ("valid _ wrt _" [0, 50] 50) where
wenzelm@20768
    99
  "valid T1 wrt T2 == T1 <= replylife + T2"
paulson@6452
   100
paulson@6452
   101
(*---------------------------------------------------------------------*)
paulson@6452
   102
paulson@6452
   103
paulson@18886
   104
(* Predicate formalising the association between authKeys and servKeys *)
haftmann@35416
   105
definition AKcryptSK :: "[key, key, event list] => bool" where
paulson@18886
   106
  "AKcryptSK authK servK evs ==
paulson@18886
   107
     \<exists>A B Ts.
paulson@18886
   108
       Says Tgs A (Crypt authK
paulson@18886
   109
                     \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   110
                       Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
paulson@14182
   111
         \<in> set evs"
paulson@6452
   112
berghofe@23746
   113
inductive_set kerbIV :: "event list set"
berghofe@23746
   114
  where
paulson@6452
   115
paulson@18886
   116
   Nil:  "[] \<in> kerbIV"
paulson@14182
   117
berghofe@23746
   118
 | Fake: "\<lbrakk> evsf \<in> kerbIV;  X \<in> synth (analz (spies evsf)) \<rbrakk>
paulson@18886
   119
          \<Longrightarrow> Says Spy B X  # evsf \<in> kerbIV"
paulson@6452
   120
paulson@6452
   121
(* FROM the initiator *)
berghofe@23746
   122
 | K1:   "\<lbrakk> evs1 \<in> kerbIV \<rbrakk>
paulson@18886
   123
          \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
paulson@18886
   124
          \<in> kerbIV"
paulson@6452
   125
paulson@6452
   126
(* Adding the timestamp serves to A in K3 to check that
paulson@14182
   127
   she doesn't get a reply too late. This kind of timeouts are ordinary.
paulson@6452
   128
   If a server's reply is late, then it is likely to be fake. *)
paulson@6452
   129
paulson@6452
   130
(*---------------------------------------------------------------------*)
paulson@6452
   131
paulson@6452
   132
(*FROM Kas *)
berghofe@23746
   133
 | K2:  "\<lbrakk> evs2 \<in> kerbIV; Key authK \<notin> used evs2; authK \<in> symKeys;
paulson@18886
   134
            Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
paulson@18886
   135
          \<Longrightarrow> Says Kas A
paulson@18886
   136
                (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2),
paulson@18886
   137
                      (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
paulson@18886
   138
                          Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV"
paulson@14182
   139
(*
paulson@18886
   140
  The internal encryption builds the authTicket.
paulson@6452
   141
  The timestamp doesn't change inside the two encryptions: the external copy
paulson@14182
   142
  will be used by the initiator in K3; the one inside the
paulson@18886
   143
  authTicket by Tgs in K4.
paulson@6452
   144
*)
paulson@6452
   145
paulson@6452
   146
(*---------------------------------------------------------------------*)
paulson@6452
   147
paulson@6452
   148
(* FROM the initiator *)
berghofe@23746
   149
 | K3:  "\<lbrakk> evs3 \<in> kerbIV;
paulson@18886
   150
            Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
paulson@18886
   151
            Says Kas' A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   152
              authTicket\<rbrace>) \<in> set evs3;
paulson@18886
   153
            valid Ta wrt T1
paulson@18886
   154
         \<rbrakk>
paulson@18886
   155
          \<Longrightarrow> Says A Tgs \<lbrace>authTicket,
paulson@18886
   156
                           (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
paulson@18886
   157
                           Agent B\<rbrace> # evs3 \<in> kerbIV"
paulson@18886
   158
(*The two events amongst the premises allow A to accept only those authKeys
paulson@6452
   159
  that are not issued late. *)
paulson@6452
   160
paulson@6452
   161
(*---------------------------------------------------------------------*)
paulson@6452
   162
paulson@6452
   163
(* FROM Tgs *)
paulson@6452
   164
(* Note that the last temporal check is not mentioned in the original MIT
paulson@18886
   165
   specification. Adding it makes many goals "available" to the peers. 
paulson@18886
   166
   Theorems that exploit it have the suffix `_u', which stands for updated 
paulson@18886
   167
   protocol.
paulson@14182
   168
*)
berghofe@23746
   169
 | K4:  "\<lbrakk> evs4 \<in> kerbIV; Key servK \<notin> used evs4; servK \<in> symKeys;
paulson@18886
   170
            B \<noteq> Tgs;  authK \<in> symKeys;
paulson@18886
   171
            Says A' Tgs \<lbrace>
paulson@18886
   172
             (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
wenzelm@32960
   173
                                 Number Ta\<rbrace>),
paulson@18886
   174
             (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
wenzelm@32960
   175
                \<in> set evs4;
paulson@18886
   176
            \<not> expiredAK Ta evs4;
paulson@18886
   177
            \<not> expiredA T2 evs4;
paulson@18886
   178
            servKlife + (CT evs4) <= authKlife + Ta
paulson@18886
   179
         \<rbrakk>
paulson@18886
   180
          \<Longrightarrow> Says Tgs A
paulson@18886
   181
                (Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4),
wenzelm@32960
   182
                               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK,
wenzelm@32960
   183
                                                Number (CT evs4)\<rbrace> \<rbrace>)
wenzelm@32960
   184
                # evs4 \<in> kerbIV"
paulson@14182
   185
(* Tgs creates a new session key per each request for a service, without
paulson@6452
   186
   checking if there is still a fresh one for that service.
paulson@18886
   187
   The cipher under Tgs' key is the authTicket, the cipher under B's key
paulson@18886
   188
   is the servTicket, which is built now.
paulson@6452
   189
   NOTE that the last temporal check is not present in the MIT specification.
paulson@14182
   190
paulson@6452
   191
*)
paulson@6452
   192
paulson@6452
   193
(*---------------------------------------------------------------------*)
paulson@6452
   194
paulson@6452
   195
(* FROM the initiator *)
berghofe@23746
   196
 | K5:  "\<lbrakk> evs5 \<in> kerbIV; authK \<in> symKeys; servK \<in> symKeys;
paulson@14182
   197
            Says A Tgs
paulson@18886
   198
                \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
wenzelm@32960
   199
                  Agent B\<rbrace>
paulson@14182
   200
              \<in> set evs5;
paulson@14182
   201
            Says Tgs' A
paulson@18886
   202
             (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
   203
                \<in> set evs5;
paulson@18886
   204
            valid Ts wrt T2 \<rbrakk>
paulson@18886
   205
          \<Longrightarrow> Says A B \<lbrace>servTicket,
wenzelm@32960
   206
                         Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
paulson@18886
   207
               # evs5 \<in> kerbIV"
paulson@6452
   208
(* Checks similar to those in K3. *)
paulson@6452
   209
paulson@6452
   210
(*---------------------------------------------------------------------*)
paulson@6452
   211
paulson@6452
   212
(* FROM the responder*)
berghofe@23746
   213
  | K6:  "\<lbrakk> evs6 \<in> kerbIV;
paulson@18886
   214
            Says A' B \<lbrace>
paulson@18886
   215
              (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
paulson@18886
   216
              (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
paulson@14182
   217
            \<in> set evs6;
paulson@18886
   218
            \<not> expiredSK Ts evs6;
paulson@18886
   219
            \<not> expiredA T3 evs6
paulson@18886
   220
         \<rbrakk>
paulson@18886
   221
          \<Longrightarrow> Says B A (Crypt servK (Number T3))
paulson@18886
   222
               # evs6 \<in> kerbIV"
paulson@6452
   223
(* Checks similar to those in K4. *)
paulson@6452
   224
paulson@6452
   225
(*---------------------------------------------------------------------*)
paulson@6452
   226
paulson@18886
   227
(* Leaking an authK... *)
berghofe@23746
   228
 | Oops1: "\<lbrakk> evsO1 \<in> kerbIV;  A \<noteq> Spy;
paulson@6452
   229
              Says Kas A
paulson@18886
   230
                (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   231
                                  authTicket\<rbrace>)  \<in> set evsO1;
paulson@18886
   232
              expiredAK Ta evsO1 \<rbrakk>
paulson@18886
   233
          \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
paulson@18886
   234
               # evsO1 \<in> kerbIV"
paulson@6452
   235
paulson@6452
   236
(*---------------------------------------------------------------------*)
paulson@6452
   237
paulson@18886
   238
(*Leaking a servK... *)
berghofe@23746
   239
 | Oops2: "\<lbrakk> evsO2 \<in> kerbIV;  A \<noteq> Spy;
paulson@14182
   240
              Says Tgs A
paulson@18886
   241
                (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
   242
                   \<in> set evsO2;
paulson@18886
   243
              expiredSK Ts evsO2 \<rbrakk>
paulson@18886
   244
          \<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
paulson@18886
   245
               # evsO2 \<in> kerbIV"
paulson@6452
   246
paulson@6452
   247
(*---------------------------------------------------------------------*)
paulson@6452
   248
paulson@14207
   249
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14200
   250
declare parts.Body [dest]
paulson@14200
   251
declare analz_into_parts [dest]
paulson@14200
   252
declare Fake_parts_insert_in_Un [dest]
paulson@14182
   253
paulson@14182
   254
wenzelm@61830
   255
subsection\<open>Lemmas about lists, for reasoning about  Issues\<close>
paulson@14182
   256
paulson@14182
   257
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
paulson@14182
   258
apply (induct_tac "evs")
blanchet@55417
   259
apply (rename_tac [2] a b)
blanchet@55417
   260
apply (induct_tac [2] a, auto)
paulson@14182
   261
done
paulson@14182
   262
paulson@14182
   263
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
paulson@14182
   264
apply (induct_tac "evs")
blanchet@55417
   265
apply (rename_tac [2] a b)
blanchet@55417
   266
apply (induct_tac [2] a, auto)
paulson@14182
   267
done
paulson@14182
   268
paulson@14207
   269
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
paulson@14182
   270
          (if A:bad then insert X (spies evs) else spies evs)"
paulson@14182
   271
apply (induct_tac "evs")
blanchet@55417
   272
apply (rename_tac [2] a b)
blanchet@55417
   273
apply (induct_tac [2] a, auto)
paulson@14182
   274
done
paulson@14182
   275
paulson@14182
   276
lemma spies_evs_rev: "spies evs = spies (rev evs)"
paulson@14182
   277
apply (induct_tac "evs")
blanchet@55417
   278
apply (rename_tac [2] a b)
blanchet@55417
   279
apply (induct_tac [2] a)
paulson@14182
   280
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
paulson@14182
   281
done
paulson@14182
   282
paulson@14182
   283
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
paulson@14182
   284
paulson@14182
   285
lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
paulson@14182
   286
apply (induct_tac "evs")
blanchet@55417
   287
apply (rename_tac [2] a b)
paulson@14182
   288
apply (induct_tac [2] "a", auto)
wenzelm@61830
   289
txt\<open>Resembles \<open>used_subset_append\<close> in theory Event.\<close>
paulson@14182
   290
done
paulson@14182
   291
paulson@14182
   292
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
paulson@14182
   293
paulson@14182
   294
wenzelm@61830
   295
subsection\<open>Lemmas about @{term authKeys}\<close>
paulson@14182
   296
paulson@18886
   297
lemma authKeys_empty: "authKeys [] = {}"
paulson@18886
   298
apply (unfold authKeys_def)
paulson@14182
   299
apply (simp (no_asm))
paulson@14182
   300
done
paulson@14182
   301
paulson@18886
   302
lemma authKeys_not_insert:
paulson@18886
   303
 "(\<forall>A Ta akey Peer.
paulson@18886
   304
   ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
paulson@18886
   305
              (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
paulson@18886
   306
       \<Longrightarrow> authKeys (ev # evs) = authKeys evs"
paulson@18886
   307
by (unfold authKeys_def, auto)
paulson@14182
   308
paulson@18886
   309
lemma authKeys_insert:
paulson@18886
   310
  "authKeys
paulson@18886
   311
     (Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
paulson@18886
   312
      (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
paulson@18886
   313
       = insert K (authKeys evs)"
paulson@18886
   314
by (unfold authKeys_def, auto)
paulson@14182
   315
paulson@18886
   316
lemma authKeys_simp:
paulson@18886
   317
   "K \<in> authKeys
paulson@18886
   318
    (Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
paulson@18886
   319
     (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
paulson@18886
   320
        \<Longrightarrow> K = K' | K \<in> authKeys evs"
paulson@18886
   321
by (unfold authKeys_def, auto)
paulson@14182
   322
paulson@18886
   323
lemma authKeysI:
paulson@18886
   324
   "Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
paulson@18886
   325
     (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
paulson@18886
   326
        \<Longrightarrow> K \<in> authKeys evs"
paulson@18886
   327
by (unfold authKeys_def, auto)
paulson@14182
   328
paulson@18886
   329
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
paulson@18886
   330
by (simp add: authKeys_def, blast)
paulson@14182
   331
paulson@14182
   332
wenzelm@61830
   333
subsection\<open>Forwarding Lemmas\<close>
paulson@14182
   334
wenzelm@61830
   335
text\<open>--For reasoning about the encrypted portion of message K3--\<close>
paulson@14182
   336
lemma K3_msg_in_parts_spies:
paulson@18886
   337
     "Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>)
paulson@18886
   338
               \<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)"
paulson@37811
   339
by blast
paulson@14182
   340
paulson@14182
   341
lemma Oops_range_spies1:
paulson@18886
   342
     "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
paulson@14207
   343
           \<in> set evs ;
paulson@18886
   344
         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
paulson@14182
   345
apply (erule rev_mp)
paulson@18886
   346
apply (erule kerbIV.induct, auto)
paulson@14182
   347
done
paulson@14182
   348
wenzelm@61830
   349
text\<open>--For reasoning about the encrypted portion of message K5--\<close>
paulson@14182
   350
lemma K5_msg_in_parts_spies:
paulson@18886
   351
     "Says Tgs' A (Crypt authK \<lbrace>servK, Agent B, Ts, servTicket\<rbrace>)
paulson@18886
   352
               \<in> set evs \<Longrightarrow> servTicket \<in> parts (spies evs)"
paulson@37811
   353
by blast
paulson@14182
   354
paulson@14182
   355
lemma Oops_range_spies2:
paulson@18886
   356
     "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
paulson@14207
   357
           \<in> set evs ;
paulson@18886
   358
         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys"
paulson@14182
   359
apply (erule rev_mp)
paulson@18886
   360
apply (erule kerbIV.induct, auto)
paulson@14182
   361
done
paulson@14182
   362
paulson@18886
   363
lemma Says_ticket_parts:
paulson@18886
   364
     "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
paulson@18886
   365
      \<Longrightarrow> Ticket \<in> parts (spies evs)"
paulson@37811
   366
by blast
paulson@14182
   367
paulson@14182
   368
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
paulson@14182
   369
lemma Spy_see_shrK [simp]:
paulson@18886
   370
     "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@18886
   371
apply (erule kerbIV.induct)
paulson@14207
   372
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   373
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
paulson@14182
   374
apply (blast+)
paulson@14182
   375
done
paulson@14182
   376
paulson@14182
   377
lemma Spy_analz_shrK [simp]:
paulson@18886
   378
     "evs \<in> kerbIV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@14182
   379
by auto
paulson@14182
   380
paulson@14182
   381
lemma Spy_see_shrK_D [dest!]:
paulson@18886
   382
     "\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A:bad"
paulson@14182
   383
by (blast dest: Spy_see_shrK)
paulson@32366
   384
paulson@14182
   385
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
paulson@14182
   386
wenzelm@61830
   387
text\<open>Nobody can have used non-existent keys!\<close>
paulson@14207
   388
lemma new_keys_not_used [simp]:
paulson@18886
   389
    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV\<rbrakk>
paulson@18886
   390
     \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
paulson@14207
   391
apply (erule rev_mp)
paulson@18886
   392
apply (erule kerbIV.induct)
paulson@14207
   393
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   394
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   395
txt\<open>Fake\<close>
paulson@14182
   396
apply (force dest!: keysFor_parts_insert)
wenzelm@61830
   397
txt\<open>Others\<close>
paulson@14207
   398
apply (force dest!: analz_shrK_Decrypt)+
paulson@14182
   399
done
paulson@14182
   400
paulson@14207
   401
(*Earlier, all protocol proofs declared this theorem.
paulson@14182
   402
  But few of them actually need it! (Another is Yahalom) *)
paulson@14182
   403
lemma new_keys_not_analzd:
paulson@18886
   404
 "\<lbrakk>evs \<in> kerbIV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
paulson@18886
   405
  \<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
paulson@14207
   406
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
paulson@14182
   407
paulson@14182
   408
paulson@18886
   409
wenzelm@61830
   410
subsection\<open>Lemmas for reasoning about predicate "before"\<close>
paulson@18886
   411
paulson@37811
   412
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
paulson@18886
   413
apply (induct_tac "evs")
paulson@18886
   414
apply simp
blanchet@55417
   415
apply (rename_tac a b)
paulson@18886
   416
apply (induct_tac "a")
paulson@18886
   417
apply auto
paulson@18886
   418
done
paulson@18886
   419
paulson@37811
   420
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
paulson@18886
   421
apply (induct_tac "evs")
paulson@18886
   422
apply simp
blanchet@55417
   423
apply (rename_tac a b)
paulson@18886
   424
apply (induct_tac "a")
paulson@18886
   425
apply auto
paulson@18886
   426
done
paulson@18886
   427
paulson@37811
   428
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
paulson@18886
   429
apply (induct_tac "evs")
paulson@18886
   430
apply simp
blanchet@55417
   431
apply (rename_tac a b)
paulson@18886
   432
apply (induct_tac "a")
paulson@18886
   433
apply auto
paulson@18886
   434
done
paulson@18886
   435
paulson@18886
   436
lemma used_evs_rev: "used evs = used (rev evs)"
paulson@18886
   437
apply (induct_tac "evs")
paulson@18886
   438
apply simp
blanchet@55417
   439
apply (rename_tac a b)
paulson@18886
   440
apply (induct_tac "a")
paulson@18886
   441
apply (simp add: used_Says_rev)
paulson@18886
   442
apply (simp add: used_Gets_rev)
paulson@18886
   443
apply (simp add: used_Notes_rev)
paulson@18886
   444
done
paulson@18886
   445
paulson@18886
   446
lemma used_takeWhile_used [rule_format]: 
paulson@18886
   447
      "x : used (takeWhile P X) --> x : used X"
paulson@18886
   448
apply (induct_tac "X")
paulson@18886
   449
apply simp
blanchet@55417
   450
apply (rename_tac a b)
paulson@18886
   451
apply (induct_tac "a")
paulson@18886
   452
apply (simp_all add: used_Nil)
paulson@18886
   453
apply (blast dest!: initState_into_used)+
paulson@18886
   454
done
paulson@18886
   455
paulson@18886
   456
lemma set_evs_rev: "set evs = set (rev evs)"
paulson@37811
   457
by auto
paulson@18886
   458
paulson@18886
   459
lemma takeWhile_void [rule_format]:
paulson@18886
   460
      "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
paulson@37811
   461
by auto
paulson@18886
   462
paulson@18886
   463
wenzelm@61830
   464
subsection\<open>Regularity Lemmas\<close>
wenzelm@61830
   465
text\<open>These concern the form of items passed in messages\<close>
paulson@14182
   466
wenzelm@61830
   467
text\<open>Describes the form of all components sent by Kas\<close>
paulson@14182
   468
lemma Says_Kas_message_form:
paulson@18886
   469
     "\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
paulson@14207
   470
           \<in> set evs;
paulson@18886
   471
         evs \<in> kerbIV \<rbrakk> \<Longrightarrow>  
paulson@18886
   472
  K = shrK A  & Peer = Tgs &
paulson@18886
   473
  authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys & 
paulson@18886
   474
  authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>) &
paulson@18886
   475
  Key authK \<notin> used(before 
paulson@18886
   476
           Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
paulson@18886
   477
                   on evs) &
paulson@18886
   478
  Ta = CT (before 
paulson@18886
   479
           Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
paulson@18886
   480
           on evs)"
paulson@18886
   481
apply (unfold before_def)
paulson@14182
   482
apply (erule rev_mp)
paulson@18886
   483
apply (erule kerbIV.induct)
paulson@18886
   484
apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast)
wenzelm@61830
   485
txt\<open>K2\<close>
paulson@18886
   486
apply (simp (no_asm) add: takeWhile_tail)
paulson@18886
   487
apply (rule conjI)
paulson@32366
   488
apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev)
paulson@18886
   489
apply blast+
paulson@14182
   490
done
paulson@14182
   491
paulson@18886
   492
paulson@18886
   493
paulson@14207
   494
(*This lemma is essential for proving Says_Tgs_message_form:
paulson@14207
   495
paulson@18886
   496
  the session key authK
paulson@14182
   497
  supplied by Kas in the authentication ticket
paulson@14182
   498
  cannot be a long-term key!
paulson@14182
   499
paulson@18886
   500
  Generalised to any session keys (both authK and servK).
paulson@14182
   501
*)
paulson@14182
   502
lemma SesKey_is_session_key:
paulson@18886
   503
     "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
paulson@14207
   504
            \<in> parts (spies evs); Tgs_B \<notin> bad;
paulson@18886
   505
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   506
      \<Longrightarrow> SesKey \<notin> range shrK"
paulson@14182
   507
apply (erule rev_mp)
paulson@18886
   508
apply (erule kerbIV.induct)
paulson@14207
   509
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14182
   510
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
paulson@14182
   511
done
paulson@14182
   512
paulson@18886
   513
lemma authTicket_authentic:
paulson@18886
   514
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
paulson@14207
   515
           \<in> parts (spies evs);
paulson@18886
   516
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   517
      \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   518
                 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@14182
   519
            \<in> set evs"
paulson@14182
   520
apply (erule rev_mp)
paulson@18886
   521
apply (erule kerbIV.induct)
paulson@14207
   522
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   523
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   524
txt\<open>Fake, K4\<close>
paulson@14182
   525
apply (blast+)
paulson@14182
   526
done
paulson@14182
   527
paulson@18886
   528
lemma authTicket_crypt_authK:
paulson@18886
   529
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
paulson@14207
   530
           \<in> parts (spies evs);
paulson@18886
   531
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   532
      \<Longrightarrow> authK \<in> authKeys evs"
paulson@18886
   533
apply (frule authTicket_authentic, assumption)
paulson@18886
   534
apply (simp (no_asm) add: authKeys_def)
paulson@14182
   535
apply blast
paulson@14182
   536
done
paulson@14182
   537
wenzelm@61830
   538
text\<open>Describes the form of servK, servTicket and authK sent by Tgs\<close>
paulson@14182
   539
lemma Says_Tgs_message_form:
paulson@18886
   540
     "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14207
   541
           \<in> set evs;
paulson@18886
   542
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   543
  \<Longrightarrow> B \<noteq> Tgs & 
paulson@18886
   544
      authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
paulson@18886
   545
      servK \<notin> range shrK & servK \<notin> authKeys evs & servK \<in> symKeys &
paulson@18886
   546
      servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>) &
paulson@18886
   547
      Key servK \<notin> used (before
paulson@18886
   548
        Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   549
                        on evs) &
paulson@18886
   550
      Ts = CT(before 
paulson@18886
   551
        Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   552
              on evs) "
paulson@18886
   553
apply (unfold before_def)
paulson@14182
   554
apply (erule rev_mp)
paulson@18886
   555
apply (erule kerbIV.induct)
paulson@18886
   556
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast)
wenzelm@61830
   557
txt\<open>We need this simplification only for Message 4\<close>
paulson@18886
   558
apply (simp (no_asm) add: takeWhile_tail)
paulson@18886
   559
apply auto
wenzelm@61830
   560
txt\<open>Five subcases of Message 4\<close>
paulson@14182
   561
apply (blast dest!: SesKey_is_session_key)
paulson@18886
   562
apply (blast dest: authTicket_crypt_authK)
paulson@18886
   563
apply (blast dest!: authKeys_used Says_Kas_message_form)
wenzelm@61830
   564
txt\<open>subcase: used before\<close>
paulson@32366
   565
apply (metis used_evs_rev used_takeWhile_used)
wenzelm@61830
   566
txt\<open>subcase: CT before\<close>
paulson@32366
   567
apply (metis length_rev set_evs_rev takeWhile_void)
paulson@18886
   568
done
paulson@18886
   569
paulson@18886
   570
lemma authTicket_form:
paulson@18886
   571
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>
paulson@18886
   572
           \<in> parts (spies evs);
paulson@18886
   573
         A \<notin> bad;
paulson@18886
   574
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   575
    \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
paulson@18886
   576
        authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>"
paulson@18886
   577
apply (erule rev_mp)
paulson@18886
   578
apply (erule kerbIV.induct)
paulson@18886
   579
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   580
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
paulson@18886
   581
apply (blast+)
paulson@14182
   582
done
paulson@14182
   583
wenzelm@61830
   584
text\<open>This form holds also over an authTicket, but is not needed below.\<close>
paulson@18886
   585
lemma servTicket_form:
paulson@18886
   586
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>
paulson@18886
   587
              \<in> parts (spies evs);
paulson@18886
   588
            Key authK \<notin> analz (spies evs);
paulson@18886
   589
            evs \<in> kerbIV \<rbrakk>
paulson@18886
   590
         \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys & 
paulson@18886
   591
    (\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)"
paulson@18886
   592
apply (erule rev_mp)
paulson@18886
   593
apply (erule rev_mp)
paulson@18886
   594
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
   595
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   596
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
paulson@18886
   597
done
paulson@18886
   598
wenzelm@61830
   599
text\<open>Essentially the same as \<open>authTicket_form\<close>\<close>
paulson@18886
   600
lemma Says_kas_message_form:
paulson@18886
   601
     "\<lbrakk> Says Kas' A (Crypt (shrK A)
paulson@18886
   602
              \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
paulson@18886
   603
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   604
      \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys & 
paulson@18886
   605
          authTicket =
paulson@18886
   606
                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
paulson@18886
   607
          | authTicket \<in> analz (spies evs)"
paulson@18886
   608
by (blast dest: analz_shrK_Decrypt authTicket_form
paulson@18886
   609
                Says_imp_spies [THEN analz.Inj])
paulson@18886
   610
paulson@18886
   611
lemma Says_tgs_message_form:
paulson@18886
   612
 "\<lbrakk> Says Tgs' A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
paulson@18886
   613
       \<in> set evs;  authK \<in> symKeys;
paulson@18886
   614
     evs \<in> kerbIV \<rbrakk>
paulson@18886
   615
  \<Longrightarrow> servK \<notin> range shrK &
paulson@18886
   616
      (\<exists>A. servTicket =
wenzelm@32960
   617
              Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
paulson@18886
   618
       | servTicket \<in> analz (spies evs)"
paulson@37811
   619
by (metis Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Decrypt analz.Snd invKey_K servTicket_form)
paulson@18886
   620
paulson@18886
   621
wenzelm@61830
   622
subsection\<open>Authenticity theorems: confirm origin of sensitive messages\<close>
paulson@18886
   623
paulson@18886
   624
lemma authK_authentic:
paulson@18886
   625
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>
paulson@14207
   626
           \<in> parts (spies evs);
paulson@18886
   627
         A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
   628
      \<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
paulson@14182
   629
            \<in> set evs"
paulson@14182
   630
apply (erule rev_mp)
paulson@18886
   631
apply (erule kerbIV.induct)
paulson@14207
   632
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   633
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   634
txt\<open>Fake\<close>
paulson@14182
   635
apply blast
wenzelm@61830
   636
txt\<open>K4\<close>
paulson@18886
   637
apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
paulson@14182
   638
done
paulson@14182
   639
wenzelm@61830
   640
text\<open>If a certain encrypted message appears then it originated with Tgs\<close>
paulson@18886
   641
lemma servK_authentic:
paulson@18886
   642
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14207
   643
           \<in> parts (spies evs);
paulson@18886
   644
         Key authK \<notin> analz (spies evs);
paulson@18886
   645
         authK \<notin> range shrK;
paulson@18886
   646
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   647
 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
   648
       \<in> set evs"
paulson@14182
   649
apply (erule rev_mp)
paulson@14182
   650
apply (erule rev_mp)
paulson@18886
   651
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14207
   652
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   653
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   654
txt\<open>Fake\<close>
paulson@14182
   655
apply blast
wenzelm@61830
   656
txt\<open>K2\<close>
paulson@14182
   657
apply blast
wenzelm@61830
   658
txt\<open>K4\<close>
paulson@14182
   659
apply auto
paulson@14182
   660
done
paulson@14182
   661
paulson@18886
   662
lemma servK_authentic_bis:
paulson@18886
   663
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14207
   664
           \<in> parts (spies evs);
paulson@18886
   665
         Key authK \<notin> analz (spies evs);
paulson@18886
   666
         B \<noteq> Tgs;
paulson@18886
   667
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   668
 \<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   669
       \<in> set evs"
paulson@14182
   670
apply (erule rev_mp)
paulson@18886
   671
apply (erule rev_mp)
paulson@18886
   672
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14207
   673
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   674
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   675
txt\<open>Fake\<close>
paulson@18886
   676
apply blast
wenzelm@61830
   677
txt\<open>K4\<close>
paulson@18886
   678
apply blast
paulson@14182
   679
done
paulson@14182
   680
wenzelm@61830
   681
text\<open>Authenticity of servK for B\<close>
paulson@18886
   682
lemma servTicket_authentic_Tgs:
paulson@18886
   683
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   684
           \<in> parts (spies evs); B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   685
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   686
 \<Longrightarrow> \<exists>authK.
paulson@18886
   687
       Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   688
                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
paulson@18886
   689
       \<in> set evs"
paulson@14182
   690
apply (erule rev_mp)
paulson@14182
   691
apply (erule rev_mp)
paulson@18886
   692
apply (erule kerbIV.induct)
paulson@18886
   693
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   694
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
paulson@18886
   695
apply blast+
paulson@18886
   696
done
paulson@18886
   697
wenzelm@61830
   698
text\<open>Anticipated here from next subsection\<close>
paulson@18886
   699
lemma K4_imp_K2:
paulson@18886
   700
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   701
      \<in> set evs;  evs \<in> kerbIV\<rbrakk>
paulson@18886
   702
   \<Longrightarrow> \<exists>Ta. Says Kas A
paulson@18886
   703
        (Crypt (shrK A)
paulson@18886
   704
         \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   705
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   706
        \<in> set evs"
paulson@18886
   707
apply (erule rev_mp)
paulson@18886
   708
apply (erule kerbIV.induct)
paulson@14207
   709
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   710
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
paulson@18886
   711
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
paulson@18886
   712
done
paulson@18886
   713
wenzelm@61830
   714
text\<open>Anticipated here from next subsection\<close>
paulson@18886
   715
lemma u_K4_imp_K2:
paulson@18886
   716
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   717
      \<in> set evs; evs \<in> kerbIV\<rbrakk>
paulson@18886
   718
   \<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   719
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   720
             \<in> set evs
paulson@18886
   721
          & servKlife + Ts <= authKlife + Ta)"
paulson@18886
   722
apply (erule rev_mp)
paulson@18886
   723
apply (erule kerbIV.induct)
paulson@18886
   724
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   725
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
paulson@18886
   726
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
paulson@14182
   727
done
paulson@14182
   728
paulson@18886
   729
lemma servTicket_authentic_Kas:
paulson@18886
   730
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   731
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   732
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   733
  \<Longrightarrow> \<exists>authK Ta.
paulson@18886
   734
       Says Kas A
paulson@18886
   735
         (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   736
            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   737
        \<in> set evs"
paulson@37811
   738
by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
paulson@18886
   739
paulson@18886
   740
lemma u_servTicket_authentic_Kas:
paulson@18886
   741
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   742
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   743
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   744
  \<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   745
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   746
             \<in> set evs
paulson@18886
   747
           & servKlife + Ts <= authKlife + Ta"
paulson@37811
   748
by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
paulson@18886
   749
paulson@18886
   750
lemma servTicket_authentic:
paulson@18886
   751
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   752
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   753
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   754
 \<Longrightarrow> \<exists>Ta authK.
paulson@18886
   755
     Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   756
                   Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   757
       \<in> set evs
paulson@18886
   758
     & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   759
                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
paulson@18886
   760
       \<in> set evs"
paulson@37811
   761
by (blast dest: servTicket_authentic_Tgs K4_imp_K2)
paulson@18886
   762
paulson@18886
   763
lemma u_servTicket_authentic:
paulson@18886
   764
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   765
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   766
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   767
 \<Longrightarrow> \<exists>Ta authK.
paulson@18886
   768
     (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
   769
                   Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
   770
       \<in> set evs
paulson@18886
   771
     & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   772
                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
paulson@18886
   773
       \<in> set evs
paulson@18886
   774
     & servKlife + Ts <= authKlife + Ta)"
paulson@37811
   775
by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
paulson@18886
   776
paulson@18886
   777
lemma u_NotexpiredSK_NotexpiredAK:
paulson@18886
   778
     "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
paulson@18886
   779
      \<Longrightarrow> \<not> expiredAK Ta evs"
wenzelm@33304
   780
  by (metis le_less_trans)
paulson@14207
   781
paulson@14182
   782
wenzelm@61830
   783
subsection\<open>Reliability: friendly agents send something if something else happened\<close>
paulson@18886
   784
paulson@18886
   785
lemma K3_imp_K2:
paulson@18886
   786
     "\<lbrakk> Says A Tgs
paulson@18886
   787
             \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
paulson@18886
   788
           \<in> set evs;
paulson@18886
   789
         A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
   790
      \<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A)
paulson@18886
   791
                      \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
paulson@18886
   792
                   \<in> set evs"
paulson@18886
   793
apply (erule rev_mp)
paulson@18886
   794
apply (erule kerbIV.induct)
paulson@18886
   795
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   796
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
paulson@18886
   797
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN authK_authentic])
paulson@14207
   798
done
paulson@14182
   799
wenzelm@61830
   800
text\<open>Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.\<close>
paulson@18886
   801
lemma Key_unique_SesKey:
paulson@18886
   802
     "\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T, Ticket\<rbrace>
paulson@14207
   803
           \<in> parts (spies evs);
paulson@18886
   804
         Crypt K' \<lbrace>Key SesKey,  Agent B', T', Ticket'\<rbrace>
paulson@14207
   805
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
paulson@18886
   806
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   807
      \<Longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket'"
paulson@14182
   808
apply (erule rev_mp)
paulson@14182
   809
apply (erule rev_mp)
paulson@14182
   810
apply (erule rev_mp)
paulson@18886
   811
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14207
   812
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   813
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   814
txt\<open>Fake, K2, K4\<close>
paulson@14182
   815
apply (blast+)
paulson@14182
   816
done
paulson@14182
   817
paulson@18886
   818
lemma Tgs_authenticates_A:
paulson@18886
   819
  "\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 
paulson@18886
   820
      Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
paulson@14207
   821
           \<in> parts (spies evs);
paulson@18886
   822
      Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
   823
 \<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
paulson@18886
   824
          Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
paulson@18886
   825
          Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs"  
paulson@18886
   826
apply (drule authTicket_authentic, assumption, rotate_tac 4)
paulson@18886
   827
apply (erule rev_mp, erule rev_mp, erule rev_mp)
paulson@18886
   828
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
   829
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   830
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   831
apply (simp_all (no_asm_simp) add: all_conj_distrib)
wenzelm@61830
   832
txt\<open>Fake\<close>
paulson@18886
   833
apply blast
wenzelm@61830
   834
txt\<open>K2\<close>
paulson@18886
   835
apply (force dest!: Crypt_imp_keysFor)
wenzelm@61830
   836
txt\<open>K3\<close>
paulson@18886
   837
apply (blast dest: Key_unique_SesKey)
wenzelm@61830
   838
txt\<open>K5\<close>
paulson@32366
   839
apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst 
paulson@32366
   840
             Says_imp_knows_Spy [THEN parts.Inj])
paulson@18886
   841
done
paulson@18886
   842
paulson@18886
   843
lemma Says_K5:
paulson@18886
   844
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
   845
         Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   846
                                     servTicket\<rbrace>) \<in> set evs;
paulson@18886
   847
         Key servK \<notin> analz (spies evs);
paulson@18886
   848
         A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
   849
 \<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
paulson@14182
   850
apply (erule rev_mp)
paulson@14182
   851
apply (erule rev_mp)
paulson@14182
   852
apply (erule rev_mp)
paulson@18886
   853
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
   854
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   855
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   856
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
   857
apply blast
wenzelm@61830
   858
txt\<open>K3\<close>
paulson@18886
   859
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
wenzelm@61830
   860
txt\<open>K4\<close>
paulson@18886
   861
apply (force dest!: Crypt_imp_keysFor)
wenzelm@61830
   862
txt\<open>K5\<close>
paulson@18886
   863
apply (blast dest: Key_unique_SesKey)
paulson@18886
   864
done
paulson@18886
   865
wenzelm@61830
   866
text\<open>Anticipated here from next subsection\<close>
paulson@18886
   867
lemma unique_CryptKey:
paulson@18886
   868
     "\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
paulson@18886
   869
           \<in> parts (spies evs);
paulson@18886
   870
         Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
paulson@18886
   871
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
paulson@18886
   872
         evs \<in> kerbIV \<rbrakk>
paulson@18886
   873
      \<Longrightarrow> A=A' & B=B' & T=T'"
paulson@18886
   874
apply (erule rev_mp)
paulson@18886
   875
apply (erule rev_mp)
paulson@18886
   876
apply (erule rev_mp)
paulson@18886
   877
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14207
   878
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   879
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   880
txt\<open>Fake, K2, K4\<close>
paulson@14182
   881
apply (blast+)
paulson@14182
   882
done
paulson@14182
   883
paulson@18886
   884
lemma Says_K6:
paulson@18886
   885
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
   886
         Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
   887
                                     servTicket\<rbrace>) \<in> set evs;
paulson@18886
   888
         Key servK \<notin> analz (spies evs);
paulson@18886
   889
         A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
   890
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@18886
   891
apply (erule rev_mp)
paulson@18886
   892
apply (erule rev_mp)
paulson@18886
   893
apply (erule rev_mp)
paulson@18886
   894
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
   895
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   896
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   897
apply (simp_all (no_asm_simp))
paulson@18886
   898
apply blast
paulson@32366
   899
apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used)
paulson@32366
   900
apply (clarify)
paulson@32366
   901
apply (frule Says_Tgs_message_form, assumption)
paulson@32366
   902
apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj] 
paulson@32366
   903
             unique_CryptKey) 
paulson@18886
   904
done
paulson@18886
   905
wenzelm@61830
   906
text\<open>Needs a unicity theorem, hence moved here\<close>
paulson@18886
   907
lemma servK_authentic_ter:
paulson@18886
   908
 "\<lbrakk> Says Kas A
paulson@18886
   909
    (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
paulson@18886
   910
     Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
   911
       \<in> parts (spies evs);
paulson@18886
   912
     Key authK \<notin> analz (spies evs);
paulson@18886
   913
     evs \<in> kerbIV \<rbrakk>
paulson@18886
   914
 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
   915
       \<in> set evs"
paulson@18886
   916
apply (frule Says_Kas_message_form, assumption)
paulson@18886
   917
apply (erule rev_mp)
paulson@18886
   918
apply (erule rev_mp)
paulson@18886
   919
apply (erule rev_mp)
paulson@18886
   920
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
   921
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@18886
   922
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
wenzelm@61830
   923
txt\<open>K2\<close>
paulson@18886
   924
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
wenzelm@61830
   925
txt\<open>K4 remain\<close>
paulson@37811
   926
apply (blast dest!: unique_CryptKey)
paulson@18886
   927
done
paulson@18886
   928
paulson@18886
   929
wenzelm@61830
   930
subsection\<open>Unicity Theorems\<close>
paulson@18886
   931
wenzelm@61830
   932
text\<open>The session key, if secure, uniquely identifies the Ticket
paulson@18886
   933
   whether authTicket or servTicket. As a matter of fact, one can read
wenzelm@61830
   934
   also Tgs in the place of B.\<close>
paulson@18886
   935
paulson@14182
   936
paulson@14182
   937
(*
paulson@14182
   938
  At reception of any message mentioning A, Kas associates shrK A with
paulson@18886
   939
  a new authK. Realistic, as the user gets a new authK at each login.
paulson@18886
   940
  Similarly, at reception of any message mentioning an authK
paulson@14207
   941
  (a legitimate user could make several requests to Tgs - by K3), Tgs
paulson@18886
   942
  associates it with a new servK.
paulson@14182
   943
paulson@14182
   944
  Therefore, a goal like
paulson@14182
   945
paulson@18886
   946
   "evs \<in> kerbIV
paulson@18886
   947
     \<Longrightarrow> Key Kc \<notin> analz (spies evs) \<longrightarrow>
paulson@14207
   948
           (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
paulson@18886
   949
            Crypt Kc \<lbrace>Key K, Agent B, T, Ticket\<rbrace>
paulson@18886
   950
             \<in> parts (spies evs) \<longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket')"
paulson@14182
   951
paulson@14182
   952
  would fail on the K2 and K4 cases.
paulson@14182
   953
*)
paulson@14182
   954
paulson@18886
   955
lemma unique_authKeys:
paulson@18886
   956
     "\<lbrakk> Says Kas A
paulson@18886
   957
              (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs;
paulson@14207
   958
         Says Kas A'
paulson@18886
   959
              (Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs;
paulson@18886
   960
         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & Ka=Ka' & Ta=Ta' & X=X'"
paulson@14182
   961
apply (erule rev_mp)
paulson@14182
   962
apply (erule rev_mp)
paulson@18886
   963
apply (erule kerbIV.induct)
paulson@14207
   964
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   965
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   966
txt\<open>K2\<close>
paulson@14182
   967
apply blast
paulson@14182
   968
done
paulson@14182
   969
wenzelm@61830
   970
text\<open>servK uniquely identifies the message from Tgs\<close>
paulson@18886
   971
lemma unique_servKeys:
paulson@18886
   972
     "\<lbrakk> Says Tgs A
paulson@18886
   973
              (Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs;
paulson@14207
   974
         Says Tgs A'
paulson@18886
   975
              (Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs;
paulson@18886
   976
         evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A=A' & B=B' & K=K' & Ts=Ts' & X=X'"
paulson@14182
   977
apply (erule rev_mp)
paulson@14182
   978
apply (erule rev_mp)
paulson@18886
   979
apply (erule kerbIV.induct)
paulson@14207
   980
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
   981
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
   982
txt\<open>K4\<close>
paulson@14182
   983
apply blast
paulson@14182
   984
done
paulson@14182
   985
wenzelm@61830
   986
text\<open>Revised unicity theorems\<close>
paulson@14182
   987
paulson@18886
   988
lemma Kas_Unique:
paulson@18886
   989
     "\<lbrakk> Says Kas A
paulson@18886
   990
              (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
paulson@18886
   991
        evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 
paulson@18886
   992
   Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>)) 
paulson@18886
   993
   on evs"
paulson@18886
   994
apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
paulson@18886
   995
apply blast
paulson@18886
   996
done
paulson@14182
   997
paulson@18886
   998
lemma Tgs_Unique:
paulson@18886
   999
     "\<lbrakk> Says Tgs A
paulson@18886
  1000
              (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs;
paulson@18886
  1001
        evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 
paulson@18886
  1002
  Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)) 
paulson@18886
  1003
  on evs"
paulson@18886
  1004
apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
paulson@18886
  1005
apply blast
paulson@18886
  1006
done
paulson@14182
  1007
paulson@18886
  1008
wenzelm@61830
  1009
subsection\<open>Lemmas About the Predicate @{term AKcryptSK}\<close>
paulson@18886
  1010
paulson@18886
  1011
lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
paulson@18886
  1012
by (simp add: AKcryptSK_def)
paulson@18886
  1013
paulson@18886
  1014
lemma AKcryptSKI:
paulson@18886
  1015
 "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
paulson@18886
  1016
     evs \<in> kerbIV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
paulson@18886
  1017
apply (unfold AKcryptSK_def)
paulson@14182
  1018
apply (blast dest: Says_Tgs_message_form)
paulson@14182
  1019
done
paulson@14182
  1020
paulson@18886
  1021
lemma AKcryptSK_Says [simp]:
paulson@18886
  1022
   "AKcryptSK authK servK (Says S A X # evs) =
paulson@14207
  1023
     (Tgs = S &
paulson@18886
  1024
      (\<exists>B Ts. X = Crypt authK
paulson@18886
  1025
                \<lbrace>Key servK, Agent B, Number Ts,
paulson@18886
  1026
                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
paulson@18886
  1027
     | AKcryptSK authK servK evs)"
paulson@37811
  1028
by (auto simp add: AKcryptSK_def)
paulson@37811
  1029
paulson@14182
  1030
paulson@18886
  1031
(*A fresh authK cannot be associated with any other
paulson@14182
  1032
  (with respect to a given trace). *)
paulson@18886
  1033
lemma Auth_fresh_not_AKcryptSK:
paulson@18886
  1034
     "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1035
      \<Longrightarrow> \<not> AKcryptSK authK servK evs"
paulson@18886
  1036
apply (unfold AKcryptSK_def)
paulson@14182
  1037
apply (erule rev_mp)
paulson@18886
  1038
apply (erule kerbIV.induct)
paulson@14207
  1039
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14182
  1040
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
paulson@14182
  1041
done
paulson@14182
  1042
paulson@18886
  1043
(*A fresh servK cannot be associated with any other
paulson@14182
  1044
  (with respect to a given trace). *)
paulson@18886
  1045
lemma Serv_fresh_not_AKcryptSK:
paulson@18886
  1046
 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
paulson@37811
  1047
by (unfold AKcryptSK_def, blast)
paulson@14182
  1048
paulson@18886
  1049
lemma authK_not_AKcryptSK:
paulson@18886
  1050
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
paulson@18886
  1051
           \<in> parts (spies evs);  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1052
      \<Longrightarrow> \<not> AKcryptSK K authK evs"
paulson@14182
  1053
apply (erule rev_mp)
paulson@18886
  1054
apply (erule kerbIV.induct)
paulson@14207
  1055
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
  1056
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
wenzelm@61830
  1057
txt\<open>Fake\<close>
paulson@14207
  1058
apply blast
wenzelm@61830
  1059
txt\<open>K2: by freshness\<close>
paulson@18886
  1060
apply (simp add: AKcryptSK_def)
wenzelm@61830
  1061
txt\<open>K4\<close>
paulson@14182
  1062
apply (blast+)
paulson@14182
  1063
done
paulson@14182
  1064
wenzelm@61830
  1065
text\<open>A secure serverkey cannot have been used to encrypt others\<close>
paulson@18886
  1066
lemma servK_not_AKcryptSK:
paulson@18886
  1067
 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs);
paulson@14207
  1068
     Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
paulson@18886
  1069
     B \<noteq> Tgs;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1070
  \<Longrightarrow> \<not> AKcryptSK SK K evs"
paulson@14182
  1071
apply (erule rev_mp)
paulson@14182
  1072
apply (erule rev_mp)
paulson@18886
  1073
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14207
  1074
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14182
  1075
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
wenzelm@61830
  1076
txt\<open>K4\<close>
paulson@32366
  1077
apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey)
paulson@14182
  1078
done
paulson@14182
  1079
wenzelm@61830
  1080
text\<open>Long term keys are not issued as servKeys\<close>
paulson@18886
  1081
lemma shrK_not_AKcryptSK:
paulson@18886
  1082
     "evs \<in> kerbIV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
paulson@18886
  1083
apply (unfold AKcryptSK_def)
paulson@18886
  1084
apply (erule kerbIV.induct)
paulson@14207
  1085
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14207
  1086
apply (frule_tac [5] K3_msg_in_parts_spies, auto)
paulson@14182
  1087
done
paulson@14182
  1088
wenzelm@61830
  1089
text\<open>The Tgs message associates servK with authK and therefore not with any
wenzelm@61830
  1090
  other key authK.\<close>
paulson@18886
  1091
lemma Says_Tgs_AKcryptSK:
paulson@18886
  1092
     "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>)
paulson@14207
  1093
           \<in> set evs;
paulson@18886
  1094
         authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1095
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs"
paulson@18886
  1096
apply (unfold AKcryptSK_def)
paulson@18886
  1097
apply (blast dest: unique_servKeys)
paulson@14182
  1098
done
paulson@14182
  1099
wenzelm@61830
  1100
text\<open>Equivalently\<close>
paulson@18886
  1101
lemma not_different_AKcryptSK:
paulson@18886
  1102
     "\<lbrakk> AKcryptSK authK servK evs;
paulson@18886
  1103
        authK' \<noteq> authK;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1104
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
paulson@18886
  1105
apply (simp add: AKcryptSK_def)
paulson@18886
  1106
apply (blast dest: unique_servKeys Says_Tgs_message_form)
paulson@18886
  1107
done
paulson@18886
  1108
paulson@18886
  1109
lemma AKcryptSK_not_AKcryptSK:
paulson@18886
  1110
     "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1111
      \<Longrightarrow> \<not> AKcryptSK servK K evs"
paulson@14182
  1112
apply (erule rev_mp)
paulson@18886
  1113
apply (erule kerbIV.induct)
paulson@14207
  1114
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@32366
  1115
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
paulson@32366
  1116
apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK 
paulson@32366
  1117
             authKeys_used authTicket_crypt_authK parts.Fst parts.Inj)
paulson@14182
  1118
done
paulson@14182
  1119
wenzelm@61830
  1120
text\<open>The only session keys that can be found with the help of session keys are
wenzelm@61830
  1121
  those sent by Tgs in step K4.\<close>
paulson@14182
  1122
wenzelm@61830
  1123
text\<open>We take some pains to express the property
wenzelm@61830
  1124
  as a logical equivalence so that the simplifier can apply it.\<close>
paulson@14182
  1125
lemma Key_analz_image_Key_lemma:
paulson@18886
  1126
     "P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
paulson@18886
  1127
      \<Longrightarrow>
paulson@18886
  1128
      P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
paulson@14182
  1129
by (blast intro: analz_mono [THEN subsetD])
paulson@14182
  1130
paulson@14182
  1131
paulson@18886
  1132
lemma AKcryptSK_analz_insert:
paulson@18886
  1133
     "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1134
      \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
paulson@18886
  1135
apply (simp add: AKcryptSK_def, clarify)
paulson@14182
  1136
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
paulson@14182
  1137
done
paulson@14182
  1138
paulson@18886
  1139
lemma authKeys_are_not_AKcryptSK:
paulson@18886
  1140
     "\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1141
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
paulson@18886
  1142
apply (simp add: authKeys_def AKcryptSK_def)
paulson@18886
  1143
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
paulson@14182
  1144
done
paulson@14182
  1145
paulson@18886
  1146
lemma not_authKeys_not_AKcryptSK:
paulson@18886
  1147
     "\<lbrakk> K \<notin> authKeys evs;
paulson@18886
  1148
         K \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1149
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
paulson@18886
  1150
apply (simp add: AKcryptSK_def)
paulson@14182
  1151
apply (blast dest: Says_Tgs_message_form)
paulson@14182
  1152
done
paulson@14182
  1153
paulson@14182
  1154
wenzelm@61830
  1155
subsection\<open>Secrecy Theorems\<close>
paulson@14182
  1156
wenzelm@61830
  1157
text\<open>For the Oops2 case of the next theorem\<close>
paulson@18886
  1158
lemma Oops2_not_AKcryptSK:
paulson@18886
  1159
     "\<lbrakk> evs \<in> kerbIV;
paulson@18886
  1160
         Says Tgs A (Crypt authK
paulson@18886
  1161
                     \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
  1162
           \<in> set evs \<rbrakk>
paulson@18886
  1163
      \<Longrightarrow> \<not> AKcryptSK servK SK evs"
paulson@37811
  1164
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
paulson@18886
  1165
   
wenzelm@61830
  1166
text\<open>Big simplification law for keys SK that are not crypted by keys in KK
paulson@14182
  1167
 It helps prove three, otherwise hard, facts about keys. These facts are
paulson@14182
  1168
 exploited as simplification laws for analz, and also "limit the damage"
paulson@14182
  1169
 in case of loss of a key to the spy. See ESORICS98.
wenzelm@61830
  1170
 [simplified by LCP]\<close>
paulson@14182
  1171
lemma Key_analz_image_Key [rule_format (no_asm)]:
paulson@18886
  1172
     "evs \<in> kerbIV \<Longrightarrow>
paulson@18886
  1173
      (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
paulson@18886
  1174
       (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
paulson@14207
  1175
       (Key SK \<in> analz (Key`KK Un (spies evs))) =
paulson@14207
  1176
       (SK \<in> KK | Key SK \<in> analz (spies evs)))"
paulson@18886
  1177
apply (erule kerbIV.induct)
paulson@14182
  1178
apply (frule_tac [10] Oops_range_spies2)
paulson@14182
  1179
apply (frule_tac [9] Oops_range_spies1)
paulson@14182
  1180
apply (frule_tac [7] Says_tgs_message_form)
paulson@14182
  1181
apply (frule_tac [5] Says_kas_message_form)
paulson@14182
  1182
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
wenzelm@61830
  1183
txt\<open>Case-splits for Oops1 and message 5: the negated case simplifies using
wenzelm@61830
  1184
 the induction hypothesis\<close>
paulson@18886
  1185
apply (case_tac [11] "AKcryptSK authK SK evsO1")
paulson@18886
  1186
apply (case_tac [8] "AKcryptSK servK SK evs5")
paulson@14207
  1187
apply (simp_all del: image_insert
paulson@18886
  1188
        add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
paulson@18886
  1189
             Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
paulson@18886
  1190
       Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
wenzelm@61830
  1191
txt\<open>Fake\<close> 
paulson@14945
  1192
apply spy_analz
wenzelm@61830
  1193
txt\<open>K2\<close>
paulson@14207
  1194
apply blast 
wenzelm@61830
  1195
txt\<open>K3\<close>
paulson@14207
  1196
apply blast 
wenzelm@61830
  1197
txt\<open>K4\<close>
paulson@18886
  1198
apply (blast dest!: authK_not_AKcryptSK)
wenzelm@61830
  1199
txt\<open>K5\<close>
paulson@18886
  1200
apply (case_tac "Key servK \<in> analz (spies evs5) ")
wenzelm@61830
  1201
txt\<open>If servK is compromised then the result follows directly...\<close>
paulson@14182
  1202
apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
wenzelm@61830
  1203
txt\<open>...therefore servK is uncompromised.\<close>
wenzelm@61830
  1204
txt\<open>The AKcryptSK servK SK evs5 case leads to a contradiction.\<close>
paulson@18886
  1205
apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
wenzelm@61830
  1206
txt\<open>Another K5 case\<close>
paulson@14207
  1207
apply blast 
wenzelm@61830
  1208
txt\<open>Oops1\<close>
paulson@14207
  1209
apply simp 
paulson@18886
  1210
apply (blast dest!: AKcryptSK_analz_insert)
paulson@14182
  1211
done
paulson@14182
  1212
wenzelm@61830
  1213
text\<open>First simplification law for analz: no session keys encrypt
wenzelm@61830
  1214
authentication keys or shared keys.\<close>
paulson@14182
  1215
lemma analz_insert_freshK1:
paulson@18886
  1216
     "\<lbrakk> evs \<in> kerbIV;  K \<in> authKeys evs Un range shrK;
paulson@18886
  1217
        SesKey \<notin> range shrK \<rbrakk>
paulson@18886
  1218
      \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
paulson@14182
  1219
          (K = SesKey | Key K \<in> analz (spies evs))"
paulson@18886
  1220
apply (frule authKeys_are_not_AKcryptSK, assumption)
paulson@14207
  1221
apply (simp del: image_insert
paulson@14182
  1222
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@14182
  1223
done
paulson@14182
  1224
paulson@14182
  1225
wenzelm@61830
  1226
text\<open>Second simplification law for analz: no service keys encrypt any other keys.\<close>
paulson@14182
  1227
lemma analz_insert_freshK2:
paulson@18886
  1228
     "\<lbrakk> evs \<in> kerbIV;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
paulson@18886
  1229
        K \<in> symKeys \<rbrakk>
paulson@18886
  1230
      \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
paulson@18886
  1231
          (K = servK | Key K \<in> analz (spies evs))"
paulson@18886
  1232
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
paulson@14207
  1233
apply (simp del: image_insert
paulson@14182
  1234
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@14182
  1235
done
paulson@14182
  1236
paulson@14182
  1237
wenzelm@61830
  1238
text\<open>Third simplification law for analz: only one authentication key encrypts a certain service key.\<close>
paulson@18886
  1239
paulson@14182
  1240
lemma analz_insert_freshK3:
paulson@18886
  1241
 "\<lbrakk> AKcryptSK authK servK evs;
paulson@18886
  1242
    authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1243
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
paulson@18886
  1244
                (servK = authK' | Key servK \<in> analz (spies evs))"
paulson@18886
  1245
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
paulson@14207
  1246
apply (simp del: image_insert
paulson@14182
  1247
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@14182
  1248
done
paulson@14182
  1249
paulson@18886
  1250
lemma analz_insert_freshK3_bis:
paulson@18886
  1251
 "\<lbrakk> Says Tgs A
paulson@18886
  1252
            (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
  1253
        \<in> set evs; 
paulson@18886
  1254
     authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1255
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
paulson@18886
  1256
                (servK = authK' | Key servK \<in> analz (spies evs))"
paulson@18886
  1257
apply (frule AKcryptSKI, assumption)
paulson@18886
  1258
apply (simp add: analz_insert_freshK3)
paulson@18886
  1259
done
paulson@14182
  1260
wenzelm@61830
  1261
text\<open>a weakness of the protocol\<close>
paulson@18886
  1262
lemma authK_compromises_servK:
paulson@18886
  1263
     "\<lbrakk> Says Tgs A
paulson@18886
  1264
              (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
  1265
           \<in> set evs;  authK \<in> symKeys;
paulson@18886
  1266
         Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk>
paulson@18886
  1267
      \<Longrightarrow> Key servK \<in> analz (spies evs)"
paulson@32366
  1268
  by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
paulson@14182
  1269
paulson@18886
  1270
lemma servK_notin_authKeysD:
paulson@18886
  1271
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
paulson@18886
  1272
                      Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
paulson@14182
  1273
           \<in> parts (spies evs);
paulson@18886
  1274
         Key servK \<notin> analz (spies evs);
paulson@18886
  1275
         B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1276
      \<Longrightarrow> servK \<notin> authKeys evs"
paulson@14182
  1277
apply (erule rev_mp)
paulson@14182
  1278
apply (erule rev_mp)
paulson@18886
  1279
apply (simp add: authKeys_def)
paulson@18886
  1280
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14182
  1281
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14182
  1282
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
paulson@14182
  1283
apply (blast+)
paulson@14182
  1284
done
paulson@14182
  1285
paulson@14182
  1286
wenzelm@61830
  1287
text\<open>If Spy sees the Authentication Key sent in msg K2, then
wenzelm@61830
  1288
    the Key has expired.\<close>
paulson@14182
  1289
lemma Confidentiality_Kas_lemma [rule_format]:
paulson@18886
  1290
     "\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1291
      \<Longrightarrow> Says Kas A
paulson@14182
  1292
               (Crypt (shrK A)
paulson@18886
  1293
                  \<lbrace>Key authK, Agent Tgs, Number Ta,
paulson@18886
  1294
          Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
paulson@18886
  1295
            \<in> set evs \<longrightarrow>
paulson@18886
  1296
          Key authK \<in> analz (spies evs) \<longrightarrow>
paulson@18886
  1297
          expiredAK Ta evs"
paulson@18886
  1298
apply (erule kerbIV.induct)
paulson@14182
  1299
apply (frule_tac [10] Oops_range_spies2)
paulson@14182
  1300
apply (frule_tac [9] Oops_range_spies1)
paulson@14182
  1301
apply (frule_tac [7] Says_tgs_message_form)
paulson@14182
  1302
apply (frule_tac [5] Says_kas_message_form)
paulson@14182
  1303
apply (safe del: impI conjI impCE)
paulson@14182
  1304
apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
wenzelm@61830
  1305
txt\<open>Fake\<close>
paulson@14182
  1306
apply spy_analz
wenzelm@61830
  1307
txt\<open>K2\<close>
paulson@14182
  1308
apply blast
wenzelm@61830
  1309
txt\<open>K4\<close>
paulson@14182
  1310
apply blast
wenzelm@61830
  1311
txt\<open>Level 8: K5\<close>
paulson@18886
  1312
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
wenzelm@61830
  1313
txt\<open>Oops1\<close>
paulson@18886
  1314
apply (blast dest!: unique_authKeys intro: less_SucI)
wenzelm@61830
  1315
txt\<open>Oops2\<close>
paulson@14182
  1316
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
paulson@14182
  1317
done
paulson@14182
  1318
paulson@14182
  1319
lemma Confidentiality_Kas:
paulson@18886
  1320
     "\<lbrakk> Says Kas A
paulson@18886
  1321
              (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
paulson@14182
  1322
           \<in> set evs;
paulson@18886
  1323
         \<not> expiredAK Ta evs;
paulson@18886
  1324
         A \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1325
      \<Longrightarrow> Key authK \<notin> analz (spies evs)"
paulson@14200
  1326
by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
paulson@14182
  1327
wenzelm@61830
  1328
text\<open>If Spy sees the Service Key sent in msg K4, then
wenzelm@61830
  1329
    the Key has expired.\<close>
paulson@14207
  1330
paulson@14182
  1331
lemma Confidentiality_lemma [rule_format]:
paulson@18886
  1332
     "\<lbrakk> Says Tgs A
wenzelm@32960
  1333
            (Crypt authK
wenzelm@32960
  1334
               \<lbrace>Key servK, Agent B, Number Ts,
wenzelm@32960
  1335
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
wenzelm@32960
  1336
           \<in> set evs;
wenzelm@32960
  1337
        Key authK \<notin> analz (spies evs);
paulson@18886
  1338
        servK \<in> symKeys;
wenzelm@32960
  1339
        A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1340
      \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
wenzelm@32960
  1341
          expiredSK Ts evs"
paulson@14182
  1342
apply (erule rev_mp)
paulson@14182
  1343
apply (erule rev_mp)
paulson@18886
  1344
apply (erule kerbIV.induct)
paulson@37811
  1345
apply (rule_tac [9] impI)+
wenzelm@61830
  1346
  \<comment>\<open>The Oops1 case is unusual: must simplify
paulson@14182
  1347
    @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
wenzelm@61830
  1348
   \<open>analz_mono_contra\<close> weaken it to
paulson@14207
  1349
   @{term "Authkey \<notin> analz (spies evs)"},
wenzelm@61830
  1350
  for we then conclude @{term "authK \<noteq> authKa"}.\<close>
paulson@14182
  1351
apply analz_mono_contra
paulson@14182
  1352
apply (frule_tac [10] Oops_range_spies2)
paulson@14182
  1353
apply (frule_tac [9] Oops_range_spies1)
paulson@14182
  1354
apply (frule_tac [7] Says_tgs_message_form)
paulson@14182
  1355
apply (frule_tac [5] Says_kas_message_form)
paulson@14182
  1356
apply (safe del: impI conjI impCE)
paulson@18886
  1357
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
wenzelm@61830
  1358
txt\<open>Fake\<close>
paulson@32366
  1359
     apply spy_analz
wenzelm@61830
  1360
txt\<open>K2\<close>
paulson@32366
  1361
    apply (blast intro: parts_insertI less_SucI)
wenzelm@61830
  1362
txt\<open>K4\<close>
paulson@32366
  1363
   apply (blast dest: authTicket_authentic Confidentiality_Kas)
wenzelm@61830
  1364
txt\<open>K5\<close>
paulson@32366
  1365
  apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2 
paulson@32366
  1366
             less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey)
wenzelm@61830
  1367
txt\<open>Oops1\<close> 
paulson@32366
  1368
 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
wenzelm@61830
  1369
txt\<open>Oops2\<close>
paulson@14182
  1370
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
paulson@14182
  1371
done
paulson@14182
  1372
paulson@14182
  1373
wenzelm@61830
  1374
text\<open>In the real world Tgs can't check wheter authK is secure!\<close>
paulson@18886
  1375
lemma Confidentiality_Tgs:
paulson@18886
  1376
     "\<lbrakk> Says Tgs A
paulson@18886
  1377
              (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
  1378
           \<in> set evs;
paulson@18886
  1379
         Key authK \<notin> analz (spies evs);
paulson@18886
  1380
         \<not> expiredSK Ts evs;
paulson@18886
  1381
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1382
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@37811
  1383
by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
paulson@14182
  1384
wenzelm@61830
  1385
text\<open>In the real world Tgs CAN check what Kas sends!\<close>
paulson@18886
  1386
lemma Confidentiality_Tgs_bis:
paulson@18886
  1387
     "\<lbrakk> Says Kas A
paulson@18886
  1388
               (Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
paulson@14182
  1389
           \<in> set evs;
paulson@14182
  1390
         Says Tgs A
paulson@18886
  1391
              (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
  1392
           \<in> set evs;
paulson@18886
  1393
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1394
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1395
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@37811
  1396
by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
paulson@14182
  1397
wenzelm@61830
  1398
text\<open>Most general form\<close>
paulson@18886
  1399
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
paulson@18886
  1400
paulson@18886
  1401
lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
paulson@18886
  1402
wenzelm@61830
  1403
text\<open>Needs a confidentiality guarantee, hence moved here.
wenzelm@61830
  1404
      Authenticity of servK for A\<close>
paulson@18886
  1405
lemma servK_authentic_bis_r:
paulson@18886
  1406
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1407
           \<in> parts (spies evs);
paulson@18886
  1408
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1409
           \<in> parts (spies evs);
paulson@18886
  1410
         \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1411
 \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@18886
  1412
       \<in> set evs"
paulson@37811
  1413
by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
paulson@18886
  1414
paulson@18886
  1415
lemma Confidentiality_Serv_A:
paulson@18886
  1416
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1417
           \<in> parts (spies evs);
paulson@18886
  1418
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1419
           \<in> parts (spies evs);
paulson@18886
  1420
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1421
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1422
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1423
apply (drule authK_authentic, assumption, assumption)
paulson@18886
  1424
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
paulson@18886
  1425
done
paulson@18886
  1426
paulson@18886
  1427
lemma Confidentiality_B:
paulson@18886
  1428
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1429
           \<in> parts (spies evs);
paulson@18886
  1430
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1431
           \<in> parts (spies evs);
paulson@18886
  1432
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1433
           \<in> parts (spies evs);
paulson@18886
  1434
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1435
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1436
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1437
apply (frule authK_authentic)
paulson@18886
  1438
apply (frule_tac [3] Confidentiality_Kas)
paulson@18886
  1439
apply (frule_tac [6] servTicket_authentic, auto)
paulson@18886
  1440
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
paulson@18886
  1441
done
paulson@18886
  1442
(*
paulson@18886
  1443
The proof above is fast.  It can be done in one command in 17 secs:
paulson@18886
  1444
apply (blast dest: authK_authentic servK_authentic
paulson@18886
  1445
                               Says_Kas_message_form servTicket_authentic
paulson@18886
  1446
                               unique_servKeys unique_authKeys
paulson@18886
  1447
                               Confidentiality_Kas
paulson@18886
  1448
                               Confidentiality_Tgs_bis)
paulson@18886
  1449
It is very brittle: we can't use this command partway
paulson@18886
  1450
through the script above.
paulson@18886
  1451
*)
paulson@18886
  1452
paulson@18886
  1453
lemma u_Confidentiality_B:
paulson@18886
  1454
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1455
           \<in> parts (spies evs);
paulson@18886
  1456
         \<not> expiredSK Ts evs;
paulson@18886
  1457
         A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1458
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@37811
  1459
by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
paulson@14182
  1460
paulson@14182
  1461
paulson@18886
  1462
wenzelm@61830
  1463
subsection\<open>Parties authentication: each party verifies "the identity of
wenzelm@61830
  1464
       another party who generated some data" (quoted from Neuman and Ts'o).\<close>
paulson@14182
  1465
wenzelm@61830
  1466
text\<open>These guarantees don't assess whether two parties agree on
paulson@18886
  1467
         the same session key: sending a message containing a key
wenzelm@61830
  1468
         doesn't a priori state knowledge of the key.\<close>
paulson@18886
  1469
paulson@14182
  1470
wenzelm@61830
  1471
text\<open>\<open>Tgs_authenticates_A\<close> can be found above\<close>
paulson@18886
  1472
paulson@18886
  1473
lemma A_authenticates_Tgs:
paulson@18886
  1474
 "\<lbrakk> Says Kas A
paulson@18886
  1475
    (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
paulson@18886
  1476
     Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14182
  1477
       \<in> parts (spies evs);
paulson@18886
  1478
     Key authK \<notin> analz (spies evs);
paulson@18886
  1479
     evs \<in> kerbIV \<rbrakk>
paulson@18886
  1480
 \<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
paulson@14182
  1481
       \<in> set evs"
paulson@14182
  1482
apply (frule Says_Kas_message_form, assumption)
paulson@14182
  1483
apply (erule rev_mp)
paulson@14182
  1484
apply (erule rev_mp)
paulson@14182
  1485
apply (erule rev_mp)
paulson@18886
  1486
apply (erule kerbIV.induct, analz_mono_contra)
paulson@14182
  1487
apply (frule_tac [7] K5_msg_in_parts_spies)
paulson@14182
  1488
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
wenzelm@61830
  1489
txt\<open>K2\<close>
paulson@18886
  1490
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
wenzelm@61830
  1491
txt\<open>K4\<close>
paulson@37811
  1492
apply (blast dest!: unique_CryptKey)
paulson@14182
  1493
done
paulson@14182
  1494
paulson@14182
  1495
paulson@18886
  1496
lemma B_authenticates_A:
paulson@18886
  1497
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1498
        Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1499
           \<in> parts (spies evs);
paulson@18886
  1500
        Key servK \<notin> analz (spies evs);
paulson@18886
  1501
        A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1502
 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
paulson@18886
  1503
               Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
paulson@37811
  1504
by (blast dest: servTicket_authentic_Tgs intro: Says_K5)
paulson@14182
  1505
wenzelm@61830
  1506
text\<open>The second assumption tells B what kind of key servK is.\<close>
paulson@18886
  1507
lemma B_authenticates_A_r:
paulson@18886
  1508
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1509
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1510
           \<in> parts (spies evs);
paulson@18886
  1511
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1512
           \<in> parts (spies evs);
paulson@18886
  1513
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1514
           \<in> parts (spies evs);
paulson@18886
  1515
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1516
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1517
   \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
paulson@18886
  1518
                  Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
paulson@37811
  1519
by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
paulson@14182
  1520
wenzelm@61830
  1521
text\<open>\<open>u_B_authenticates_A\<close> would be the same as \<open>B_authenticates_A\<close> because the servK confidentiality assumption is yet unrelaxed\<close>
paulson@14182
  1522
paulson@18886
  1523
lemma u_B_authenticates_A_r:
paulson@18886
  1524
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1525
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@14182
  1526
           \<in> parts (spies evs);
paulson@18886
  1527
         \<not> expiredSK Ts evs;
paulson@18886
  1528
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1529
   \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
paulson@18886
  1530
                  Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
paulson@37811
  1531
by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
paulson@14182
  1532
paulson@18886
  1533
lemma A_authenticates_B:
paulson@18886
  1534
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1535
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14182
  1536
           \<in> parts (spies evs);
paulson@18886
  1537
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@14182
  1538
           \<in> parts (spies evs);
paulson@18886
  1539
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
paulson@18886
  1540
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1541
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@37811
  1542
by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)
paulson@14182
  1543
paulson@18886
  1544
lemma A_authenticates_B_r:
paulson@18886
  1545
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1546
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14182
  1547
           \<in> parts (spies evs);
paulson@18886
  1548
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@14182
  1549
           \<in> parts (spies evs);
paulson@18886
  1550
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1551
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1552
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@18886
  1553
apply (frule authK_authentic)
paulson@14182
  1554
apply (frule_tac [3] Says_Kas_message_form)
paulson@14182
  1555
apply (frule_tac [4] Confidentiality_Kas)
paulson@18886
  1556
apply (frule_tac [7] servK_authentic)
paulson@14182
  1557
prefer 8 apply blast
paulson@14182
  1558
apply (erule_tac [9] exE)
paulson@14182
  1559
apply (frule_tac [9] K4_imp_K2)
paulson@14182
  1560
apply assumption+
paulson@18886
  1561
apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
paulson@14182
  1562
)
paulson@14182
  1563
done
paulson@14182
  1564
paulson@14182
  1565
wenzelm@61830
  1566
subsection\<open>Key distribution guarantees
paulson@18886
  1567
       An agent knows a session key if he used it to issue a cipher.
paulson@18886
  1568
       These guarantees also convey a stronger form of 
wenzelm@61830
  1569
       authentication - non-injective agreement on the session key\<close>
paulson@18886
  1570
paulson@18886
  1571
paulson@18886
  1572
lemma Kas_Issues_A:
paulson@18886
  1573
   "\<lbrakk> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs;
paulson@18886
  1574
      evs \<in> kerbIV \<rbrakk>
paulson@18886
  1575
  \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 
paulson@18886
  1576
          on evs"
paulson@18886
  1577
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1578
apply (rule exI)
paulson@18886
  1579
apply (rule conjI, assumption)
paulson@18886
  1580
apply (simp (no_asm))
paulson@18886
  1581
apply (erule rev_mp)
paulson@18886
  1582
apply (erule kerbIV.induct)
paulson@18886
  1583
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1584
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1585
apply (simp_all (no_asm_simp) add: all_conj_distrib)
wenzelm@61830
  1586
txt\<open>K2\<close>
paulson@18886
  1587
apply (simp add: takeWhile_tail)
paulson@18886
  1588
apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
  1589
done
paulson@18886
  1590
paulson@18886
  1591
lemma A_authenticates_and_keydist_to_Kas:
paulson@18886
  1592
  "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace> \<in> parts (spies evs);
paulson@18886
  1593
     A \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1594
 \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 
paulson@18886
  1595
          on evs"
paulson@37811
  1596
by (blast dest: authK_authentic Kas_Issues_A)
paulson@14182
  1597
paulson@18886
  1598
lemma honest_never_says_newer_timestamp_in_auth:
paulson@18886
  1599
     "\<lbrakk> (CT evs) \<le> T; A \<notin> bad; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 
paulson@18886
  1600
     \<Longrightarrow> \<forall> B Y.  Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
paulson@18886
  1601
apply (erule rev_mp)
paulson@18886
  1602
apply (erule kerbIV.induct)
paulson@18886
  1603
apply force+
paulson@18886
  1604
done
paulson@18886
  1605
paulson@18886
  1606
lemma honest_never_says_current_timestamp_in_auth:
paulson@18886
  1607
     "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 
paulson@18886
  1608
     \<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
paulson@32366
  1609
  by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth)
paulson@18886
  1610
paulson@18886
  1611
lemma A_trusts_secure_authenticator:
paulson@18886
  1612
    "\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
paulson@18886
  1613
       Key K \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk>
paulson@18886
  1614
\<Longrightarrow> \<exists> B X. Says A Tgs \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>, Agent B\<rbrace> \<in> set evs \<or> 
paulson@37811
  1615
           Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
  1616
apply (erule rev_mp)
paulson@18886
  1617
apply (erule rev_mp)
paulson@18886
  1618
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
  1619
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1620
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1621
apply (simp_all add: all_conj_distrib)
paulson@18886
  1622
apply blast+
paulson@18886
  1623
done
paulson@18886
  1624
paulson@18886
  1625
lemma A_Issues_Tgs:
paulson@18886
  1626
  "\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
paulson@18886
  1627
       \<in> set evs; 
paulson@18886
  1628
     Key authK \<notin> analz (spies evs);  
paulson@18886
  1629
     A \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1630
 \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
paulson@14182
  1631
apply (simp (no_asm) add: Issues_def)
paulson@14182
  1632
apply (rule exI)
paulson@14182
  1633
apply (rule conjI, assumption)
paulson@14182
  1634
apply (simp (no_asm))
paulson@14182
  1635
apply (erule rev_mp)
paulson@14182
  1636
apply (erule rev_mp)
paulson@18886
  1637
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
  1638
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1639
apply (frule_tac [7] Says_ticket_parts)
paulson@14182
  1640
apply (simp_all (no_asm_simp) add: all_conj_distrib)
wenzelm@61830
  1641
txt\<open>fake\<close>
paulson@14182
  1642
apply blast
wenzelm@61830
  1643
txt\<open>K3\<close>
paulson@18886
  1644
(*
paulson@18886
  1645
apply clarify
paulson@18886
  1646
apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption, assumption, assumption)
paulson@18886
  1647
*)
paulson@14182
  1648
apply (simp add: takeWhile_tail)
paulson@18886
  1649
apply auto
paulson@18886
  1650
apply (force dest!: authK_authentic Says_Kas_message_form)
paulson@18886
  1651
apply (drule parts_spies_takeWhile_mono [THEN subsetD, THEN parts_spies_evs_revD2 [THEN subsetD]])
paulson@18886
  1652
apply (drule A_trusts_secure_authenticator, assumption, assumption)
paulson@18886
  1653
apply (simp add: honest_never_says_current_timestamp_in_auth)
paulson@14182
  1654
done
paulson@14182
  1655
paulson@18886
  1656
lemma Tgs_authenticates_and_keydist_to_A:
paulson@18886
  1657
  "\<lbrakk>  Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs); 
paulson@18886
  1658
      Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
paulson@14182
  1659
           \<in> parts (spies evs);
paulson@18886
  1660
     Key authK \<notin> analz (spies evs);  
paulson@18886
  1661
     A \<notin> bad; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1662
 \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
paulson@37811
  1663
by (blast dest: A_Issues_Tgs Tgs_authenticates_A)
paulson@14182
  1664
paulson@18886
  1665
lemma Tgs_Issues_A:
paulson@18886
  1666
    "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>)
paulson@18886
  1667
         \<in> set evs; 
paulson@18886
  1668
       Key authK \<notin> analz (spies evs);  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1669
  \<Longrightarrow> Tgs Issues A with 
paulson@18886
  1670
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
paulson@18886
  1671
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1672
apply (rule exI)
paulson@18886
  1673
apply (rule conjI, assumption)
paulson@18886
  1674
apply (simp (no_asm))
paulson@14182
  1675
apply (erule rev_mp)
paulson@14182
  1676
apply (erule rev_mp)
paulson@18886
  1677
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
  1678
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1679
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1680
apply (simp_all (no_asm_simp) add: all_conj_distrib)
wenzelm@61830
  1681
txt\<open>K4\<close>
paulson@18886
  1682
apply (simp add: takeWhile_tail)
paulson@18886
  1683
(*Last two thms installed only to derive authK \<notin> range shrK*)
paulson@37811
  1684
apply (metis knows_Spy_partsEs(2) parts.Fst usedI used_evs_rev used_takeWhile_used)
paulson@14182
  1685
done
paulson@14182
  1686
paulson@18886
  1687
lemma A_authenticates_and_keydist_to_Tgs:
paulson@18886
  1688
"\<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace> \<in> parts (spies evs);
paulson@18886
  1689
  Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1690
 \<Longrightarrow> \<exists>A. Tgs Issues A with 
paulson@18886
  1691
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
paulson@37811
  1692
by (blast dest: Tgs_Issues_A servK_authentic_bis)
paulson@18886
  1693
paulson@18886
  1694
paulson@18886
  1695
paulson@18886
  1696
lemma B_Issues_A:
paulson@18886
  1697
     "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
paulson@18886
  1698
         Key servK \<notin> analz (spies evs);
paulson@18886
  1699
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1700
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@14182
  1701
apply (simp (no_asm) add: Issues_def)
paulson@14182
  1702
apply (rule exI)
paulson@14182
  1703
apply (rule conjI, assumption)
paulson@14182
  1704
apply (simp (no_asm))
paulson@14182
  1705
apply (erule rev_mp)
paulson@14182
  1706
apply (erule rev_mp)
paulson@18886
  1707
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
  1708
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1709
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1710
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
  1711
apply blast
wenzelm@61830
  1712
txt\<open>K6 requires numerous lemmas\<close>
paulson@18886
  1713
apply (simp add: takeWhile_tail)
paulson@18886
  1714
apply (blast dest: servTicket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6)
paulson@18886
  1715
done
paulson@18886
  1716
paulson@18886
  1717
lemma B_Issues_A_r:
paulson@18886
  1718
     "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
paulson@18886
  1719
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1720
            \<in> parts (spies evs);
paulson@18886
  1721
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1722
            \<in> parts (spies evs);
paulson@18886
  1723
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1724
           \<in> parts (spies evs);
paulson@18886
  1725
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1726
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1727
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@37811
  1728
by (blast dest!: Confidentiality_B B_Issues_A)
paulson@18886
  1729
paulson@18886
  1730
lemma u_B_Issues_A_r:
paulson@18886
  1731
     "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
paulson@18886
  1732
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1733
            \<in> parts (spies evs);
paulson@18886
  1734
         \<not> expiredSK Ts evs;
paulson@18886
  1735
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1736
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@37811
  1737
by (blast dest!: u_Confidentiality_B B_Issues_A)
paulson@18886
  1738
paulson@18886
  1739
lemma A_authenticates_and_keydist_to_B:
paulson@18886
  1740
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1741
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1742
           \<in> parts (spies evs);
paulson@18886
  1743
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1744
           \<in> parts (spies evs);
paulson@18886
  1745
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
paulson@18886
  1746
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1747
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@37811
  1748
by (blast dest!: A_authenticates_B B_Issues_A)
paulson@18886
  1749
paulson@18886
  1750
lemma A_authenticates_and_keydist_to_B_r:
paulson@18886
  1751
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1752
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1753
           \<in> parts (spies evs);
paulson@18886
  1754
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1755
           \<in> parts (spies evs);
paulson@18886
  1756
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1757
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
paulson@18886
  1758
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@37811
  1759
by (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
paulson@18886
  1760
paulson@18886
  1761
paulson@18886
  1762
lemma A_Issues_B:
paulson@18886
  1763
     "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
paulson@18886
  1764
           \<in> set evs;
paulson@18886
  1765
         Key servK \<notin> analz (spies evs);
paulson@18886
  1766
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1767
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@18886
  1768
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1769
apply (rule exI)
paulson@18886
  1770
apply (rule conjI, assumption)
paulson@18886
  1771
apply (simp (no_asm))
paulson@18886
  1772
apply (erule rev_mp)
paulson@18886
  1773
apply (erule rev_mp)
paulson@18886
  1774
apply (erule kerbIV.induct, analz_mono_contra)
paulson@18886
  1775
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1776
apply (frule_tac [7] Says_ticket_parts)
paulson@14182
  1777
apply (simp_all (no_asm_simp))
paulson@14182
  1778
apply clarify
wenzelm@61830
  1779
txt\<open>K5\<close>
paulson@14182
  1780
apply auto
paulson@14182
  1781
apply (simp add: takeWhile_tail)
wenzelm@61830
  1782
txt\<open>Level 15: case analysis necessary because the assumption doesn't state
wenzelm@61830
  1783
  the form of servTicket. The guarantee becomes stronger.\<close>
paulson@14207
  1784
apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
paulson@18886
  1785
                   K3_imp_K2 servK_authentic_ter
paulson@14207
  1786
                   parts_spies_takeWhile_mono [THEN subsetD]
paulson@14182
  1787
                   parts_spies_evs_revD2 [THEN subsetD]
paulson@18886
  1788
             intro: Says_K5)
paulson@14182
  1789
apply (simp add: takeWhile_tail)
paulson@14182
  1790
done
paulson@14182
  1791
paulson@18886
  1792
lemma A_Issues_B_r:
paulson@18886
  1793
     "\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace>
paulson@14182
  1794
           \<in> set evs;
paulson@18886
  1795
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@18886
  1796
           \<in> parts (spies evs);
paulson@18886
  1797
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@14182
  1798
           \<in> parts (spies evs);
paulson@18886
  1799
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1800
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1801
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@37811
  1802
by (blast dest!: Confidentiality_Serv_A A_Issues_B)
paulson@18886
  1803
paulson@18886
  1804
lemma B_authenticates_and_keydist_to_A:
paulson@18886
  1805
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1806
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@14182
  1807
           \<in> parts (spies evs);
paulson@18886
  1808
         Key servK \<notin> analz (spies evs);
paulson@18886
  1809
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1810
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@37811
  1811
by (blast dest: B_authenticates_A A_Issues_B)
paulson@14182
  1812
paulson@18886
  1813
lemma B_authenticates_and_keydist_to_A_r:
paulson@18886
  1814
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1815
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@14182
  1816
           \<in> parts (spies evs);
paulson@18886
  1817
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
paulson@18886
  1818
           \<in> parts (spies evs);
paulson@18886
  1819
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
paulson@14182
  1820
           \<in> parts (spies evs);
paulson@18886
  1821
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1822
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1823
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@37811
  1824
by (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
paulson@18886
  1825
wenzelm@61830
  1826
text\<open>\<open>u_B_authenticates_and_keydist_to_A\<close> would be the same as \<open>B_authenticates_and_keydist_to_A\<close> because the
wenzelm@61830
  1827
 servK confidentiality assumption is yet unrelaxed\<close>
paulson@18886
  1828
paulson@18886
  1829
lemma u_B_authenticates_and_keydist_to_A_r:
paulson@18886
  1830
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1831
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@14182
  1832
           \<in> parts (spies evs);
paulson@18886
  1833
         \<not> expiredSK Ts evs;
paulson@18886
  1834
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
paulson@18886
  1835
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@37811
  1836
by (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
paulson@6452
  1837
paulson@6452
  1838
end