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