src/HOL/Auth/Recur.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13922 75ae4244a596
permissions -rw-r--r--
tidying of Isar scripts
paulson@2449
     1
(*  Title:      HOL/Auth/Recur
paulson@2449
     2
    ID:         $Id$
paulson@2449
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2449
     4
    Copyright   1996  University of Cambridge
paulson@2449
     5
paulson@2449
     6
Inductive relation "recur" for the Recursive Authentication protocol.
paulson@2449
     7
*)
paulson@2449
     8
paulson@11264
     9
theory Recur = Shared:
paulson@2449
    10
paulson@5434
    11
(*End marker for message bundles*)
paulson@11264
    12
syntax        END :: "msg"
paulson@5434
    13
translations "END" == "Number 0"
paulson@5434
    14
paulson@2449
    15
(*Two session keys are distributed to each agent except for the initiator,
paulson@2516
    16
        who receives one.
paulson@2449
    17
  Perhaps the two session keys could be bundled into a single message.
paulson@2449
    18
*)
paulson@2516
    19
consts     respond :: "event list => (msg*msg*key)set"
paulson@2516
    20
inductive "respond evs" (*Server's response to the nested message*)
paulson@11264
    21
  intros
paulson@11264
    22
   One:  "Key KAB \<notin> used evs
paulson@11264
    23
          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
paulson@5434
    24
               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
paulson@11264
    25
               KAB)   \<in> respond evs"
paulson@2449
    26
paulson@2532
    27
    (*The most recent session key is passed up to the caller*)
paulson@11264
    28
   Cons: "[| (PA, RA, KAB) \<in> respond evs;
paulson@11264
    29
             Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
paulson@5434
    30
             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
paulson@11264
    31
          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
paulson@11264
    32
               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
paulson@2550
    33
                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@2516
    34
                 RA|},
paulson@2516
    35
               KBC)
paulson@11264
    36
              \<in> respond evs"
paulson@2449
    37
paulson@2449
    38
paulson@2481
    39
(*Induction over "respond" can be difficult due to the complexity of the
paulson@2532
    40
  subgoals.  Set "responses" captures the general form of certificates.
paulson@2449
    41
*)
paulson@11264
    42
consts     responses :: "event list => msg set"
paulson@11264
    43
inductive "responses evs"
paulson@11264
    44
  intros
paulson@2449
    45
    (*Server terminates lists*)
paulson@11264
    46
   Nil:  "END \<in> responses evs"
paulson@2449
    47
paulson@11264
    48
   Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
paulson@2516
    49
          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@11264
    50
                RA|}  \<in> responses evs"
paulson@2449
    51
paulson@2449
    52
paulson@11264
    53
consts     recur   :: "event list set"
paulson@3519
    54
inductive "recur"
paulson@11264
    55
  intros
paulson@2449
    56
         (*Initial trace is empty*)
paulson@11264
    57
   Nil:  "[] \<in> recur"
paulson@2449
    58
paulson@2532
    59
         (*The spy MAY say anything he CAN say.  Common to
paulson@2449
    60
           all similar protocols.*)
paulson@11264
    61
   Fake: "[| evsf \<in> recur;  X \<in> synth (analz (knows Spy evsf)) |]
paulson@11264
    62
          ==> Says Spy B X  # evsf \<in> recur"
paulson@2449
    63
paulson@2449
    64
         (*Alice initiates a protocol run.
paulson@5434
    65
           END is a placeholder to terminate the nesting.*)
paulson@11264
    66
   RA1:  "[| evs1: recur;  Nonce NA \<notin> used evs1 |]
paulson@5434
    67
          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
paulson@11264
    68
              # evs1 \<in> recur"
paulson@2449
    69
paulson@2449
    70
         (*Bob's response to Alice's message.  C might be the Server.
paulson@4552
    71
           We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
paulson@4552
    72
           it complicates proofs, so B may respond to any message at all!*)
