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