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