paulson@11264
    73
   RA2:  "[| evs2: recur;  Nonce NB \<notin> used evs2;
paulson@11264
    74
             Says A' B PA \<in> set evs2 |]
paulson@2516
    75
          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
paulson@11264
    76
              # evs2 \<in> recur"
paulson@2449
    77
paulson@2550
    78
         (*The Server receives Bob's message and prepares a response.*)
paulson@11264
    79
   RA3:  "[| evs3: recur;  Says B' Server PB \<in> set evs3;
paulson@11264
    80
             (PB,RB,K) \<in> respond evs3 |]
paulson@11264
    81
          ==> Says Server B RB # evs3 \<in> recur"
paulson@2449
    82
paulson@2449
    83
         (*Bob receives the returned message and compares the Nonces with
paulson@2516
    84
           those in the message he previously sent the Server.*)
paulson@11264
    85
   RA4:  "[| evs4: recur;
paulson@11264
    86
             Says B  C {|XH, Agent B, Agent C, Nonce NB,
paulson@11264
    87
                         XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
paulson@11264
    88
             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
paulson@11264
    89
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@11264
    90
                         RA|} \<in> set evs4 |]
paulson@11264
    91
          ==> Says B A RA # evs4 \<in> recur"
paulson@5359
    92
paulson@5359
    93
   (*No "oops" message can easily be expressed.  Each session key is
paulson@11264
    94
     associated--in two separate messages--with two nonces.  This is
paulson@5359
    95
     one try, but it isn't that useful.  Re domino attack, note that
paulson@5359
    96
     Recur.ML proves that each session key is secure provided the two
paulson@5359
    97
     peers are, even if there are compromised agents elsewhere in
paulson@5359
    98
     the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
paulson@5359
    99
     etc.
paulson@5359
   100
paulson@11264
   101
   Oops:  "[| evso: recur;  Says Server B RB \<in> set evso;
paulson@11264
   102
	      RB \<in> responses evs';  Key K \<in> parts {RB} |]
paulson@11264
   103
           ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
paulson@5359
   104
  *)
paulson@11264
   105
paulson@11264
   106
paulson@11264
   107
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
paulson@11264
   108
declare parts.Body  [dest]
paulson@11264
   109
declare analz_into_parts [dest]
paulson@11264
   110
declare Fake_parts_insert_in_Un  [dest]
paulson@11264
   111
paulson@11264
   112
paulson@11264
   113
(** Possibility properties: traces that reach the end
paulson@11264
   114
        ONE theorem would be more elegant and faster!
paulson@11264
   115
        By induction on a list of agents (no repetitions)
paulson@11264
   116
**)
paulson@11264
   117
paulson@11264
   118
paulson@11264
   119
(*Simplest case: Alice goes directly to the server*)
paulson@11264
   120
lemma "\<exists>K NA. \<exists>evs \<in> recur.
paulson@11264
   121
   Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
paulson@11264
   122
                   END|}  \<in> set evs"
paulson@11264
   123
apply (intro exI bexI)
paulson@11264
   124
apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
paulson@13507
   125
                               THEN recur.RA3 [OF _ _ respond.One]], possibility)
paulson@11264
   126
done
paulson@11264
   127
paulson@11264
   128
paulson@11270
   129
(*Case two: Alice, Bob and the server*)
paulson@11264
   130
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
paulson@11264
   131
        Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
paulson@11264
   132
                   END|}  \<in> set evs"
paulson@13507
   133
apply (cut_tac Nonce_supply2 Key_supply2, clarify)
paulson@11264
   134
apply (intro exI bexI)
paulson@11270
   135
apply (rule_tac [2] 
paulson@11270
   136
          recur.Nil [THEN recur.RA1, 
paulson@11270
   137
                     THEN recur.RA2,
paulson@11270
   138
                     THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
paulson@11270
   139
                     THEN recur.RA4])
paulson@11270
   140
