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