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