apply (tactic "basic_possibility_tac")
paulson@11270
   141
apply (tactic
paulson@11270
   142
      "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
paulson@11264
   143
done
paulson@11264
   144
paulson@11264
   145
(*Case three: Alice, Bob, Charlie and the server
paulson@11270
   146
  Rather slow (16 seconds) to run every time...
paulson@11270
   147
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
paulson@11264
   148
        Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
paulson@11264
   149
                   END|}  \<in> set evs"
paulson@13507
   150
apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
paulson@11270
   151
apply (intro exI bexI)
paulson@11270
   152
apply (rule_tac [2] 
paulson@11270
   153
          recur.Nil [THEN recur.RA1, 
paulson@11270
   154
                     THEN recur.RA2, THEN recur.RA2,
paulson@11270
   155
                     THEN recur.RA3 
paulson@11270
   156
                          [OF _ _ respond.One 
paulson@11270
   157
                                  [THEN respond.Cons, THEN respond.Cons]],
paulson@11270
   158
                     THEN recur.RA4, THEN recur.RA4])
paulson@11270
   159
apply (tactic "basic_possibility_tac")
paulson@11270
   160
apply (tactic
paulson@11270
   161
      "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
paulson@11270
   162
\                   eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
paulson@11270
   163
done
paulson@11270
   164
*)
paulson@11264
   165
paulson@11264
   166
(**** Inductive proofs about recur ****)
paulson@11264
   167
paulson@11264
   168
lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
paulson@11264
   169
by (erule respond.induct, simp_all)
paulson@11264
   170
paulson@11264
   171
lemma Key_in_parts_respond [rule_format]:
paulson@11264
   172
   "[| Key K \<in> parts {RB};  (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs"
paulson@11264
   173
apply (erule rev_mp, erule respond.induct)
paulson@11264
   174
apply (auto dest: Key_not_used respond_imp_not_used)
paulson@11264
   175
done
paulson@11264
   176
paulson@11264
   177
(*Simple inductive reasoning about responses*)
paulson@11264
   178
lemma respond_imp_responses:
paulson@11264
   179
     "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
paulson@11264
   180
apply (erule respond.induct)
paulson@11264
   181
apply (blast intro!: respond_imp_not_used responses.intros)+
paulson@11264
   182
done
paulson@11264
   183
paulson@11264
   184
paulson@11264
   185
(** For reasoning about the encrypted portion of messages **)
paulson@11264
   186
paulson@11264
   187
lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
paulson@11264
   188
paulson@11264
   189
lemma RA4_analz_spies:
paulson@11264
   190
     "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
paulson@11264
   191
by blast
paulson@11264
   192
paulson@11264
   193
paulson@11264
   194
(*RA2_analz... and RA4_analz... let us treat those cases using the same
paulson@11264
   195
  argument as for the Fake case.  This is possible for most, but not all,
paulson@11264
   196
  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
paulson@11264
   197
  messages originate from the Spy. *)
paulson@11264
   198
paulson@11264
   199
lemmas RA2_parts_spies =  RA2_analz_spies [THEN analz_into_parts]
paulson@11264
   200
lemmas RA4_parts_spies =  RA4_analz_spies [THEN analz_into_parts]
paulson@11264
   201
paulson@11264
   202
paulson@11264
   203
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
paulson@11264
   204
    sends messages containing X! **)
paulson@11264
   205
paulson@11264
   206
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
paulson@11264
   207
paulson@11264
   208
lemma Spy_see_shrK [simp]:
paulson@11264
   209
     "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@13507
   210
apply (erule recur.induct, auto)
paulson@11264
   211
(*RA3.  It's ugly to call auto twice, but it seems necessary.*)
paulson@11264
   212
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
paulson@11264
   213
done
paulson@11264
   214
paulson@11264
   215
lemma Spy_analz_shrK [simp]:
paulson@11264
   216
     "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@11264
   217
by auto
paulson@11264
   218
paulson@11264
   219
lemma Spy_see_shrK_D [dest!]:
paulson@11264
   220
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> recur|] ==> A \<in> bad"
paulson@11264
   221
