src/HOL/Auth/KerberosV.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 26300 03def556e26e
child 32404 da3ca3c6ec81
permissions -rw-r--r--
generalize tendsto to class topological_space
paulson@18886
     1
(*  ID:         $Id$
paulson@18886
     2
    Author:     Giampaolo Bella, Catania University
paulson@18886
     3
*)
paulson@18886
     4
paulson@18886
     5
header{*The Kerberos Protocol, Version V*}
paulson@18886
     6
paulson@18886
     7
theory KerberosV imports Public begin
paulson@18886
     8
paulson@18886
     9
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
    10
wenzelm@20768
    11
abbreviation
wenzelm@21404
    12
  Kas :: agent where
wenzelm@20768
    13
  "Kas == Server"
paulson@18886
    14
wenzelm@21404
    15
abbreviation
wenzelm@21404
    16
  Tgs :: agent where
wenzelm@20768
    17
  "Tgs == Friend 0"
paulson@18886
    18
paulson@18886
    19
paulson@18886
    20
axioms
paulson@18886
    21
  Tgs_not_bad [iff]: "Tgs \<notin> bad"
paulson@18886
    22
   --{*Tgs is secure --- we already know that Kas is secure*}
paulson@18886
    23
paulson@18886
    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. 
paulson@18886
    28
        Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Ta\<rbrace>,
paulson@18886
    29
                     Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Ta\<rbrace>
paulson@18886
    30
                   \<rbrace> \<in> set evs}"
paulson@18886
    31
paulson@18886
    32
 (* A is the true creator of X if she has sent X and X never appeared on
paulson@18886
    33
    the trace before this event. Recall that traces grow from head. *)
paulson@18886
    34
  Issues :: "[agent, agent, msg, event list] => bool"
paulson@18886
    35
             ("_ Issues _ with _ on _")
paulson@18886
    36
   "A Issues B with X on evs ==
paulson@18886
    37
      \<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
paulson@18886
    38
      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
paulson@18886
    39
paulson@18886
    40
paulson@18886
    41
consts
paulson@18886
    42
    (*Duration of the authentication key*)
paulson@18886
    43
    authKlife   :: nat
paulson@18886
    44
paulson@18886
    45
    (*Duration of the service key*)
paulson@18886
    46
    servKlife   :: nat
paulson@18886
    47
paulson@18886
    48
    (*Duration of an authenticator*)
paulson@18886
    49
    authlife   :: nat
paulson@18886
    50
paulson@18886
    51
    (*Upper bound on the time of reaction of a server*)
paulson@18886
    52
    replylife   :: nat
paulson@18886
    53
paulson@18886
    54
specification (authKlife)
paulson@18886
    55
  authKlife_LB [iff]: "2 \<le> authKlife"
paulson@18886
    56
    by blast
paulson@18886
    57
paulson@18886
    58
specification (servKlife)
paulson@18886
    59
  servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
paulson@18886
    60
    by blast
paulson@18886
    61
paulson@18886
    62
specification (authlife)
paulson@18886
    63
  authlife_LB [iff]: "Suc 0 \<le> authlife"
paulson@18886
    64
    by blast
paulson@18886
    65
paulson@18886
    66
specification (replylife)
paulson@18886
    67
  replylife_LB [iff]: "Suc 0 \<le> replylife"
paulson@18886
    68
    by blast
paulson@18886
    69
wenzelm@20768
    70
abbreviation
wenzelm@20768
    71
  (*The current time is just the length of the trace!*)
wenzelm@21404
    72
  CT :: "event list=>nat" where
wenzelm@20768
    73
  "CT == length"
paulson@18886
    74
wenzelm@21404
    75
abbreviation
wenzelm@21404
    76
  expiredAK :: "[nat, event list] => bool" where
wenzelm@20768
    77
  "expiredAK T evs == authKlife + T < CT evs"
paulson@18886
    78
wenzelm@21404
    79
abbreviation
wenzelm@21404
    80
  expiredSK :: "[nat, event list] => bool" where
wenzelm@20768
    81
  "expiredSK T evs == servKlife + T < CT evs"
paulson@18886
    82
wenzelm@21404
    83
abbreviation
wenzelm@21404
    84
  expiredA :: "[nat, event list] => bool" where
wenzelm@20768
    85
  "expiredA T evs == authlife + T < CT evs"
paulson@18886
    86
wenzelm@21404
    87
abbreviation
wenzelm@21404
    88
  valid :: "[nat, nat] => bool"  ("valid _ wrt _") where
wenzelm@20768
    89
  "valid T1 wrt T2 == T1 <= replylife + T2"
paulson@18886
    90
paulson@18886
    91
(*---------------------------------------------------------------------*)
paulson@18886
    92
paulson@18886
    93
paulson@18886
    94
(* Predicate formalising the association between authKeys and servKeys *)
paulson@18886
    95
constdefs
paulson@18886
    96
  AKcryptSK :: "[key, key, event list] => bool"
paulson@18886
    97
  "AKcryptSK authK servK evs ==
paulson@18886
    98
     \<exists>A B tt.
paulson@18886
    99
       Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>,
paulson@18886
   100
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, tt\<rbrace> \<rbrace>
paulson@18886
   101
         \<in> set evs"
paulson@18886
   102
berghofe@23746
   103
inductive_set kerbV :: "event list set"
berghofe@23746
   104
  where
paulson@18886
   105
paulson@18886
   106
   Nil:  "[] \<in> kerbV"
paulson@18886
   107
berghofe@23746
   108
 | Fake: "\<lbrakk> evsf \<in> kerbV;  X \<in> synth (analz (spies evsf)) \<rbrakk>
paulson@18886
   109
          \<Longrightarrow> Says Spy B X  # evsf \<in> kerbV"
paulson@18886
   110
paulson@18886
   111
paulson@18886
   112
(*Authentication phase*)
berghofe@23746
   113
 | KV1:   "\<lbrakk> evs1 \<in> kerbV \<rbrakk>
paulson@18886
   114
          \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
paulson@18886
   115
          \<in> kerbV"
paulson@18886
   116
   (*Unlike version IV, authTicket is not re-encrypted*)
berghofe@23746
   117
 | KV2:  "\<lbrakk> evs2 \<in> kerbV; Key authK \<notin> used evs2; authK \<in> symKeys;
paulson@18886
   118
            Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
paulson@18886
   119
          \<Longrightarrow> Says Kas A \<lbrace>
paulson@18886
   120
          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2)\<rbrace>,
paulson@18886
   121
        Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number (CT evs2)\<rbrace> 
paulson@18886
   122
                         \<rbrace> # evs2 \<in> kerbV"
paulson@18886
   123
paulson@18886
   124
paulson@18886
   125
(* Authorisation phase *)
berghofe@23746
   126
 | KV3:  "\<lbrakk> evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs;
paulson@18886
   127
            Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
paulson@18886
   128
            Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   129
                          authTicket\<rbrace> \<in> set evs3;
paulson@18886
   130
            valid Ta wrt T1
paulson@18886
   131
         \<rbrakk>
paulson@18886
   132
          \<Longrightarrow> Says A Tgs \<lbrace>authTicket,