by (blast dest: Spy_see_shrK)
paulson@11264
   222
paulson@11264
   223
paulson@11264
   224
(*** Proofs involving analz ***)
paulson@11264
   225
paulson@11264
   226
(** Session keys are not used to encrypt other session keys **)
paulson@11264
   227
paulson@11264
   228
(*Version for "responses" relation.  Handles case RA3 in the theorem below.
paulson@11264
   229
  Note that it holds for *any* set H (not just "spies evs")
paulson@11264
   230
  satisfying the inductive hypothesis.*)
paulson@11264
   231
lemma resp_analz_image_freshK_lemma:
paulson@11264
   232
     "[| RB \<in> responses evs;
paulson@11264
   233
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   234
                   (Key K \<in> analz (Key`KK Un H)) =
paulson@11264
   235
                   (K \<in> KK | Key K \<in> analz H) |]
paulson@11264
   236
     ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   237
                   (Key K \<in> analz (insert RB (Key`KK Un H))) =
paulson@11264
   238
                   (K \<in> KK | Key K \<in> analz (insert RB H))"
paulson@11264
   239
by (erule responses.induct,
paulson@11264
   240
    simp_all del: image_insert
paulson@11264
   241
	     add: analz_image_freshK_simps)
paulson@11264
   242
paulson@11264
   243
paulson@11264
   244
(*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
paulson@11264
   245
lemma raw_analz_image_freshK:
paulson@11264
   246
 "evs \<in> recur ==>
paulson@11264
   247
   \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   248
          (Key K \<in> analz (Key`KK Un (spies evs))) =
paulson@11264
   249
          (K \<in> KK | Key K \<in> analz (spies evs))"
paulson@11264
   250
apply (erule recur.induct)
paulson@11264
   251
apply (drule_tac [4] RA2_analz_spies,
paulson@11281
   252
       drule_tac [5] respond_imp_responses,
paulson@13507
   253
       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
paulson@11264
   254
(*RA3*)
paulson@11264
   255
apply (simp_all add: resp_analz_image_freshK_lemma)
paulson@11264
   256
done
paulson@11264
   257
paulson@11264
   258
paulson@11264
   259
(*Instance of the lemma with H replaced by (spies evs):
paulson@11264
   260
   [| RB \<in> responses evs;  evs \<in> recur; |]
paulson@11264
   261
   ==> KK \<subseteq> - (range shrK) -->
paulson@11264
   262
       Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
paulson@11264
   263
       (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
paulson@11264
   264
*)
paulson@11264
   265
lemmas resp_analz_image_freshK =  
paulson@11264
   266
       resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
paulson@11264
   267
paulson@11264
   268
lemma analz_insert_freshK:
paulson@11264
   269
     "[| evs \<in> recur;  KAB \<notin> range shrK |]
wenzelm@11655
   270
      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@11264
   271
          (K = KAB | Key K \<in> analz (spies evs))"
paulson@11264
   272
by (simp del: image_insert
paulson@11264
   273
         add: analz_image_freshK_simps raw_analz_image_freshK)
paulson@11264
   274
paulson@11264
   275
paulson@11264
   276
(*Everything that's hashed is already in past traffic. *)
paulson@11270
   277
lemma Hash_imp_body:
paulson@11270
   278
     "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
paulson@11264
   279
         evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
paulson@11264
   280
apply (erule rev_mp)
paulson@11264
   281
apply (erule recur.induct,
paulson@11281
   282
       drule_tac [6] RA4_parts_spies,
paulson@11281
   283
       drule_tac [5] respond_imp_responses,
paulson@11281
   284
       drule_tac [4] RA2_parts_spies)
paulson@11264
   285
(*RA3 requires a further induction*)
paulson@13507
   286
apply (erule_tac [5] responses.induct, simp_all)
paulson@11264
   287
(*Nil*)
paulson@11264
   288
apply force
paulson@11264
   289
(*Fake*)
paulson@11264
   290
apply (blast intro: parts_insertI)
paulson@11264
   291
done
paulson@11264
   292
paulson@11264
   293
paulson@11264
   294
(** The Nonce NA uniquely identifies A's message.
paulson@11264
   295
    This theorem applies to steps RA1 and RA2!
paulson@11264
   296
paulson@11264
   297
  Unicity is not used in other proofs but is desirable in its own right.
paulson@11264
   298
**)
paulson@11264
   299
paulson@11264
   300
lemma unique_NA:
paulson@11264
   301
  "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \<in> parts (spies evs);
paulson@11264
   302
      Hash {|Key(shrK A), Agent A, B',NA, P'|} \<in> parts (spies evs);
paulson@11264
   303
      evs \<in> recur;  A \<notin> bad |]
paulson@11264
   304
    ==> B=B' & P=P'"
paulson@11264
   305
apply (erule rev_mp, erule rev_mp)
paulson@11264
   306
apply (erule recur.induct,
paulson@11281
   307
       drule_tac [5] respond_imp_responses)
paulson@11264
   308
apply (force, simp_all)
paulson@11264
   309
(*Fake*)
paulson@11264
   310
apply blast
paulson@11264
   311
apply (erule_tac [3] responses.induct)
paulson@11264
   312
(*RA1,2: creation of new Nonce*)
paulson@11264
   313
apply simp_all
paulson@11264
   314
apply (blast dest!: Hash_imp_body)+
paulson@11264
   315
done
paulson@11264
   316
paulson@11264
   317
paulson@11264
   318
(*** Lemmas concerning the Server's response
paulson@11264
   319
      (relations "respond" and "responses")
paulson@11264
   320
***)
paulson@11264
   321
paulson@11264
   322
lemma shrK_in_analz_respond [simp]:
paulson@11264
   323
     "[| RB \<in> responses evs;  evs \<in> recur |]
paulson@11264
   324
  ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
paulson@11264
   325
by (erule responses.induct,
paulson@11264
   326
    simp_all del: image_insert
paulson@11264
   327
             add: analz_image_freshK_simps resp_analz_image_freshK)
paulson@11264
   328
paulson@11264
   329
paulson@11264
   330
lemma resp_analz_insert_lemma:
paulson@11264
   331
     "[| Key K \<in> analz (insert RB H);
paulson@11264
   332
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   333
                   (Key K \<in> analz (Key`KK Un H)) =
paulson@11264
   334
                   (K \<in> KK | Key K \<in> analz H);
paulson@11264
   335
         RB \<in> responses evs |]
paulson@11264
   336
     ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
paulson@11264
   337
apply (erule rev_mp, erule responses.induct)
paulson@11264
   338
apply (simp_all del: image_insert
paulson@11264
   339
             add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
paulson@11264
   340
(*Simplification using two distinct treatments of "image"*)
paulson@13507
   341
apply (simp add: parts_insert2, blast)
paulson@11264
   342
done
paulson@11264
   343
paulson@11264
   344
lemmas resp_analz_insert =
paulson@11264
   345
       resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
paulson@11264
   346
paulson@11264
   347
(*The last key returned by respond indeed appears in a certificate*)
paulson@11264
   348
lemma respond_certificate:
paulson@11264
   349
     "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
paulson@11264
   350
      ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
paulson@11264
   351
apply (ind_cases "(X, RA, K) \<in> respond evs")
paulson@11264
   352
apply simp_all
paulson@11264
   353
done
paulson@11264
   354
paulson@11264
   355
(*This unicity proof differs from all the others in the HOL/Auth directory.
paulson@11264
   356
  The conclusion isn't quite unicity but duplicity, in that there are two
paulson@11264
   357
  possibilities.  Also, the presence of two different matching messages in
paulson@11264
   358
  the inductive step complicates the case analysis.  Unusually for such proofs,
paulson@11264
   359
  the quantifiers appear to be necessary.*)
paulson@11264
   360
lemma unique_lemma [rule_format]:
paulson@11264
   361
     "(PB,RB,KXY) \<in> respond evs ==>
paulson@11264
   362
      \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
paulson@11264
   363
      (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
paulson@11264
   364
      (A'=A & B'=B) | (A'=B & B'=A))"
paulson@11264
   365
apply (erule respond.induct)
paulson@11264
   366
apply (simp_all add: all_conj_distrib)
paulson@11264
   367
apply (blast dest: respond_certificate)
paulson@11264
   368
done
paulson@11264
   369
paulson@11264
   370
lemma unique_session_keys:
paulson@11264
   371
     "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
paulson@11264
   372
         Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
paulson@11264
   373
         (PB,RB,KXY) \<in> respond evs |]