paulson@18886
   133
                           (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
paulson@18886
   134
                           Agent B\<rbrace> # evs3 \<in> kerbV"
paulson@18886
   135
   (*Unlike version IV, servTicket is not re-encrypted*)
berghofe@23746
   136
 | KV4:  "\<lbrakk> evs4 \<in> kerbV; Key servK \<notin> used evs4; servK \<in> symKeys;
paulson@18886
   137
            B \<noteq> Tgs;  authK \<in> symKeys;
paulson@18886
   138
            Says A' Tgs \<lbrace>
paulson@18886
   139
             (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
paulson@18886
   140
				 Number Ta\<rbrace>),
paulson@18886
   141
             (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
paulson@18886
   142
	        \<in> set evs4;
paulson@18886
   143
            \<not> expiredAK Ta evs4;
paulson@18886
   144
            \<not> expiredA T2 evs4;
paulson@18886
   145
            servKlife + (CT evs4) <= authKlife + Ta
paulson@18886
   146
         \<rbrakk>
paulson@18886
   147
          \<Longrightarrow> Says Tgs A \<lbrace>
paulson@18886
   148
             Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4)\<rbrace>,
paulson@18886
   149
   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number (CT evs4)\<rbrace> 
paulson@18886
   150
                          \<rbrace> # evs4 \<in> kerbV"
paulson@18886
   151
paulson@18886
   152
paulson@18886
   153
(*Service phase*)
berghofe@23746
   154
 | KV5:  "\<lbrakk> evs5 \<in> kerbV; authK \<in> symKeys; servK \<in> symKeys;
paulson@18886
   155
            A \<noteq> Kas; A \<noteq> Tgs;
paulson@18886
   156
            Says A Tgs
paulson@18886
   157
                \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
paulson@18886
   158
		  Agent B\<rbrace>
paulson@18886
   159
              \<in> set evs5;
paulson@18886
   160
            Says Tgs' A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   161
                          servTicket\<rbrace>
paulson@18886
   162
                \<in> set evs5;
paulson@18886
   163
            valid Ts wrt T2 \<rbrakk>
paulson@18886
   164
          \<Longrightarrow> Says A B \<lbrace>servTicket,
paulson@18886
   165
			 Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
paulson@18886
   166
               # evs5 \<in> kerbV"
paulson@18886
   167
berghofe@23746
   168
  | KV6:  "\<lbrakk> evs6 \<in> kerbV; B \<noteq> Kas; B \<noteq> Tgs;
paulson@18886
   169
            Says A' B \<lbrace>
paulson@18886
   170
              (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
paulson@18886
   171
              (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
paulson@18886
   172
            \<in> set evs6;
paulson@18886
   173
            \<not> expiredSK Ts evs6;
paulson@18886
   174
            \<not> expiredA T3 evs6
paulson@18886
   175
         \<rbrakk>
paulson@18886
   176
          \<Longrightarrow> Says B A (Crypt servK (Number Ta2))
paulson@18886
   177
               # evs6 \<in> kerbV"
paulson@18886
   178
paulson@18886
   179
paulson@18886
   180
paulson@18886
   181
(* Leaking an authK... *)
berghofe@23746
   182
 | Oops1:"\<lbrakk> evsO1 \<in> kerbV;  A \<noteq> Spy;
paulson@18886
   183
             Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   184
                          authTicket\<rbrace>  \<in> set evsO1;
paulson@18886
   185
              expiredAK Ta evsO1 \<rbrakk>
paulson@18886
   186
          \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
paulson@18886
   187
               # evsO1 \<in> kerbV"
paulson@18886
   188
paulson@18886
   189
(*Leaking a servK... *)
berghofe@23746
   190
 | Oops2: "\<lbrakk> evsO2 \<in> kerbV;  A \<noteq> Spy;
paulson@18886
   191
              Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   192
                           servTicket\<rbrace>  \<in> set evsO2;
paulson@18886
   193
              expiredSK Ts evsO2 \<rbrakk>
paulson@18886
   194
          \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
paulson@18886
   195
               # evsO2 \<in> kerbV"
paulson@18886
   196
paulson@18886
   197
paulson@18886
   198
paulson@18886
   199
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@18886
   200
declare parts.Body [dest]
paulson@18886
   201
declare analz_into_parts [dest]
paulson@18886
   202
declare Fake_parts_insert_in_Un [dest]
paulson@18886
   203
paulson@18886
   204
paulson@18886
   205
paulson@18886
   206
subsection{*Lemmas about lists, for reasoning about  Issues*}
paulson@18886
   207
paulson@18886
   208
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
paulson@18886
   209
apply (induct_tac "evs")
paulson@18886
   210
apply (induct_tac [2] "a", auto)
paulson@18886
   211
done
paulson@18886
   212
paulson@18886
   213
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
paulson@18886
   214
apply (induct_tac "evs")
paulson@18886
   215
apply (induct_tac [2] "a", auto)
paulson@18886
   216
done
paulson@18886
   217
paulson@18886
   218
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
paulson@18886
   219
          (if A:bad then insert X (spies evs) else spies evs)"
paulson@18886
   220
apply (induct_tac "evs")
paulson@18886
   221
apply (induct_tac [2] "a", auto)
paulson@18886
   222
done
paulson@18886
   223
paulson@18886
   224
lemma spies_evs_rev: "spies evs = spies (rev evs)"
paulson@18886
   225
apply (induct_tac "evs")
paulson@18886
   226
apply (induct_tac [2] "a")
paulson@18886
   227
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
paulson@18886
   228
done
paulson@18886
   229
paulson@18886
   230
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
paulson@18886
   231
paulson@18886
   232
lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
paulson@18886
   233
apply (induct_tac "evs")
paulson@18886
   234
apply (induct_tac [2] "a", auto)
paulson@18886
   235
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
paulson@18886
   236
done
paulson@18886
   237
paulson@18886
   238
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
paulson@18886
   239
paulson@18886
   240
paulson@18886
   241
subsection{*Lemmas about @{term authKeys}*}
paulson@18886
   242
paulson@18886
   243
lemma authKeys_empty: "authKeys [] = {}"
paulson@18886
   244
apply (unfold authKeys_def)
paulson@18886
   245
apply (simp (no_asm))
paulson@18886
   246
done
paulson@18886
   247
paulson@18886
   248
lemma authKeys_not_insert:
paulson@18886
   249
 "(\<forall>A Ta akey Peer.
paulson@18886
   250
   ev \<noteq> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta\<rbrace>,
paulson@18886
   251
                     Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace> \<rbrace>)
paulson@18886
   252
       \<Longrightarrow> authKeys (ev # evs) = authKeys evs"
paulson@18886
   253
apply (unfold authKeys_def, auto)
paulson@18886
   254
done
paulson@18886
   255
paulson@18886
   256
lemma authKeys_insert:
paulson@18886
   257
  "authKeys
paulson@18886
   258
     (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta\<rbrace>,
paulson@18886
   259
         Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace> \<rbrace> # evs)
paulson@18886
   260
       = insert K (authKeys evs)"
paulson@18886
   261
apply (unfold authKeys_def, auto)
paulson@18886
   262
done
paulson@18886
   263
paulson@18886
   264
lemma authKeys_simp:
paulson@18886
   265
   "K \<in> authKeys
paulson@18886
   266
    (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta\<rbrace>,
paulson@18886
   267
        Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace> \<rbrace> # evs)
paulson@18886
   268
        \<Longrightarrow> K = K' | K \<in> authKeys evs"
paulson@18886
   269
apply (unfold authKeys_def, auto)
paulson@18886
   270
done
paulson@18886
   271
paulson@18886
   272
lemma authKeysI:
paulson@18886
   273
   "Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   274
         Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace> \<rbrace> \<in> set evs
paulson@18886
   275
        \<Longrightarrow> K \<in> authKeys evs"
paulson@18886
   276
apply (unfold authKeys_def, auto)
paulson@18886
   277
done
paulson@18886
   278
paulson@18886
   279
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
paulson@18886
   280
apply (simp add: authKeys_def, blast)
paulson@18886
   281
done
paulson@18886
   282
paulson@18886
   283
paulson@18886
   284
subsection{*Forwarding Lemmas*}
paulson@18886
   285
paulson@18886
   286
lemma Says_ticket_parts:
paulson@18886
   287
     "Says S A \<lbrace>Crypt K \<lbrace>SesKey, B, TimeStamp\<rbrace>, Ticket\<rbrace>
paulson@18886
   288
               \<in> set evs \<Longrightarrow> Ticket \<in> parts (spies evs)"
paulson@18886
   289
apply blast
paulson@18886
   290
done
paulson@18886
   291
paulson@18886
   292
lemma Says_ticket_analz:
paulson@18886
   293
     "Says S A \<lbrace>Crypt K \<lbrace>SesKey, B, TimeStamp\<rbrace>, Ticket\<rbrace>
paulson@18886
   294
               \<in> set evs \<Longrightarrow> Ticket \<in> analz (spies evs)"
paulson@18886
   295
apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
paulson@18886
   296
done
paulson@18886
   297
paulson@18886
   298
lemma Oops_range_spies1:
paulson@18886
   299
     "\<lbrakk> Says Kas A \<lbrace>Crypt KeyA \<lbrace>Key authK, Peer, Ta\<rbrace>, authTicket\<rbrace>
paulson@18886
   300
           \<in> set evs ;
paulson@18886
   301
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
paulson@18886
   302
apply (erule rev_mp)
paulson@18886
   303
apply (erule kerbV.induct, auto)
paulson@18886
   304
done
paulson@18886
   305
paulson@18886
   306
lemma Oops_range_spies2:
paulson@18886
   307
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
   308
           \<in> set evs ;
paulson@18886
   309
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys"
paulson@18886
   310
apply (erule rev_mp)
paulson@18886
   311
apply (erule kerbV.induct, auto)
paulson@18886
   312
done
paulson@18886
   313
paulson@18886
   314
paulson@18886
   315
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
paulson@18886
   316
lemma Spy_see_shrK [simp]:
paulson@18886
   317
     "evs \<in> kerbV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@18886
   318
apply (erule kerbV.induct)
paulson@18886
   319
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   320
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   321
apply (blast+)
paulson@18886
   322
done
paulson@18886
   323
paulson@18886
   324
lemma Spy_analz_shrK [simp]:
paulson@18886
   325
     "evs \<in> kerbV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@18886
   326
by auto
paulson@18886
   327
paulson@18886
   328
lemma Spy_see_shrK_D [dest!]:
paulson@18886
   329
     "\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbV \<rbrakk> \<Longrightarrow> A:bad"
paulson@18886
   330
by (blast dest: Spy_see_shrK)
paulson@18886
   331
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
paulson@18886
   332
paulson@18886
   333
text{*Nobody can have used non-existent keys!*}
paulson@18886
   334
lemma new_keys_not_used [simp]:
paulson@18886
   335
    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbV\<rbrakk>
paulson@18886
   336
     \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
paulson@18886
   337
apply (erule rev_mp)
paulson@18886
   338
apply (erule kerbV.induct)
paulson@18886
   339
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   340
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   341
txt{*Fake*}
paulson@18886
   342
apply (force dest!: keysFor_parts_insert)
paulson@18886
   343
txt{*Others*}
paulson@18886
   344
apply (force dest!: analz_shrK_Decrypt)+
paulson@18886
   345
done
paulson@18886
   346
paulson@18886
   347
(*Earlier, all protocol proofs declared this theorem.
paulson@18886
   348
  But few of them actually need it! (Another is Yahalom) *)
paulson@18886
   349
lemma new_keys_not_analzd:
paulson@18886
   350
 "\<lbrakk>evs \<in> kerbV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
paulson@18886
   351
  \<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
paulson@18886
   352
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
paulson@18886
   353
paulson@18886
   354
paulson@18886
   355
paulson@18886
   356
subsection{*Regularity Lemmas*}
paulson@18886
   357
text{*These concern the form of items passed in messages*}
paulson@18886
   358
paulson@18886
   359
text{*Describes the form of all components sent by Kas*}
paulson@18886
   360
lemma Says_Kas_message_form:
paulson@18886
   361
     "\<lbrakk> Says Kas A \<lbrace>Crypt K \<lbrace>Key authK, Agent Peer, Ta\<rbrace>, authTicket\<rbrace>
paulson@18886
   362
           \<in> set evs;
paulson@18886
   363
         evs \<in> kerbV \<rbrakk>
paulson@18886
   364
      \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 
paulson@18886
   365
  authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>) \<and>
paulson@18886
   366
             K = shrK A  \<and> Peer = Tgs"
paulson@18886
   367
apply (erule rev_mp)
paulson@18886
   368
apply (erule kerbV.induct)
paulson@18886
   369
apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
paulson@18886
   370
apply blast+
paulson@18886
   371
done
paulson@18886
   372
paulson@18886
   373
paulson@18886
   374
paulson@18886
   375
(*This lemma is essential for proving Says_Tgs_message_form:
paulson@18886
   376
paulson@18886
   377
  the session key authK
paulson@18886
   378
  supplied by Kas in the authentication ticket
paulson@18886
   379
  cannot be a long-term key!
paulson@18886
   380
paulson@18886
   381
  Generalised to any session keys (both authK and servK).
paulson@18886
   382
*)
paulson@18886
   383
lemma SesKey_is_session_key:
paulson@18886
   384
     "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
paulson@18886
   385
            \<in> parts (spies evs); Tgs_B \<notin> bad;
paulson@18886
   386
         evs \<in> kerbV \<rbrakk>
paulson@18886
   387
      \<Longrightarrow> SesKey \<notin> range shrK"
paulson@18886
   388
apply (erule rev_mp)
paulson@18886
   389
apply (erule kerbV.induct)
paulson@18886
   390
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   391
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
paulson@18886
   392
done
paulson@18886
   393
paulson@18886
   394
lemma authTicket_authentic:
paulson@18886
   395
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
paulson@18886
   396
           \<in> parts (spies evs);
paulson@18886
   397
         evs \<in> kerbV \<rbrakk>
paulson@18886
   398
      \<Longrightarrow> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>,
paulson@18886
   399
                 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>\<rbrace>
paulson@18886
   400
            \<in> set evs"
paulson@18886
   401
apply (erule rev_mp)
paulson@18886
   402
apply (erule kerbV.induct)
paulson@18886
   403
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   404
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   405
txt{*Fake, K4*}
paulson@18886
   406
apply (blast+)
paulson@18886
   407
done
paulson@18886
   408
paulson@18886
   409
lemma authTicket_crypt_authK:
paulson@18886
   410
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
paulson@18886
   411
           \<in> parts (spies evs);
paulson@18886
   412
         evs \<in> kerbV \<rbrakk>
paulson@18886
   413
      \<Longrightarrow> authK \<in> authKeys evs"
paulson@18886
   414
apply (frule authTicket_authentic, assumption)
paulson@18886
   415
apply (simp (no_asm) add: authKeys_def)
paulson@18886
   416
apply blast
paulson@18886
   417
done
paulson@18886
   418
paulson@18886
   419
text{*Describes the form of servK, servTicket and authK sent by Tgs*}
paulson@18886
   420
lemma Says_Tgs_message_form:
paulson@18886
   421
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
   422
           \<in> set evs;
paulson@18886
   423
         evs \<in> kerbV \<rbrakk>
paulson@18886
   424
   \<Longrightarrow> B \<noteq> Tgs \<and> 
paulson@18886
   425
       servK \<notin> range shrK \<and> servK \<notin> authKeys evs \<and> servK \<in> symKeys \<and>
paulson@18886
   426
       servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>) \<and>
paulson@18886
   427
       authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys"
paulson@18886
   428
apply (erule rev_mp)
paulson@18886
   429
apply (erule kerbV.induct)
paulson@18886
   430
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto)
paulson@18886
   431
txt{*Three subcases of Message 4*}
paulson@18886
   432
apply (blast dest!: authKeys_used Says_Kas_message_form)
paulson@18886
   433
apply (blast dest!: SesKey_is_session_key)
paulson@18886
   434
apply (blast dest: authTicket_crypt_authK)
paulson@18886
   435
done
paulson@18886
   436
paulson@18886
   437
paulson@18886
   438
paulson@18886
   439
(*
paulson@18886
   440
lemma authTicket_form:
paulson@18886
   441
lemma servTicket_form:
paulson@18886
   442
lemma Says_kas_message_form:
paulson@18886
   443
lemma Says_tgs_message_form:
paulson@18886
   444
paulson@18886
   445
cannot be proved for version V, but a new proof strategy can be used in their
paulson@18886
   446
place. The new strategy merely says that both the authTicket and the servTicket
paulson@18886
   447
are in parts and in analz as soon as they appear, using lemmas Says_ticket_parts and Says_ticket_analz. 
paulson@18886
   448
The new strategy always lets the simplifier solve cases K3 and K5, saving on
paulson@18886
   449
long dedicated analyses, which seemed unavoidable. For this reason, lemma 
paulson@18886
   450
servK_notin_authKeysD is no longer needed.
paulson@18886
   451
*)
paulson@18886
   452
paulson@18886
   453
subsection{*Authenticity theorems: confirm origin of sensitive messages*}
paulson@18886
   454
paulson@18886
   455
lemma authK_authentic:
paulson@18886
   456
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>
paulson@18886
   457
           \<in> parts (spies evs);
paulson@18886
   458
         A \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
   459
      \<Longrightarrow> \<exists> AT. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>, AT\<rbrace>
paulson@18886
   460
            \<in> set evs"
paulson@18886
   461
apply (erule rev_mp)
paulson@18886
   462
apply (erule kerbV.induct)
paulson@18886
   463
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   464
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   465
apply blast+
paulson@18886
   466
done
paulson@18886
   467
paulson@18886
   468
text{*If a certain encrypted message appears then it originated with Tgs*}
paulson@18886
   469
lemma servK_authentic:
paulson@18886
   470
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
paulson@18886
   471
           \<in> parts (spies evs);
paulson@18886
   472
         Key authK \<notin> analz (spies evs);
paulson@18886
   473
         authK \<notin> range shrK;
paulson@18886
   474
         evs \<in> kerbV \<rbrakk>
paulson@18886
   475
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
paulson@18886
   476
       \<in> set evs"
paulson@18886
   477
apply (erule rev_mp)
paulson@18886
   478
apply (erule rev_mp)
paulson@18886
   479
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   480
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   481
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   482
apply blast+
paulson@18886
   483
done
paulson@18886
   484
paulson@18886
   485
lemma servK_authentic_bis:
paulson@18886
   486
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
paulson@18886
   487
           \<in> parts (spies evs);
paulson@18886
   488
         Key authK \<notin> analz (spies evs);
paulson@18886
   489
         B \<noteq> Tgs;
paulson@18886
   490
         evs \<in> kerbV \<rbrakk>
paulson@18886
   491
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
paulson@18886
   492
       \<in> set evs"
paulson@18886
   493
apply (erule rev_mp)
paulson@18886
   494
apply (erule rev_mp)
paulson@18886
   495
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   496
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   497
apply (frule_tac [5] Says_ticket_parts, simp_all, blast+)
paulson@18886
   498
done
paulson@18886
   499
paulson@18886
   500
text{*Authenticity of servK for B*}
paulson@18886
   501
lemma servTicket_authentic_Tgs:
paulson@18886
   502
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>
paulson@18886
   503
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   504
         evs \<in> kerbV \<rbrakk>
paulson@18886
   505
 \<Longrightarrow> \<exists>authK.
paulson@18886
   506
       Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>,
paulson@18886
   507
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
paulson@18886
   508
       \<in> set evs"
paulson@18886
   509
apply (erule rev_mp)
paulson@18886
   510
apply (erule kerbV.induct)
paulson@18886
   511
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   512
apply (frule_tac [5] Says_ticket_parts, simp_all, blast+)
paulson@18886
   513
done
paulson@18886
   514
paulson@18886
   515
text{*Anticipated here from next subsection*}
paulson@18886
   516
lemma K4_imp_K2:
paulson@18886
   517
"\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
   518
      \<in> set evs;  evs \<in> kerbV\<rbrakk>
paulson@18886
   519
   \<Longrightarrow> \<exists>Ta. Says Kas A
paulson@18886
   520
        \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   521
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
paulson@18886
   522
        \<in> set evs"
paulson@18886
   523
apply (erule rev_mp)
paulson@18886
   524
apply (erule kerbV.induct)
paulson@18886
   525
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   526
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
paulson@18886
   527
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
paulson@18886
   528
done
paulson@18886
   529
paulson@18886
   530
text{*Anticipated here from next subsection*}
paulson@18886
   531
lemma u_K4_imp_K2:
paulson@18886
   532
"\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>  \<in> set evs; evs \<in> kerbV\<rbrakk>
paulson@18886
   533
   \<Longrightarrow> \<exists>Ta. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   534
             Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
paulson@18886
   535
             \<in> set evs
paulson@18886
   536
          \<and> servKlife + Ts <= authKlife + Ta"
paulson@18886
   537
apply (erule rev_mp)
paulson@18886
   538
apply (erule kerbV.induct)
paulson@18886
   539
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   540
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
paulson@18886
   541
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
paulson@18886
   542
done
paulson@18886
   543
paulson@18886
   544
lemma servTicket_authentic_Kas:
paulson@18886
   545
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   546
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   547
         evs \<in> kerbV \<rbrakk>
paulson@18886
   548
  \<Longrightarrow> \<exists>authK Ta.
paulson@18886
   549
       Says Kas A
paulson@18886
   550
         \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   551
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
paulson@18886
   552
        \<in> set evs"
paulson@18886
   553
apply (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
paulson@18886
   554
done
paulson@18886
   555
paulson@18886
   556
lemma u_servTicket_authentic_Kas:
paulson@18886
   557
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   558
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   559
         evs \<in> kerbV \<rbrakk>
paulson@18886
   560
  \<Longrightarrow> \<exists>authK Ta.
paulson@18886
   561
       Says Kas A
paulson@18886
   562
         \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   563
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
paulson@18886
   564
        \<in> set evs \<and> 
paulson@18886
   565
      servKlife + Ts <= authKlife + Ta"
paulson@18886
   566
apply (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
paulson@18886
   567
done
paulson@18886
   568
paulson@18886
   569
lemma servTicket_authentic:
paulson@18886
   570
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   571
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   572
         evs \<in> kerbV \<rbrakk>
paulson@18886
   573
 \<Longrightarrow> \<exists>Ta authK.
paulson@18886
   574
     Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   575
                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>  \<in> set evs
paulson@18886
   576
     \<and> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   577
                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
paulson@18886
   578
       \<in> set evs"
paulson@18886
   579
apply (blast dest: servTicket_authentic_Tgs K4_imp_K2)
paulson@18886
   580
done
paulson@18886
   581
paulson@18886
   582
lemma u_servTicket_authentic:
paulson@18886
   583
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
   584
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
paulson@18886
   585
         evs \<in> kerbV \<rbrakk>
paulson@18886
   586
 \<Longrightarrow> \<exists>Ta authK.
paulson@18886
   587
     Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
   588
                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace> \<in> set evs
paulson@18886
   589
     \<and> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   590
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
paulson@18886
   591
       \<in> set evs
paulson@18886
   592
     \<and> servKlife + Ts <= authKlife + Ta"
paulson@18886
   593
apply (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
paulson@18886
   594
done
paulson@18886
   595
paulson@18886
   596
lemma u_NotexpiredSK_NotexpiredAK:
paulson@18886
   597
     "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
paulson@18886
   598
      \<Longrightarrow> \<not> expiredAK Ta evs"
paulson@18886
   599
apply (blast dest: leI le_trans dest: leD)
paulson@18886
   600
done
paulson@18886
   601
paulson@18886
   602
paulson@18886
   603
subsection{* Reliability: friendly agents send somthing if something else happened*}
paulson@18886
   604
paulson@18886
   605
lemma K3_imp_K2:
paulson@18886
   606
     "\<lbrakk> Says A Tgs
paulson@18886
   607
             \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
paulson@18886
   608
           \<in> set evs;
paulson@18886
   609
         A \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
   610
      \<Longrightarrow> \<exists>Ta AT. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, 
paulson@18886
   611
                               AT\<rbrace> \<in> set evs"
paulson@18886
   612
apply (erule rev_mp)
paulson@18886
   613
apply (erule kerbV.induct)
paulson@18886
   614
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   615
apply (frule_tac [5] Says_ticket_parts, simp_all, blast, blast)
paulson@18886
   616
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authK_authentic])
paulson@18886
   617
done
paulson@18886
   618
paulson@18886
   619
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
   620
lemma Key_unique_SesKey:
paulson@18886
   621
     "\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T\<rbrace>
paulson@18886
   622
           \<in> parts (spies evs);
paulson@18886
   623
         Crypt K' \<lbrace>Key SesKey,  Agent B', T'\<rbrace>
paulson@18886
   624
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
paulson@18886
   625
         evs \<in> kerbV \<rbrakk>
paulson@18886
   626
      \<Longrightarrow> K=K' \<and> B=B' \<and> T=T'"
paulson@18886
   627
apply (erule rev_mp)
paulson@18886
   628
apply (erule rev_mp)
paulson@18886
   629
apply (erule rev_mp)
paulson@18886
   630
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   631
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   632
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   633
txt{*Fake, K2, K4*}
paulson@18886
   634
apply (blast+)
paulson@18886
   635
done
paulson@18886
   636
paulson@18886
   637
text{*This inevitably has an existential form in version V*}
paulson@18886
   638
lemma Says_K5:
paulson@18886
   639
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
   640
         Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   641
                                     servTicket\<rbrace> \<in> set evs;
paulson@18886
   642
         Key servK \<notin> analz (spies evs);
paulson@18886
   643
         A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
   644
 \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   645
apply (erule rev_mp)
paulson@18886
   646
apply (erule rev_mp)
paulson@18886
   647
apply (erule rev_mp)
paulson@18886
   648
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   649
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   650
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   651
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
   652
apply blast
paulson@18886
   653
txt{*K3*}
paulson@18886
   654
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
paulson@18886
   655
txt{*K4*}
paulson@18886
   656
apply (force dest!: Crypt_imp_keysFor)
paulson@18886
   657
txt{*K5*}
paulson@18886
   658
apply (blast dest: Key_unique_SesKey)
paulson@18886
   659
done
paulson@18886
   660
paulson@18886
   661
text{*Anticipated here from next subsection*}
paulson@18886
   662
lemma unique_CryptKey:
paulson@18886
   663
     "\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
paulson@18886
   664
           \<in> parts (spies evs);
paulson@18886
   665
         Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
paulson@18886
   666
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
paulson@18886
   667
         evs \<in> kerbV \<rbrakk>
paulson@18886
   668
      \<Longrightarrow> A=A' & B=B' & T=T'"
paulson@18886
   669
apply (erule rev_mp)
paulson@18886
   670
apply (erule rev_mp)
paulson@18886
   671
apply (erule rev_mp)
paulson@18886
   672
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   673
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   674
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   675
txt{*Fake, K2, K4*}
paulson@18886
   676
apply (blast+)
paulson@18886
   677
done
paulson@18886
   678
paulson@18886
   679
lemma Says_K6:
paulson@18886
   680
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
   681
         Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
   682
                      servTicket\<rbrace> \<in> set evs;
paulson@18886
   683
         Key servK \<notin> analz (spies evs);
paulson@18886
   684
         A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
   685
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@18886
   686
apply (frule Says_Tgs_message_form, assumption, clarify)
paulson@18886
   687
apply (erule rev_mp)
paulson@18886
   688
apply (erule rev_mp)
paulson@18886
   689
apply (erule rev_mp)
paulson@18886
   690
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   691
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   692
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   693
apply (simp_all (no_asm_simp))
paulson@18886
   694
paulson@18886
   695
txt{*fake*}
paulson@18886
   696
apply blast
paulson@18886
   697
txt{*K4*}
paulson@18886
   698
apply (force dest!: Crypt_imp_keysFor, clarify)
paulson@18886
   699
txt{*K6*}
paulson@18886
   700
apply (drule  Says_imp_spies [THEN parts.Inj, THEN parts.Fst])
paulson@18886
   701
apply (drule  Says_imp_spies [THEN parts.Inj, THEN parts.Snd])
paulson@18886
   702
apply (blast dest!: unique_CryptKey)
paulson@18886
   703
done
paulson@18886
   704
paulson@18886
   705
text{*Needs a unicity theorem, hence moved here*}
paulson@18886
   706
lemma servK_authentic_ter:
paulson@18886
   707
 "\<lbrakk> Says Kas A
paulson@18886
   708
       \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, authTicket\<rbrace> \<in> set evs;
paulson@18886
   709
     Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
paulson@18886
   710
       \<in> parts (spies evs);
paulson@18886
   711
     Key authK \<notin> analz (spies evs);
paulson@18886
   712
     evs \<in> kerbV \<rbrakk>
paulson@18886
   713
 \<Longrightarrow> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, 
paulson@18886
   714
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace> \<rbrace>
paulson@18886
   715
       \<in> set evs"
paulson@18886
   716
apply (frule Says_Kas_message_form, assumption)
paulson@18886
   717
apply clarify
paulson@18886
   718
apply (erule rev_mp)
paulson@18886
   719
apply (erule rev_mp)
paulson@18886
   720
apply (erule rev_mp)
paulson@18886
   721
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   722
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   723
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
paulson@18886
   724
txt{*K2 and K4 remain*}
paulson@18886
   725
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
paulson@18886
   726
apply (blast dest!: unique_CryptKey)
paulson@18886
   727
done
paulson@18886
   728
paulson@18886
   729
paulson@18886
   730
subsection{*Unicity Theorems*}
paulson@18886
   731
paulson@18886
   732
text{* The session key, if secure, uniquely identifies the Ticket
paulson@18886
   733
   whether authTicket or servTicket. As a matter of fact, one can read
paulson@18886
   734
   also Tgs in the place of B.                                     *}
paulson@18886
   735
paulson@18886
   736
paulson@18886
   737
lemma unique_authKeys:
paulson@18886
   738
     "\<lbrakk> Says Kas A
paulson@18886
   739
              \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, X\<rbrace> \<in> set evs;
paulson@18886
   740
         Says Kas A'
paulson@18886
   741
              \<lbrace>Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta'\<rbrace>, X'\<rbrace> \<in> set evs;
paulson@18886
   742
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> A=A' \<and> Ka=Ka' \<and> Ta=Ta' \<and> X=X'"
paulson@18886
   743
apply (erule rev_mp)
paulson@18886
   744
apply (erule rev_mp)
paulson@18886
   745
apply (erule kerbV.induct)
paulson@18886
   746
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   747
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   748
apply blast+
paulson@18886
   749
done
paulson@18886
   750
paulson@18886
   751
text{* servK uniquely identifies the message from Tgs *}
paulson@18886
   752
lemma unique_servKeys:
paulson@18886
   753
     "\<lbrakk> Says Tgs A
paulson@18886
   754
              \<lbrace>Crypt K \<lbrace>Key servK, Agent B, Ts\<rbrace>, X\<rbrace> \<in> set evs;
paulson@18886
   755
         Says Tgs A'
paulson@18886
   756
              \<lbrace>Crypt K' \<lbrace>Key servK, Agent B', Ts'\<rbrace>, X'\<rbrace> \<in> set evs;
paulson@18886
   757
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> K=K' \<and> Ts=Ts' \<and> X=X'"
paulson@18886
   758
apply (erule rev_mp)
paulson@18886
   759
apply (erule rev_mp)
paulson@18886
   760
apply (erule kerbV.induct)
paulson@18886
   761
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   762
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   763
apply blast+
paulson@18886
   764
done
paulson@18886
   765
paulson@18886
   766
subsection{*Lemmas About the Predicate @{term AKcryptSK}*}
paulson@18886
   767
paulson@18886
   768
lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
paulson@18886
   769
apply (simp add: AKcryptSK_def)
paulson@18886
   770
done
paulson@18886
   771
paulson@18886
   772
lemma AKcryptSKI:
paulson@18886
   773
 "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>, X \<rbrace> \<in> set evs;
paulson@18886
   774
     evs \<in> kerbV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
paulson@18886
   775
apply (unfold AKcryptSK_def)
paulson@18886
   776
apply (blast dest: Says_Tgs_message_form)
paulson@18886
   777
done
paulson@18886
   778
paulson@18886
   779
lemma AKcryptSK_Says [simp]:
paulson@18886
   780
   "AKcryptSK authK servK (Says S A X # evs) =
paulson@18886
   781
     (S = Tgs \<and>
paulson@18886
   782
      (\<exists>B tt. X = \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>,
paulson@18886
   783
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, tt\<rbrace> \<rbrace>)
paulson@18886
   784
     | AKcryptSK authK servK evs)"
paulson@18886
   785
apply (unfold AKcryptSK_def)
paulson@18886
   786
apply (simp (no_asm))
paulson@18886
   787
apply blast
paulson@18886
   788
done
paulson@18886
   789
paulson@18886
   790
lemma AKcryptSK_Notes [simp]:
paulson@18886
   791
   "AKcryptSK authK servK (Notes A X # evs) =
paulson@18886
   792
      AKcryptSK authK servK evs"
paulson@18886
   793
apply (unfold AKcryptSK_def)
paulson@18886
   794
apply (simp (no_asm))
paulson@18886
   795
done
paulson@18886
   796
paulson@18886
   797
(*A fresh authK cannot be associated with any other
paulson@18886
   798
  (with respect to a given trace). *)
paulson@18886
   799
lemma Auth_fresh_not_AKcryptSK:
paulson@18886
   800
     "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbV \<rbrakk>
paulson@18886
   801
      \<Longrightarrow> \<not> AKcryptSK authK servK evs"
paulson@18886
   802
apply (unfold AKcryptSK_def)
paulson@18886
   803
apply (erule rev_mp)
paulson@18886
   804
apply (erule kerbV.induct)
paulson@18886
   805
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   806
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
paulson@18886
   807
done
paulson@18886
   808
paulson@18886
   809
(*A fresh servK cannot be associated with any other
paulson@18886
   810
  (with respect to a given trace). *)
paulson@18886
   811
lemma Serv_fresh_not_AKcryptSK:
paulson@18886
   812
 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
paulson@18886
   813
apply (unfold AKcryptSK_def, blast)
paulson@18886
   814
done
paulson@18886
   815
paulson@18886
   816
lemma authK_not_AKcryptSK:
paulson@18886
   817
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
paulson@18886
   818
           \<in> parts (spies evs);  evs \<in> kerbV \<rbrakk>
paulson@18886
   819
      \<Longrightarrow> \<not> AKcryptSK K authK evs"
paulson@18886
   820
apply (erule rev_mp)
paulson@18886
   821
apply (erule kerbV.induct)
paulson@18886
   822
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   823
apply (frule_tac [5] Says_ticket_parts, simp_all)
paulson@18886
   824
txt{*Fake*}
paulson@18886
   825
apply blast
paulson@18886
   826
txt{*K2: by freshness*}
paulson@18886
   827
apply (simp add: AKcryptSK_def)
paulson@18886
   828
apply blast
paulson@18886
   829
txt{*K4*}
paulson@18886
   830
apply blast
paulson@18886
   831
done
paulson@18886
   832
paulson@18886
   833
text{*A secure serverkey cannot have been used to encrypt others*}
paulson@18886
   834
lemma servK_not_AKcryptSK:
paulson@18886
   835
 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, tt\<rbrace> \<in> parts (spies evs);
paulson@18886
   836
     Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
paulson@18886
   837
     B \<noteq> Tgs;  evs \<in> kerbV \<rbrakk>
paulson@18886
   838
  \<Longrightarrow> \<not> AKcryptSK SK K evs"
paulson@18886
   839
apply (erule rev_mp)
paulson@18886
   840
apply (erule rev_mp)
paulson@18886
   841
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
   842
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   843
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
paulson@18886
   844
txt{*K4 splits into distinct subcases*}
paulson@18886
   845
apply auto
paulson@18886
   846
txt{*servK can't have been enclosed in two certificates*}
paulson@18886
   847
 prefer 2 apply (blast dest: unique_CryptKey)
paulson@18886
   848
txt{*servK is fresh and so could not have been used, by
paulson@18886
   849
   @{text new_keys_not_used}*}
paulson@18886
   850
apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
paulson@18886
   851
done
paulson@18886
   852
paulson@18886
   853
text{*Long term keys are not issued as servKeys*}
paulson@18886
   854
lemma shrK_not_AKcryptSK:
paulson@18886
   855
     "evs \<in> kerbV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
paulson@18886
   856
apply (unfold AKcryptSK_def)
paulson@18886
   857
apply (erule kerbV.induct)
paulson@18886
   858
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   859
apply (frule_tac [5] Says_ticket_parts, auto)
paulson@18886
   860
done
paulson@18886
   861
paulson@18886
   862
text{*The Tgs message associates servK with authK and therefore not with any
paulson@18886
   863
  other key authK.*}
paulson@18886
   864
lemma Says_Tgs_AKcryptSK:
paulson@18886
   865
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>, X \<rbrace>
paulson@18886
   866
           \<in> set evs;
paulson@18886
   867
         authK' \<noteq> authK;  evs \<in> kerbV \<rbrakk>
paulson@18886
   868
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs"
paulson@18886
   869
apply (unfold AKcryptSK_def)
paulson@18886
   870
apply (blast dest: unique_servKeys)
paulson@18886
   871
done
paulson@18886
   872
paulson@18886
   873
lemma AKcryptSK_not_AKcryptSK:
paulson@18886
   874
     "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbV \<rbrakk>
paulson@18886
   875
      \<Longrightarrow> \<not> AKcryptSK servK K evs"
paulson@18886
   876
apply (erule rev_mp)
paulson@18886
   877
apply (erule kerbV.induct)
paulson@18886
   878
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
   879
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
   880
apply (simp_all, safe)
paulson@18886
   881
txt{*K4 splits into subcases*}
paulson@18886
   882
(*apply simp_all*)
paulson@18886
   883
prefer 4 apply (blast dest!: authK_not_AKcryptSK)
paulson@18886
   884
txt{*servK is fresh and so could not have been used, by
paulson@18886
   885
   @{text new_keys_not_used}*}
paulson@18886
   886
 prefer 2 
paulson@18886
   887
 apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
paulson@18886
   888
txt{*Others by freshness*}
paulson@18886
   889
apply (blast+)
paulson@18886
   890
done
paulson@18886
   891
paulson@18886
   892
lemma not_different_AKcryptSK:
paulson@18886
   893
     "\<lbrakk> AKcryptSK authK servK evs;
paulson@18886
   894
        authK' \<noteq> authK;  evs \<in> kerbV \<rbrakk>
paulson@18886
   895
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
paulson@18886
   896
apply (simp add: AKcryptSK_def)
paulson@18886
   897
apply (blast dest: unique_servKeys Says_Tgs_message_form)
paulson@18886
   898
done
paulson@18886
   899
paulson@18886
   900
text{*The only session keys that can be found with the help of session keys are
paulson@18886
   901
  those sent by Tgs in step K4.  *}
paulson@18886
   902
paulson@18886
   903
text{*We take some pains to express the property
paulson@18886
   904
  as a logical equivalence so that the simplifier can apply it.*}
paulson@18886
   905
lemma Key_analz_image_Key_lemma:
paulson@18886
   906
     "P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
paulson@18886
   907
      \<Longrightarrow>
paulson@18886
   908
      P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
paulson@18886
   909
by (blast intro: analz_mono [THEN subsetD])
paulson@18886
   910
paulson@18886
   911
paulson@18886
   912
lemma AKcryptSK_analz_insert:
paulson@18886
   913
     "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbV \<rbrakk>
paulson@18886
   914
      \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
paulson@18886
   915
apply (simp add: AKcryptSK_def, clarify)
paulson@18886
   916
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
paulson@18886
   917
done
paulson@18886
   918
paulson@18886
   919
lemma authKeys_are_not_AKcryptSK:
paulson@18886
   920
     "\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbV \<rbrakk>
paulson@18886
   921
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
paulson@18886
   922
apply (simp add: authKeys_def AKcryptSK_def)
paulson@18886
   923
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
paulson@18886
   924
done
paulson@18886
   925
paulson@18886
   926
lemma not_authKeys_not_AKcryptSK:
paulson@18886
   927
     "\<lbrakk> K \<notin> authKeys evs;
paulson@18886
   928
         K \<notin> range shrK; evs \<in> kerbV \<rbrakk>
paulson@18886
   929
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
paulson@18886
   930
apply (simp add: AKcryptSK_def)
paulson@18886
   931
apply (blast dest: Says_Tgs_message_form)
paulson@18886
   932
done
paulson@18886
   933
paulson@18886
   934
paulson@18886
   935
subsection{*Secrecy Theorems*}
paulson@18886
   936
paulson@18886
   937
text{*For the Oops2 case of the next theorem*}
paulson@18886
   938
lemma Oops2_not_AKcryptSK:
paulson@18886
   939
     "\<lbrakk> evs \<in> kerbV;
paulson@18886
   940
         Says Tgs A \<lbrace>Crypt authK
paulson@18886
   941
                     \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
   942
           \<in> set evs \<rbrakk>
paulson@18886
   943
      \<Longrightarrow> \<not> AKcryptSK servK SK evs"
paulson@18886
   944
apply (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
paulson@18886
   945
done
paulson@18886
   946
   
paulson@18886
   947
text{* Big simplification law for keys SK that are not crypted by keys in KK
paulson@18886
   948
 It helps prove three, otherwise hard, facts about keys. These facts are
paulson@18886
   949
 exploited as simplification laws for analz, and also "limit the damage"
paulson@18886
   950
 in case of loss of a key to the spy. See ESORICS98.*}
paulson@18886
   951
lemma Key_analz_image_Key [rule_format (no_asm)]:
paulson@18886
   952
     "evs \<in> kerbV \<Longrightarrow>
paulson@18886
   953
      (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
paulson@18886
   954
       (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
paulson@18886
   955
       (Key SK \<in> analz (Key`KK Un (spies evs))) =
paulson@18886
   956
       (SK \<in> KK | Key SK \<in> analz (spies evs)))"
paulson@18886
   957
apply (erule kerbV.induct)
paulson@18886
   958
apply (frule_tac [10] Oops_range_spies2)
paulson@18886
   959
apply (frule_tac [9] Oops_range_spies1)
paulson@18886
   960
(*Used to apply Says_tgs_message form, which is no longer available. 
paulson@18886
   961
  Instead\<dots>*)
paulson@18886
   962
apply (drule_tac [7] Says_ticket_analz)
paulson@18886
   963
(*Used to apply Says_kas_message form, which is no longer available. 
paulson@18886
   964
  Instead\<dots>*)
paulson@18886
   965
apply (drule_tac [5] Says_ticket_analz)
paulson@18886
   966
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
paulson@18886
   967
txt{*Case-splits for Oops1 and message 5: the negated case simplifies using
paulson@18886
   968
 the induction hypothesis*}
paulson@18886
   969
apply (case_tac [9] "AKcryptSK authK SK evsO1")
paulson@18886
   970
apply (case_tac [7] "AKcryptSK servK SK evs5")
paulson@18886
   971
apply (simp_all del: image_insert
paulson@18886
   972
          add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
paulson@18886
   973
               Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
paulson@18886
   974
               Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
paulson@18886
   975
txt{*Fake*} 
paulson@18886
   976
apply spy_analz
paulson@18886
   977
txt{*K2*}
paulson@18886
   978
apply blast 
paulson@18886
   979
txt{*Cases K3 and K5 solved by the simplifier thanks to the ticket being in 
paulson@18886
   980
analz - this strategy is new wrt version IV*} 
paulson@18886
   981
txt{*K4*}
paulson@18886
   982
apply (blast dest!: authK_not_AKcryptSK)
paulson@18886
   983
txt{*Oops1*}
paulson@18886
   984
apply clarify
paulson@18886
   985
apply simp
paulson@18886
   986
apply (blast dest!: AKcryptSK_analz_insert)
paulson@18886
   987
done
paulson@18886
   988
paulson@18886
   989
text{* First simplification law for analz: no session keys encrypt
paulson@18886
   990
authentication keys or shared keys. *}
paulson@18886
   991
lemma analz_insert_freshK1:
paulson@18886
   992
     "\<lbrakk> evs \<in> kerbV;  K \<in> authKeys evs Un range shrK;
paulson@18886
   993
        SesKey \<notin> range shrK \<rbrakk>
paulson@18886
   994
      \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
paulson@18886
   995
          (K = SesKey | Key K \<in> analz (spies evs))"
paulson@18886
   996
apply (frule authKeys_are_not_AKcryptSK, assumption)
paulson@18886
   997
apply (simp del: image_insert
paulson@18886
   998
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@18886
   999
done
paulson@18886
  1000
paulson@18886
  1001
paulson@18886
  1002
text{* Second simplification law for analz: no service keys encrypt any other keys.*}
paulson@18886
  1003
lemma analz_insert_freshK2:
paulson@18886
  1004
     "\<lbrakk> evs \<in> kerbV;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
paulson@18886
  1005
        K \<in> symKeys \<rbrakk>
paulson@18886
  1006
      \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
paulson@18886
  1007
          (K = servK | Key K \<in> analz (spies evs))"
paulson@18886
  1008
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
paulson@18886
  1009
apply (simp del: image_insert
paulson@18886
  1010
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@18886
  1011
done
paulson@18886
  1012
paulson@18886
  1013
paulson@18886
  1014
text{* Third simplification law for analz: only one authentication key encrypts a certain service key.*}
paulson@18886
  1015
paulson@18886
  1016
lemma analz_insert_freshK3:
paulson@18886
  1017
 "\<lbrakk> AKcryptSK authK servK evs;
paulson@18886
  1018
    authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbV \<rbrakk>
paulson@18886
  1019
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
paulson@18886
  1020
                (servK = authK' | Key servK \<in> analz (spies evs))"
paulson@18886
  1021
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
paulson@18886
  1022
apply (simp del: image_insert
paulson@18886
  1023
            add: analz_image_freshK_simps add: Key_analz_image_Key)
paulson@18886
  1024
done
paulson@18886
  1025
paulson@18886
  1026
lemma analz_insert_freshK3_bis:
paulson@18886
  1027
 "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
  1028
        \<in> set evs; 
paulson@18886
  1029
     authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbV \<rbrakk>
paulson@18886
  1030
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
paulson@18886
  1031
                (servK = authK' | Key servK \<in> analz (spies evs))"
paulson@18886
  1032
apply (frule AKcryptSKI, assumption)
paulson@18886
  1033
apply (simp add: analz_insert_freshK3)
paulson@18886
  1034
done
paulson@18886
  1035
paulson@18886
  1036
text{*a weakness of the protocol*}
paulson@18886
  1037
lemma authK_compromises_servK:
paulson@18886
  1038
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
  1039
        \<in> set evs;  authK \<in> symKeys;
paulson@18886
  1040
         Key authK \<in> analz (spies evs); evs \<in> kerbV \<rbrakk>
paulson@18886
  1041
      \<Longrightarrow> Key servK \<in> analz (spies evs)"
paulson@18886
  1042
apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Fst])
paulson@18886
  1043
done
paulson@18886
  1044
paulson@18886
  1045
text{*lemma @{text servK_notin_authKeysD} not needed in version V*}
paulson@18886
  1046
paulson@18886
  1047
text{*If Spy sees the Authentication Key sent in msg K2, then
paulson@18886
  1048
    the Key has expired.*}
paulson@18886
  1049
lemma Confidentiality_Kas_lemma [rule_format]:
paulson@18886
  1050
     "\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1051
      \<Longrightarrow> Says Kas A
paulson@18886
  1052
               \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
paulson@18886
  1053
          Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>
paulson@18886
  1054
            \<in> set evs \<longrightarrow>
paulson@18886
  1055
          Key authK \<in> analz (spies evs) \<longrightarrow>
paulson@18886
  1056
          expiredAK Ta evs"
paulson@18886
  1057
apply (erule kerbV.induct)
paulson@18886
  1058
apply (frule_tac [10] Oops_range_spies2)
paulson@18886
  1059
apply (frule_tac [9] Oops_range_spies1)
paulson@18886
  1060
apply (frule_tac [7] Says_ticket_analz)
paulson@18886
  1061
apply (frule_tac [5] Says_ticket_analz)
paulson@18886
  1062
apply (safe del: impI conjI impCE)
paulson@18886
  1063
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@18886
  1064
txt{*Fake*}
paulson@18886
  1065
apply spy_analz
paulson@18886
  1066
txt{*K2*}
paulson@18886
  1067
apply blast
paulson@18886
  1068
txt{*K4*}
paulson@18886
  1069
apply blast
paulson@18886
  1070
txt{*Oops1*}
paulson@18886
  1071
apply (blast dest!: unique_authKeys intro: less_SucI)
paulson@18886
  1072
txt{*Oops2*}
paulson@18886
  1073
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
paulson@18886
  1074
done
paulson@18886
  1075
paulson@18886
  1076
lemma Confidentiality_Kas:
paulson@18886
  1077
     "\<lbrakk> Says Kas A
paulson@18886
  1078
              \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace>
paulson@18886
  1079
           \<in> set evs;
paulson@18886
  1080
        \<not> expiredAK Ta evs;
paulson@18886
  1081
        A \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1082
      \<Longrightarrow> Key authK \<notin> analz (spies evs)"
paulson@18886
  1083
apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
paulson@18886
  1084
done
paulson@18886
  1085
paulson@18886
  1086
text{*If Spy sees the Service Key sent in msg K4, then
paulson@18886
  1087
    the Key has expired.*}
paulson@18886
  1088
paulson@18886
  1089
lemma Confidentiality_lemma [rule_format]:
paulson@18886
  1090
     "\<lbrakk> Says Tgs A
paulson@18886
  1091
	    \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
paulson@18886
  1092
	      Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
paulson@18886
  1093
	   \<in> set evs;
paulson@18886
  1094
	Key authK \<notin> analz (spies evs);
paulson@18886
  1095
        servK \<in> symKeys;
paulson@18886
  1096
	A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1097
      \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
paulson@18886
  1098
	  expiredSK Ts evs"
paulson@18886
  1099
apply (erule rev_mp)
paulson@18886
  1100
apply (erule rev_mp)
paulson@18886
  1101
apply (erule kerbV.induct)
paulson@18886
  1102
apply (rule_tac [9] impI)+;
paulson@18886
  1103
  --{*The Oops1 case is unusual: must simplify
paulson@18886
  1104
    @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
paulson@18886
  1105
   @{text analz_mono_contra} weaken it to
paulson@18886
  1106
   @{term "Authkey \<notin> analz (spies evs)"},
paulson@18886
  1107
  for we then conclude @{term "authK \<noteq> authKa"}.*}
paulson@18886
  1108
apply analz_mono_contra
paulson@18886
  1109
apply (frule_tac [10] Oops_range_spies2)
paulson@18886
  1110
apply (frule_tac [9] Oops_range_spies1)
paulson@18886
  1111
apply (frule_tac [7] Says_ticket_analz)
paulson@18886
  1112
apply (frule_tac [5] Says_ticket_analz)
paulson@18886
  1113
apply (safe del: impI conjI impCE)
paulson@18886
  1114
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@18886
  1115
txt{*Fake*}
paulson@18886
  1116
apply spy_analz
paulson@18886
  1117
txt{*K2*}
paulson@18886
  1118
apply (blast intro: parts_insertI less_SucI)
paulson@18886
  1119
txt{*K4*}
paulson@18886
  1120
apply (blast dest: authTicket_authentic Confidentiality_Kas)
paulson@18886
  1121
txt{*Oops1*}
paulson@18886
  1122
 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
paulson@18886
  1123
txt{*Oops2*}
paulson@18886
  1124
  apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
paulson@18886
  1125
done
paulson@18886
  1126
paulson@18886
  1127
paulson@18886
  1128
text{* In the real world Tgs can't check wheter authK is secure! *}
paulson@18886
  1129
lemma Confidentiality_Tgs:
paulson@18886
  1130
     "\<lbrakk> Says Tgs A
paulson@18886
  1131
              \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
  1132
           \<in> set evs;
paulson@18886
  1133
         Key authK \<notin> analz (spies evs);
paulson@18886
  1134
         \<not> expiredSK Ts evs;
paulson@18886
  1135
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1136
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1137
apply (blast dest: Says_Tgs_message_form Confidentiality_lemma)
paulson@18886
  1138
done
paulson@18886
  1139
paulson@18886
  1140
text{* In the real world Tgs CAN check what Kas sends! *}
paulson@18886
  1141
lemma Confidentiality_Tgs_bis:
paulson@18886
  1142
     "\<lbrakk> Says Kas A
paulson@18886
  1143
               \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace>
paulson@18886
  1144
           \<in> set evs;
paulson@18886
  1145
         Says Tgs A
paulson@18886
  1146
              \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
  1147
           \<in> set evs;
paulson@18886
  1148
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1149
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1150
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1151
apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
paulson@18886
  1152
done
paulson@18886
  1153
paulson@18886
  1154
text{*Most general form*}
paulson@18886
  1155
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
paulson@18886
  1156
paulson@18886
  1157
lemmas Confidentiality_Auth_A = authK_authentic [THEN exE, THEN Confidentiality_Kas]
paulson@18886
  1158
paulson@18886
  1159
text{*Needs a confidentiality guarantee, hence moved here.
paulson@18886
  1160
      Authenticity of servK for A*}
paulson@18886
  1161
lemma servK_authentic_bis_r:
paulson@18886
  1162
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1163
           \<in> parts (spies evs);
paulson@18886
  1164
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1165
           \<in> parts (spies evs);
paulson@18886
  1166
         \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1167
 \<Longrightarrow> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, 
paulson@18886
  1168
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>
paulson@18886
  1169
       \<in> set evs"
paulson@18886
  1170
apply (frule authK_authentic, assumption, assumption)
paulson@18886
  1171
apply (erule exE)
paulson@18886
  1172
apply (drule Confidentiality_Auth_A, assumption, assumption)
paulson@18886
  1173
apply (blast, assumption, assumption, assumption)
paulson@18886
  1174
apply (blast dest:  servK_authentic_ter)
paulson@18886
  1175
done
paulson@18886
  1176
paulson@18886
  1177
lemma Confidentiality_Serv_A:
paulson@18886
  1178
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1179
           \<in> parts (spies evs);
paulson@18886
  1180
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1181
           \<in> parts (spies evs);
paulson@18886
  1182
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1183
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1184
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1185
apply (drule authK_authentic, assumption, assumption)
paulson@18886
  1186
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
paulson@18886
  1187
done
paulson@18886
  1188
paulson@18886
  1189
lemma Confidentiality_B:
paulson@18886
  1190
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1191
           \<in> parts (spies evs);
paulson@18886
  1192
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1193
           \<in> parts (spies evs);
paulson@18886
  1194
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1195
           \<in> parts (spies evs);
paulson@18886
  1196
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1197
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1198
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1199
apply (frule authK_authentic)
paulson@18886
  1200
apply (erule_tac [3] exE)
paulson@18886
  1201
apply (frule_tac [3] Confidentiality_Kas)
paulson@18886
  1202
apply (frule_tac [6] servTicket_authentic, auto)
paulson@18886
  1203
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
paulson@18886
  1204
done
paulson@18886
  1205
paulson@18886
  1206
lemma u_Confidentiality_B:
paulson@18886
  1207
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1208
           \<in> parts (spies evs);
paulson@18886
  1209
         \<not> expiredSK Ts evs;
paulson@18886
  1210
         A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1211
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
paulson@18886
  1212
apply (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
paulson@18886
  1213
done
paulson@18886
  1214
paulson@18886
  1215
paulson@18886
  1216
paulson@18886
  1217
subsection{*Parties authentication: each party verifies "the identity of
paulson@18886
  1218
       another party who generated some data" (quoted from Neuman and Ts'o).*}
paulson@18886
  1219
paulson@18886
  1220
text{*These guarantees don't assess whether two parties agree on
paulson@18886
  1221
      the same session key: sending a message containing a key
paulson@18886
  1222
      doesn't a priori state knowledge of the key.*}
paulson@18886
  1223
paulson@18886
  1224
paulson@18886
  1225
text{*These didn't have existential form in version IV*}
paulson@18886
  1226
lemma B_authenticates_A:
paulson@18886
  1227
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1228
        Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1229
           \<in> parts (spies evs);
paulson@18886
  1230
        Key servK \<notin> analz (spies evs);
paulson@18886
  1231
        A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1232
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
paulson@18886
  1233
apply (blast dest: servTicket_authentic_Tgs intro: Says_K5)
paulson@18886
  1234
done
paulson@18886
  1235
paulson@18886
  1236
text{*The second assumption tells B what kind of key servK is.*}
paulson@18886
  1237
lemma B_authenticates_A_r:
paulson@18886
  1238
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1239
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1240
           \<in> parts (spies evs);
paulson@18886
  1241
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1242
           \<in> parts (spies evs);
paulson@18886
  1243
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1244
           \<in> parts (spies evs);
paulson@18886
  1245
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
paulson@18886
  1246
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1247
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
paulson@18886
  1248
apply (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
paulson@18886
  1249
done
paulson@18886
  1250
paulson@18886
  1251
text{* @{text u_B_authenticates_A} would be the same as @{text B_authenticates_A} because the
paulson@18886
  1252
 servK confidentiality assumption is yet unrelaxed*}
paulson@18886
  1253
paulson@18886
  1254
lemma u_B_authenticates_A_r:
paulson@18886
  1255
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1256
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1257
           \<in> parts (spies evs);
paulson@18886
  1258
         \<not> expiredSK Ts evs;
paulson@18886
  1259
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1260
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
paulson@18886
  1261
apply (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
paulson@18886
  1262
done
paulson@18886
  1263
paulson@18886
  1264
lemma A_authenticates_B:
paulson@18886
  1265
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1266
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1267
           \<in> parts (spies evs);
paulson@18886
  1268
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1269
           \<in> parts (spies evs);
paulson@18886
  1270
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
paulson@18886
  1271
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1272
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@18886
  1273
apply (frule authK_authentic)
paulson@18886
  1274
apply assumption+
paulson@18886
  1275
apply (frule servK_authentic)
paulson@18886
  1276
prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form)
paulson@18886
  1277
apply assumption+
paulson@18886
  1278
apply clarify
paulson@18886
  1279
apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6)
paulson@18886
  1280
(*Single command proof: much slower!
paulson@18886
  1281
apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6)
paulson@18886
  1282
*)
paulson@18886
  1283
done
paulson@18886
  1284
paulson@18886
  1285
lemma A_authenticates_B_r:
paulson@18886
  1286
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1287
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1288
           \<in> parts (spies evs);
paulson@18886
  1289
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1290
           \<in> parts (spies evs);
paulson@18886
  1291
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
paulson@18886
  1292
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1293
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
paulson@18886
  1294
apply (frule authK_authentic)
paulson@18886
  1295
apply (erule_tac [3] exE)
paulson@18886
  1296
apply (frule_tac [3] Says_Kas_message_form)
paulson@18886
  1297
apply (frule_tac [4] Confidentiality_Kas)
paulson@18886
  1298
apply (frule_tac [7] servK_authentic)
paulson@18886
  1299
prefer 8 apply blast
paulson@18886
  1300
apply (erule_tac [9] exE)
paulson@18886
  1301
apply (erule_tac [9] exE)
paulson@18886
  1302
apply (frule_tac [9] K4_imp_K2)
paulson@18886
  1303
apply assumption+
paulson@18886
  1304
apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
paulson@18886
  1305
)
paulson@18886
  1306
done
paulson@18886
  1307
paulson@18886
  1308
paulson@18886
  1309
paulson@18886
  1310
paulson@18886
  1311
subsection{*Parties' knowledge of session keys. 
paulson@18886
  1312
       An agent knows a session key if he used it to issue a cipher. These
paulson@18886
  1313
       guarantees can be interpreted both in terms of key distribution
paulson@18886
  1314
       and of non-injective agreement on the session key.*}
paulson@18886
  1315
paulson@18886
  1316
lemma Kas_Issues_A:
paulson@18886
  1317
   "\<lbrakk> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>, authTicket\<rbrace> \<in> set evs;
paulson@18886
  1318
      evs \<in> kerbV \<rbrakk>
paulson@18886
  1319
  \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>)
paulson@18886
  1320
          on evs"
paulson@18886
  1321
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1322
apply (rule exI)
paulson@18886
  1323
apply (rule conjI, assumption)
paulson@18886
  1324
apply (simp (no_asm))
paulson@18886
  1325
apply (erule rev_mp)
paulson@18886
  1326
apply (erule kerbV.induct)
paulson@18886
  1327
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1328
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1329
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
  1330
txt{*K2*}
paulson@18886
  1331
apply (simp add: takeWhile_tail)
paulson@18886
  1332
apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
  1333
done
paulson@18886
  1334
paulson@18886
  1335
lemma A_authenticates_and_keydist_to_Kas:
paulson@18886
  1336
  "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace> \<in> parts (spies evs);
paulson@18886
  1337
     A \<notin> bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1338
 \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>) 
paulson@18886
  1339
          on evs"
paulson@18886
  1340
by (blast dest!: authK_authentic Kas_Issues_A)
paulson@18886
  1341
paulson@18886
  1342
lemma Tgs_Issues_A:
paulson@18886
  1343
    "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
paulson@18886
  1344
         \<in> set evs; 
paulson@18886
  1345
       Key authK \<notin> analz (spies evs);  evs \<in> kerbV \<rbrakk>
paulson@18886
  1346
  \<Longrightarrow> Tgs Issues A with 
paulson@18886
  1347
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>) on evs"
paulson@18886
  1348
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1349
apply (rule exI)
paulson@18886
  1350
apply (rule conjI, assumption)
paulson@18886
  1351
apply (simp (no_asm))
paulson@18886
  1352
apply (erule rev_mp)
paulson@18886
  1353
apply (erule rev_mp)
paulson@18886
  1354
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
  1355
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1356
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1357
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
  1358
apply (simp add: takeWhile_tail)
paulson@18886
  1359
(*Last two thms installed only to derive authK \<notin> range shrK*)
paulson@18886
  1360
apply (blast dest: servK_authentic parts_spies_takeWhile_mono [THEN subsetD]
paulson@18886
  1361
      parts_spies_evs_revD2 [THEN subsetD] authTicket_authentic 
paulson@18886
  1362
      Says_Kas_message_form)
paulson@18886
  1363
done
paulson@18886
  1364
paulson@18886
  1365
lemma A_authenticates_and_keydist_to_Tgs:
paulson@18886
  1366
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1367
           \<in> parts (spies evs);
paulson@18886
  1368
       Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1369
  \<Longrightarrow> \<exists>A. Tgs Issues A with 
paulson@18886
  1370
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>) on evs"
paulson@18886
  1371
by (blast dest: Tgs_Issues_A servK_authentic_bis)
paulson@18886
  1372
paulson@18886
  1373
lemma B_Issues_A:
paulson@18886
  1374
     "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
paulson@18886
  1375
         Key servK \<notin> analz (spies evs);
paulson@18886
  1376
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1377
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@18886
  1378
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1379
apply (rule exI)
paulson@18886
  1380
apply (rule conjI, assumption)
paulson@18886
  1381
apply (simp (no_asm))
paulson@18886
  1382
apply (erule rev_mp)
paulson@18886
  1383
apply (erule rev_mp)
paulson@18886
  1384
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
  1385
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@18886
  1386
apply blast
paulson@18886
  1387
txt{*K6 requires numerous lemmas*}
paulson@18886
  1388
apply (simp add: takeWhile_tail)
paulson@18886
  1389
apply (blast intro: Says_K6 dest: servTicket_authentic 
paulson@18886
  1390
        parts_spies_takeWhile_mono [THEN subsetD] 
paulson@18886
  1391
        parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
  1392
done
paulson@18886
  1393
paulson@18886
  1394
lemma A_authenticates_and_keydist_to_B:
paulson@18886
  1395
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
paulson@18886
  1396
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
paulson@18886
  1397
           \<in> parts (spies evs);
paulson@18886
  1398
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
paulson@18886
  1399
           \<in> parts (spies evs);
paulson@18886
  1400
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
paulson@18886
  1401
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
paulson@18886
  1402
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
paulson@18886
  1403
by (blast dest!: A_authenticates_B B_Issues_A)
paulson@18886
  1404
paulson@18886
  1405
paulson@18886
  1406
(*Must use \<le> rather than =, otherwise it cannot be proved inductively!*)
paulson@18886
  1407
(*This is too strong for version V but would hold for version IV if only B 
paulson@18886
  1408
  in K6 said a fresh timestamp.
paulson@18886
  1409
lemma honest_never_says_newer_timestamp:
paulson@18886
  1410
     "\<lbrakk> (CT evs) \<le> T ; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1411
     \<Longrightarrow> \<forall> A B. A \<noteq> Spy \<longrightarrow> Says A B X \<notin> set evs"
paulson@18886
  1412
apply (erule rev_mp)
paulson@18886
  1413
apply (erule kerbV.induct)
paulson@18886
  1414
apply (simp_all)
paulson@18886
  1415
apply force
paulson@18886
  1416
apply force
paulson@18886
  1417
txt{*clarifying case K3*}
paulson@18886
  1418
apply (rule impI)
paulson@18886
  1419
apply (rule impI)
paulson@18886
  1420
apply (frule Suc_leD)
paulson@18886
  1421
apply (clarify)
paulson@18886
  1422
txt{*cannot solve K3 or K5 because the spy might send CT evs as authTicket
paulson@18886
  1423
or servTicket, which the honest agent would forward*}
paulson@18886
  1424
prefer 2 apply force
paulson@18886
  1425
prefer 4 apply force
paulson@18886
  1426
prefer 4 apply force
paulson@18886
  1427
txt{*cannot solve K6 unless B updates the timestamp - rather than bouncing T3*}
paulson@18886
  1428
oops
paulson@18886
  1429
*)
paulson@18886
  1430
paulson@18886
  1431
paulson@18886
  1432
text{*But can prove a less general fact conerning only authenticators!*}
paulson@18886
  1433
lemma honest_never_says_newer_timestamp_in_auth:
paulson@18886
  1434
     "\<lbrakk> (CT evs) \<le> T; Number T \<in> parts {X}; A \<notin> bad; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1435
     \<Longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
paulson@18886
  1436
apply (erule rev_mp)
paulson@18886
  1437
apply (erule kerbV.induct)
paulson@18886
  1438
apply (simp_all)
paulson@18886
  1439
apply force+
paulson@18886
  1440
done
paulson@18886
  1441
paulson@18886
  1442
lemma honest_never_says_current_timestamp_in_auth:
paulson@18886
  1443
     "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; A \<notin> bad; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1444
     \<Longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
paulson@18886
  1445
apply (frule eq_imp_le)
paulson@18886
  1446
apply (blast dest: honest_never_says_newer_timestamp_in_auth)
paulson@18886
  1447
done
paulson@18886
  1448
paulson@18886
  1449
paulson@18886
  1450
paulson@18886
  1451
lemma A_Issues_B:
paulson@18886
  1452
     "\<lbrakk> Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1453
         Key servK \<notin> analz (spies evs);
paulson@18886
  1454
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1455
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@18886
  1456
apply (simp (no_asm) add: Issues_def)
paulson@18886
  1457
apply (rule exI)
paulson@18886
  1458
apply (rule conjI, assumption)
paulson@18886
  1459
apply (simp (no_asm))
paulson@18886
  1460
apply (erule rev_mp)
paulson@18886
  1461
apply (erule rev_mp)
paulson@18886
  1462
apply (erule kerbV.induct, analz_mono_contra)
paulson@18886
  1463
apply (frule_tac [7] Says_ticket_parts)
paulson@18886
  1464
apply (frule_tac [5] Says_ticket_parts)
paulson@18886
  1465
apply (simp_all (no_asm_simp))
paulson@18886
  1466
txt{*K5*}
paulson@18886
  1467
apply auto
paulson@18886
  1468
apply (simp add: takeWhile_tail)
paulson@18886
  1469
txt{*Level 15: case study necessary because the assumption doesn't state
paulson@18886
  1470
  the form of servTicket. The guarantee becomes stronger.*}
paulson@18886
  1471
prefer 2 apply (simp add: takeWhile_tail)
paulson@18886
  1472
(**This single command of version IV...
paulson@18886
  1473
apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
paulson@18886
  1474
                   K3_imp_K2 K4_trustworthy'
paulson@18886
  1475
                   parts_spies_takeWhile_mono [THEN subsetD]
paulson@18886
  1476
                   parts_spies_evs_revD2 [THEN subsetD]
paulson@18886
  1477
             intro: Says_Auth)
paulson@18886
  1478
...expands as follows - including extra exE because of new form of lemmas*)
paulson@18886
  1479
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
paulson@18886
  1480
apply (case_tac "Key authK \<in> analz (spies evs5)")
paulson@18886
  1481
apply (drule Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst, THEN analz_Decrypt', THEN analz.Fst], assumption, assumption, simp)
paulson@18886
  1482
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
paulson@18886
  1483
apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst])
paulson@18886
  1484
apply (frule servK_authentic_ter, blast, assumption+)
paulson@18886
  1485
apply (drule parts_spies_takeWhile_mono [THEN subsetD])
paulson@18886
  1486
apply (drule parts_spies_evs_revD2 [THEN subsetD])
paulson@18886
  1487
txt{* @{term Says_K5} closes the proof in version IV because it is clear which 
paulson@18886
  1488
servTicket an authenticator appears with in msg 5. In version V an authenticator can appear with any item that the spy could replace the servTicket with*}
paulson@18886
  1489
apply (frule Says_K5, blast, assumption, assumption, assumption, assumption, erule exE)
paulson@18886
  1490
txt{*We need to state that an honest agent wouldn't send the wrong timestamp
paulson@18886
  1491
within an authenticator, wathever it is paired with*}
paulson@18886
  1492
apply (simp add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1493
done
paulson@18886
  1494
paulson@18886
  1495
lemma B_authenticates_and_keydist_to_A:
paulson@18886
  1496
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
paulson@18886
  1497
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
paulson@18886
  1498
           \<in> parts (spies evs);
paulson@18886
  1499
         Key servK \<notin> analz (spies evs);
paulson@18886
  1500
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
paulson@18886
  1501
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
paulson@18886
  1502
by (blast dest: B_authenticates_A A_Issues_B)
paulson@18886
  1503
paulson@18886
  1504
paulson@18886
  1505
paulson@18886
  1506
subsection{*
paulson@18886
  1507
Novel guarantees, never studied before. Because honest agents always say
paulson@18886
  1508
the right timestamp in authenticators, we can prove unicity guarantees based 
paulson@18886
  1509
exactly on timestamps. Classical unicity guarantees are based on nonces.
paulson@18886
  1510
Of course assuming the agent to be different from the Spy, rather than not in 
paulson@18886
  1511
bad, would suffice below. Similar guarantees must also hold of
paulson@18886
  1512
Kerberos IV.*}
paulson@18886
  1513
paulson@18886
  1514
text{*Notice that an honest agent can send the same timestamp on two
paulson@18886
  1515
different traces of the same length, but not on the same trace!*}
paulson@18886
  1516
paulson@18886
  1517
lemma unique_timestamp_authenticator1:
paulson@18886
  1518
     "\<lbrakk> Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs;
paulson@18886
  1519
         Says A Kas' \<lbrace>Agent A, Agent Tgs', Number T1\<rbrace> \<in> set evs;
paulson@18886
  1520
         A \<notin>bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1521
  \<Longrightarrow> Kas=Kas' \<and> Tgs=Tgs'"
paulson@18886
  1522
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1523
apply (erule kerbV.induct)
paulson@18886
  1524
apply (simp_all, blast)
paulson@18886
  1525
apply auto
paulson@18886
  1526
apply (simp_all add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1527
done
paulson@18886
  1528
paulson@18886
  1529
lemma unique_timestamp_authenticator2:
paulson@18886
  1530
     "\<lbrakk> Says A Tgs \<lbrace>AT, Crypt AK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> \<in> set evs;
paulson@18886
  1531
     Says A Tgs' \<lbrace>AT', Crypt AK' \<lbrace>Agent A, Number T2\<rbrace>, Agent B'\<rbrace> \<in> set evs;
paulson@18886
  1532
         A \<notin>bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1533
  \<Longrightarrow> Tgs=Tgs' \<and> AT=AT' \<and> AK=AK' \<and> B=B'"
paulson@18886
  1534
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1535
apply (erule kerbV.induct)
paulson@18886
  1536
apply (simp_all, blast)
paulson@18886
  1537
apply auto
paulson@18886
  1538
apply (simp_all add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1539
done
paulson@18886
  1540
paulson@18886
  1541
lemma unique_timestamp_authenticator3:
paulson@18886
  1542
     "\<lbrakk> Says A B \<lbrace>ST, Crypt SK \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1543
         Says A B' \<lbrace>ST', Crypt SK' \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1544
         A \<notin>bad; evs \<in> kerbV \<rbrakk>
paulson@18886
  1545
  \<Longrightarrow> B=B' \<and> ST=ST' \<and> SK=SK'"
paulson@18886
  1546
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1547
apply (erule kerbV.induct)
paulson@18886
  1548
apply (simp_all, blast)
paulson@18886
  1549
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1550
done
paulson@18886
  1551
paulson@18886
  1552
text{*The second part of the message is treated as an authenticator by the last
paulson@18886
  1553
simplification step, even if it is not an authenticator!*}
paulson@18886
  1554
lemma unique_timestamp_authticket:
paulson@18886
  1555
     "\<lbrakk> Says Kas A \<lbrace>X, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key AK, T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1556
       Says Kas A' \<lbrace>X', Crypt (shrK Tgs') \<lbrace>Agent A', Agent Tgs', Key AK', T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1557
         evs \<in> kerbV \<rbrakk>
paulson@18886
  1558
  \<Longrightarrow> A=A' \<and> X=X' \<and> Tgs=Tgs' \<and> AK=AK'"
paulson@18886
  1559
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1560
apply (erule kerbV.induct)
paulson@18886
  1561
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1562
done
paulson@18886
  1563
paulson@18886
  1564
text{*The second part of the message is treated as an authenticator by the last
paulson@18886
  1565
simplification step, even if it is not an authenticator!*}
paulson@18886
  1566
lemma unique_timestamp_servticket:
paulson@18886
  1567
     "\<lbrakk> Says Tgs A \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1568
       Says Tgs A' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SK', T\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
  1569
         evs \<in> kerbV \<rbrakk>
paulson@18886
  1570
  \<Longrightarrow> A=A' \<and> X=X' \<and> B=B' \<and> SK=SK'"
paulson@18886
  1571
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1572
apply (erule kerbV.induct)
paulson@18886
  1573
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
paulson@18886
  1574
done
paulson@18886
  1575
paulson@18886
  1576
(*Uses assumption K6's assumption that B \<noteq> Kas, otherwise B should say
paulson@18886
  1577
fresh timestamp*)
paulson@18886
  1578
lemma Kas_never_says_newer_timestamp:
paulson@18886
  1579
     "\<lbrakk> (CT evs) \<le> T; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1580
     \<Longrightarrow> \<forall> A. Says Kas A X \<notin> set evs"
paulson@18886
  1581
apply (erule rev_mp)
paulson@18886
  1582
apply (erule kerbV.induct, auto)
paulson@18886
  1583
done
paulson@18886
  1584
paulson@18886
  1585
lemma Kas_never_says_current_timestamp:
paulson@18886
  1586
     "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1587
     \<Longrightarrow> \<forall> A. Says Kas A X \<notin> set evs"
paulson@18886
  1588
apply (frule eq_imp_le)
paulson@18886
  1589
apply (blast dest: Kas_never_says_newer_timestamp)
paulson@18886
  1590
done
paulson@18886
  1591
paulson@18886
  1592
lemma unique_timestamp_msg2:
paulson@18886
  1593
     "\<lbrakk> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key AK, Agent Tgs, T\<rbrace>, AT\<rbrace> \<in> set evs;
paulson@18886
  1594
     Says Kas A' \<lbrace>Crypt (shrK A') \<lbrace>Key AK', Agent Tgs', T\<rbrace>, AT'\<rbrace> \<in> set evs;
paulson@18886
  1595
         evs \<in> kerbV \<rbrakk>
paulson@18886
  1596
  \<Longrightarrow> A=A' \<and> AK=AK' \<and> Tgs=Tgs' \<and> AT=AT'"
paulson@18886
  1597
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1598
apply (erule kerbV.induct)
paulson@18886
  1599
apply (auto simp add: Kas_never_says_current_timestamp)
paulson@18886
  1600
done
paulson@18886
  1601
paulson@18886
  1602
(*Uses assumption K6's assumption that B \<noteq> Tgs, otherwise B should say
paulson@18886
  1603
fresh timestamp*)
paulson@18886
  1604
lemma Tgs_never_says_newer_timestamp:
paulson@18886
  1605
     "\<lbrakk> (CT evs) \<le> T; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1606
     \<Longrightarrow> \<forall> A. Says Tgs A X \<notin> set evs"
paulson@18886
  1607
apply (erule rev_mp)
paulson@18886
  1608
apply (erule kerbV.induct, auto)
paulson@18886
  1609
done
paulson@18886
  1610
paulson@18886
  1611
lemma Tgs_never_says_current_timestamp:
paulson@18886
  1612
     "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
paulson@18886
  1613
     \<Longrightarrow> \<forall> A. Says Tgs A X \<notin> set evs"
paulson@18886
  1614
apply (frule eq_imp_le)
paulson@18886
  1615
apply (blast dest: Tgs_never_says_newer_timestamp)
paulson@18886
  1616
done
paulson@18886
  1617
paulson@18886
  1618
paulson@18886
  1619
lemma unique_timestamp_msg4:
paulson@18886
  1620
     "\<lbrakk> Says Tgs A \<lbrace>Crypt (shrK A) \<lbrace>Key SK, Agent B, T\<rbrace>, ST\<rbrace> \<in> set evs;
paulson@18886
  1621
       Says Tgs A' \<lbrace>Crypt (shrK A') \<lbrace>Key SK', Agent B', T\<rbrace>, ST'\<rbrace> \<in> set evs;
paulson@18886
  1622
         evs \<in> kerbV \<rbrakk> 
paulson@18886
  1623
  \<Longrightarrow> A=A' \<and> SK=SK' \<and> B=B' \<and> ST=ST'"
paulson@18886
  1624
apply (erule rev_mp, erule rev_mp)
paulson@18886
  1625
apply (erule kerbV.induct)
paulson@18886
  1626
apply (auto simp add: Tgs_never_says_current_timestamp)
paulson@18886
  1627
done
paulson@18886
  1628
 
paulson@18886
  1629
end