paulson@11264
   374
      ==> (A'=A & B'=B) | (A'=B & B'=A)"
paulson@11264
   375
by (rule unique_lemma, auto)
paulson@11264
   376
paulson@11264
   377
paulson@11264
   378
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
paulson@11264
   379
    Does not in itself guarantee security: an attack could violate
paulson@11264
   380
    the premises, e.g. by having A=Spy **)
paulson@11264
   381
paulson@11264
   382
lemma respond_Spy_not_see_session_key [rule_format]:
paulson@11264
   383
     "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
paulson@11264
   384
      ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
paulson@11264
   385
          Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
paulson@11264
   386
          Key K \<notin> analz (insert RB (spies evs))"
paulson@11264
   387
apply (erule respond.induct)
paulson@11264
   388
apply (frule_tac [2] respond_imp_responses)
paulson@11264
   389
apply (frule_tac [2] respond_imp_not_used)
paulson@11264
   390
apply (simp_all del: image_insert
paulson@11264
   391
                add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
paulson@11264
   392
                     resp_analz_image_freshK parts_insert2)
paulson@11264
   393
apply (simp_all add: ex_disj_distrib)
paulson@11264
   394
(** LEVEL 5 **)
paulson@11264
   395
(*Base case of respond*)
paulson@11264
   396
apply blast
paulson@11264
   397
(*Inductive step of respond*)
paulson@13507
   398
apply (intro allI conjI impI, simp_all)
paulson@11264
   399
(*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
paulson@11264
   400
apply (blast dest: unique_session_keys [OF _ respond_certificate])
paulson@11264
   401
apply (blast dest!: respond_certificate)
paulson@11264
   402
apply (blast dest!: resp_analz_insert)
paulson@11264
   403
done
paulson@11264
   404
paulson@11264
   405
paulson@11264
   406
lemma Spy_not_see_session_key:
paulson@11264
   407
     "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
paulson@11264
   408
         A \<notin> bad;  A' \<notin> bad;  evs \<in> recur |]
paulson@11264
   409
      ==> Key K \<notin> analz (spies evs)"
paulson@11264
   410
apply (erule rev_mp)
paulson@11264
   411
apply (erule recur.induct)
paulson@11264
   412
apply (drule_tac [4] RA2_analz_spies,
paulson@11264
   413
       frule_tac [5] respond_imp_responses,
paulson@11264
   414
       drule_tac [6] RA4_analz_spies,
paulson@11264
   415
       simp_all add: split_ifs analz_insert_eq analz_insert_freshK)
paulson@11264
   416
(*Base*)
paulson@11264
   417
apply force
paulson@11264
   418
(*Fake*)
paulson@11264
   419
apply spy_analz
paulson@11264
   420
(*RA2*)
paulson@11264
   421
apply blast 
paulson@11264
   422
(*RA3 remains*)
paulson@11264
   423
apply (simp add: parts_insert_spies)
paulson@11264
   424
(*Now we split into two cases.  A single blast could do it, but it would take
paulson@11264
   425
  a CPU minute.*)
paulson@11264
   426
apply (safe del: impCE)
paulson@11264
   427
(*RA3, case 1: use lemma previously proved by induction*)
paulson@11264
   428
apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
paulson@11264
   429
(*RA3, case 2: K is an old key*)
paulson@11264
   430
apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
paulson@11264
   431
(*RA4*)
paulson@11264
   432
apply blast 
paulson@11264
   433
done
paulson@11264
   434
paulson@11264
   435
(**** Authenticity properties for Agents ****)
paulson@11264
   436
paulson@11264
   437
(*The response never contains Hashes*)
paulson@11264
   438
lemma Hash_in_parts_respond:
paulson@11264
   439
     "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
paulson@11264
   440
         (PB,RB,K) \<in> respond evs |]
paulson@11264
   441
      ==> Hash {|Key (shrK B), M|} \<in> parts H"
paulson@11264
   442
apply (erule rev_mp)
paulson@13507
   443
apply (erule respond_imp_responses [THEN responses.induct], auto)
paulson@11264
   444
done
paulson@11264
   445
paulson@11264
   446
(*Only RA1 or RA2 can have caused such a part of a message to appear.
paulson@11264
   447
  This result is of no use to B, who cannot verify the Hash.  Moreover,
paulson@11264
   448
  it can say nothing about how recent A's message is.  It might later be
paulson@11264
   449
  used to prove B's presence to A at the run's conclusion.*)
paulson@11264
   450
lemma Hash_auth_sender [rule_format]:
paulson@11264
   451
     "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
paulson@11264
   452
         A \<notin> bad;  evs \<in> recur |]
paulson@11264
   453
      ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs"
paulson@11264
   454
apply (unfold HPair_def)
paulson@11264
   455
apply (erule rev_mp)
paulson@11264
   456
apply (erule recur.induct,
paulson@11281
   457
       drule_tac [6] RA4_parts_spies,
paulson@11281
   458
       drule_tac [4] RA2_parts_spies,
paulson@11264
   459
       simp_all)
paulson@11264
   460
(*Nil*)
paulson@11264
   461
apply force
paulson@11264
   462
(*Fake, RA3*)
paulson@11281
   463
apply (blast dest: Hash_in_parts_respond)+
paulson@11264
   464
done
paulson@11264
   465
paulson@11264
   466
(** These two results subsume (for all agents) the guarantees proved
paulson@11264
   467
    separately for A and B in the Otway-Rees protocol.
paulson@11264
   468
**)
paulson@11264
   469
paulson@11264
   470
paulson@11264
   471
(*Certificates can only originate with the Server.*)
paulson@11264
   472
lemma Cert_imp_Server_msg:
paulson@11264
   473
     "[| Crypt (shrK A) Y \<in> parts (spies evs);
paulson@11264
   474
         A \<notin> bad;  evs \<in> recur |]
paulson@11264
   475
      ==> \<exists>C RC. Says Server C RC \<in> set evs  &
paulson@11264
   476
                   Crypt (shrK A) Y \<in> parts {RC}"
paulson@11264
   477
apply (erule rev_mp, erule recur.induct, simp_all)
paulson@11264
   478
(*Nil*)
paulson@11264
   479
apply force
paulson@11264
   480
(*Fake*)
paulson@11264
   481
apply blast
paulson@11264
   482
(*RA1*)
paulson@11264
   483
apply blast
paulson@11264
   484
(*RA2: it cannot be a new Nonce, contradiction.*)
paulson@11264
   485
apply blast
paulson@11270
   486
(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
paulson@11270
   487
          which however would break all other steps.*)
paulson@11264
   488
apply (simp add: parts_insert_spies, blast)
paulson@11264
   489
(*RA4*)
paulson@11264
   490
apply blast
paulson@11264
   491
done
paulson@11264
   492
paulson@11264
   493
end