src/HOL/Auth/Recur.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14207 f20fbb141673
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
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
paulson@14207
     9
theory Recur = Public:
paulson@2449
    10
paulson@13922
    11
text{*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@14207
    66
   RA1:  "[| evs1 \<in> 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@14207
    73
   RA2:  "[| evs2 \<in> 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@14207
    79
   RA3:  "[| evs3 \<in> 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@14207
    85
   RA4:  "[| evs4 \<in> 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@14207
   101
   Oops:  "[| evso \<in> 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@13922
   119
text{*Simplest case: Alice goes directly to the server*}
paulson@14200
   120
lemma "Key K \<notin> used [] 
paulson@14200
   121
       ==> \<exists>NA. \<exists>evs \<in> recur.
paulson@14200
   122
              Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
paulson@14200
   123
                    END|}  \<in> set evs"
paulson@11264
   124
apply (intro exI bexI)
paulson@11264
   125
apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
paulson@14200
   126
                             THEN recur.RA3 [OF _ _ respond.One]])
paulson@14200
   127
apply (possibility, simp add: used_Cons) 
paulson@11264
   128
done
paulson@11264
   129
paulson@11264
   130
paulson@13922
   131
text{*Case two: Alice, Bob and the server*}
paulson@14207
   132
lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
paulson@14207
   133
          Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
paulson@14207
   134
       ==> \<exists>NA. \<exists>evs \<in> recur.
paulson@11264
   135
        Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
paulson@11264
   136
                   END|}  \<in> set evs"
paulson@11264
   137
apply (intro exI bexI)
paulson@11270
   138
apply (rule_tac [2] 
paulson@14207
   139
          recur.Nil
paulson@14207
   140
           [THEN recur.RA1 [of _ NA], 
paulson@14207
   141
	    THEN recur.RA2 [of _ NB],
paulson@14207
   142
	    THEN recur.RA3 [OF _ _ respond.One 
paulson@14207
   143
                                     [THEN respond.Cons [of _ _ K _ K']]],
paulson@14207
   144
	    THEN recur.RA4], possibility)
paulson@14200
   145
apply (auto simp add: used_Cons)
paulson@11264
   146
done
paulson@11264
   147
paulson@14200
   148
(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
paulson@14200
   149
lemma "[| Key K \<notin> used []; Key K' \<notin> used [];  
paulson@14207
   150
          Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'';
paulson@14207
   151
          Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 
paulson@14207
   152
          NA < NB; NB < NC |]
paulson@14200
   153
       ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
paulson@14200
   154
             Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
paulson@14200
   155
                        END|}  \<in> set evs"
paulson@11270
   156
apply (intro exI bexI)
paulson@11270
   157
apply (rule_tac [2] 
paulson@11270
   158
          recur.Nil [THEN recur.RA1, 
paulson@11270
   159
                     THEN recur.RA2, THEN recur.RA2,
paulson@11270
   160
                     THEN recur.RA3 
paulson@11270
   161
                          [OF _ _ respond.One 
paulson@11270
   162
                                  [THEN respond.Cons, THEN respond.Cons]],
paulson@11270
   163
                     THEN recur.RA4, THEN recur.RA4])
paulson@11270
   164
apply (tactic "basic_possibility_tac")
paulson@14200
   165
apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
paulson@11270
   166
done
paulson@11264
   167
paulson@11264
   168
paulson@11264
   169
lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
paulson@11264
   170
by (erule respond.induct, simp_all)
paulson@11264
   171
paulson@11264
   172
lemma Key_in_parts_respond [rule_format]:
paulson@11264
   173
   "[| Key K \<in> parts {RB};  (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs"
paulson@11264
   174
apply (erule rev_mp, erule respond.induct)
paulson@11264
   175
apply (auto dest: Key_not_used respond_imp_not_used)
paulson@11264
   176
done
paulson@11264
   177
paulson@13922
   178
text{*Simple inductive reasoning about responses*}
paulson@11264
   179
lemma respond_imp_responses:
paulson@11264
   180
     "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
paulson@11264
   181
apply (erule respond.induct)
paulson@11264
   182
apply (blast intro!: respond_imp_not_used responses.intros)+
paulson@11264
   183
done
paulson@11264
   184
paulson@11264
   185
paulson@11264
   186
(** For reasoning about the encrypted portion of messages **)
paulson@11264
   187
paulson@11264
   188
lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
paulson@11264
   189
paulson@11264
   190
lemma RA4_analz_spies:
paulson@11264
   191
     "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
paulson@11264
   192
by blast
paulson@11264
   193
paulson@11264
   194
paulson@11264
   195
(*RA2_analz... and RA4_analz... let us treat those cases using the same
paulson@11264
   196
  argument as for the Fake case.  This is possible for most, but not all,
paulson@11264
   197
  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
paulson@11264
   198
  messages originate from the Spy. *)
paulson@11264
   199
paulson@11264
   200
lemmas RA2_parts_spies =  RA2_analz_spies [THEN analz_into_parts]
paulson@11264
   201
lemmas RA4_parts_spies =  RA4_analz_spies [THEN analz_into_parts]
paulson@11264
   202
paulson@11264
   203
paulson@11264
   204
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
paulson@11264
   205
    sends messages containing X! **)
paulson@11264
   206
paulson@11264
   207
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
paulson@11264
   208
paulson@11264
   209
lemma Spy_see_shrK [simp]:
paulson@11264
   210
     "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@13507
   211
apply (erule recur.induct, auto)
paulson@13922
   212
txt{*RA3.  It's ugly to call auto twice, but it seems necessary.*}
paulson@11264
   213
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
paulson@11264
   214
done
paulson@11264
   215
paulson@11264
   216
lemma Spy_analz_shrK [simp]:
paulson@11264
   217
     "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@11264
   218
by auto
paulson@11264
   219
paulson@11264
   220
lemma Spy_see_shrK_D [dest!]:
paulson@11264
   221
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> recur|] ==> A \<in> bad"
paulson@11264
   222
by (blast dest: Spy_see_shrK)
paulson@11264
   223
paulson@11264
   224
paulson@11264
   225
(*** Proofs involving analz ***)
paulson@11264
   226
paulson@11264
   227
(** Session keys are not used to encrypt other session keys **)
paulson@11264
   228
paulson@11264
   229
(*Version for "responses" relation.  Handles case RA3 in the theorem below.
paulson@11264
   230
  Note that it holds for *any* set H (not just "spies evs")
paulson@11264
   231
  satisfying the inductive hypothesis.*)
paulson@11264
   232
lemma resp_analz_image_freshK_lemma:
paulson@11264
   233
     "[| RB \<in> responses evs;
paulson@11264
   234
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   235
                   (Key K \<in> analz (Key`KK Un H)) =
paulson@11264
   236
                   (K \<in> KK | Key K \<in> analz H) |]
paulson@11264
   237
     ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   238
                   (Key K \<in> analz (insert RB (Key`KK Un H))) =
paulson@11264
   239
                   (K \<in> KK | Key K \<in> analz (insert RB H))"
paulson@14207
   240
apply (erule responses.induct)
paulson@14207
   241
apply (simp_all del: image_insert
paulson@14207
   242
	        add: analz_image_freshK_simps, auto)
paulson@14207
   243
done 
paulson@11264
   244
paulson@11264
   245
paulson@14207
   246
text{*Version for the protocol.  Proof is easy, thanks to the lemma.*}
paulson@11264
   247
lemma raw_analz_image_freshK:
paulson@11264
   248
 "evs \<in> recur ==>
paulson@11264
   249
   \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   250
          (Key K \<in> analz (Key`KK Un (spies evs))) =
paulson@11264
   251
          (K \<in> KK | Key K \<in> analz (spies evs))"
paulson@11264
   252
apply (erule recur.induct)
paulson@11264
   253
apply (drule_tac [4] RA2_analz_spies,
paulson@11281
   254
       drule_tac [5] respond_imp_responses,
paulson@13507
   255
       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
paulson@13922
   256
txt{*RA3*}
paulson@11264
   257
apply (simp_all add: resp_analz_image_freshK_lemma)
paulson@11264
   258
done
paulson@11264
   259
paulson@11264
   260
paulson@11264
   261
(*Instance of the lemma with H replaced by (spies evs):
paulson@11264
   262
   [| RB \<in> responses evs;  evs \<in> recur; |]
paulson@11264
   263
   ==> KK \<subseteq> - (range shrK) -->
paulson@11264
   264
       Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
paulson@11264
   265
       (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
paulson@11264
   266
*)
paulson@11264
   267
lemmas resp_analz_image_freshK =  
paulson@11264
   268
       resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
paulson@11264
   269
paulson@11264
   270
lemma analz_insert_freshK:
paulson@11264
   271
     "[| evs \<in> recur;  KAB \<notin> range shrK |]
wenzelm@11655
   272
      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@11264
   273
          (K = KAB | Key K \<in> analz (spies evs))"
paulson@11264
   274
by (simp del: image_insert
paulson@11264
   275
         add: analz_image_freshK_simps raw_analz_image_freshK)
paulson@11264
   276
paulson@11264
   277
paulson@13922
   278
text{*Everything that's hashed is already in past traffic. *}
paulson@11270
   279
lemma Hash_imp_body:
paulson@11270
   280
     "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
paulson@11264
   281
         evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
paulson@11264
   282
apply (erule rev_mp)
paulson@11264
   283
apply (erule recur.induct,
paulson@11281
   284
       drule_tac [6] RA4_parts_spies,
paulson@11281
   285
       drule_tac [5] respond_imp_responses,
paulson@11281
   286
       drule_tac [4] RA2_parts_spies)
paulson@13922
   287
txt{*RA3 requires a further induction*}
paulson@13507
   288
apply (erule_tac [5] responses.induct, simp_all)
paulson@13922
   289
txt{*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@13922
   309
txt{*Fake*}
paulson@11264
   310
apply blast
paulson@11264
   311
apply (erule_tac [3] responses.induct)
paulson@13922
   312
txt{*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@14207
   325
apply (erule responses.induct)
paulson@14207
   326
apply (simp_all del: image_insert
paulson@14207
   327
                add: analz_image_freshK_simps resp_analz_image_freshK, auto) 
paulson@14207
   328
done
paulson@11264
   329
paulson@11264
   330
paulson@11264
   331
lemma resp_analz_insert_lemma:
paulson@11264
   332
     "[| Key K \<in> analz (insert RB H);
paulson@11264
   333
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
paulson@11264
   334
                   (Key K \<in> analz (Key`KK Un H)) =
paulson@11264
   335
                   (K \<in> KK | Key K \<in> analz H);
paulson@11264
   336
         RB \<in> responses evs |]
paulson@11264
   337
     ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
paulson@11264
   338
apply (erule rev_mp, erule responses.induct)
paulson@11264
   339
apply (simp_all del: image_insert
paulson@11264
   340
             add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
paulson@13922
   341
txt{*Simplification using two distinct treatments of "image"*}
paulson@13507
   342
apply (simp add: parts_insert2, blast)
paulson@11264
   343
done
paulson@11264
   344
paulson@11264
   345
lemmas resp_analz_insert =
paulson@11264
   346
       resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
paulson@11264
   347
paulson@13922
   348
text{*The last key returned by respond indeed appears in a certificate*}
paulson@11264
   349
lemma respond_certificate:
paulson@11264
   350
     "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
paulson@11264
   351
      ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
paulson@11264
   352
apply (ind_cases "(X, RA, K) \<in> respond evs")
paulson@11264
   353
apply simp_all
paulson@11264
   354
done
paulson@11264
   355
paulson@11264
   356
(*This unicity proof differs from all the others in the HOL/Auth directory.
paulson@11264
   357
  The conclusion isn't quite unicity but duplicity, in that there are two
paulson@11264
   358
  possibilities.  Also, the presence of two different matching messages in
paulson@11264
   359
  the inductive step complicates the case analysis.  Unusually for such proofs,
paulson@11264
   360
  the quantifiers appear to be necessary.*)
paulson@11264
   361
lemma unique_lemma [rule_format]:
paulson@11264
   362
     "(PB,RB,KXY) \<in> respond evs ==>
paulson@11264
   363
      \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
paulson@11264
   364
      (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
paulson@11264
   365
      (A'=A & B'=B) | (A'=B & B'=A))"
paulson@11264
   366
apply (erule respond.induct)
paulson@11264
   367
apply (simp_all add: all_conj_distrib)
paulson@11264
   368
apply (blast dest: respond_certificate)
paulson@11264
   369
done
paulson@11264
   370
paulson@11264
   371
lemma unique_session_keys:
paulson@11264
   372
     "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
paulson@11264
   373
         Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
paulson@11264
   374
         (PB,RB,KXY) \<in> respond evs |]
paulson@11264
   375
      ==> (A'=A & B'=B) | (A'=B & B'=A)"
paulson@11264
   376
by (rule unique_lemma, auto)
paulson@11264
   377
paulson@11264
   378
paulson@11264
   379
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
paulson@11264
   380
    Does not in itself guarantee security: an attack could violate
paulson@11264
   381
    the premises, e.g. by having A=Spy **)
paulson@11264
   382
paulson@11264
   383
lemma respond_Spy_not_see_session_key [rule_format]:
paulson@11264
   384
     "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
paulson@11264
   385
      ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
paulson@11264
   386
          Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
paulson@11264
   387
          Key K \<notin> analz (insert RB (spies evs))"
paulson@11264
   388
apply (erule respond.induct)
paulson@11264
   389
apply (frule_tac [2] respond_imp_responses)
paulson@11264
   390
apply (frule_tac [2] respond_imp_not_used)
paulson@11264
   391
apply (simp_all del: image_insert
paulson@11264
   392
                add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
paulson@11264
   393
                     resp_analz_image_freshK parts_insert2)
paulson@13922
   394
txt{*Base case of respond*}
paulson@11264
   395
apply blast
paulson@13922
   396
txt{*Inductive step of respond*}
paulson@13507
   397
apply (intro allI conjI impI, simp_all)
paulson@13956
   398
txt{*by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
paulson@13956
   399
     if @{term "B \<in> bad"}*}   
paulson@13935
   400
apply (blast dest: unique_session_keys 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@13922
   416
txt{*Fake*}
paulson@11264
   417
apply spy_analz
paulson@13922
   418
txt{*RA2*}
paulson@11264
   419
apply blast 
paulson@13922
   420
txt{*RA3 remains*}
paulson@11264
   421
apply (simp add: parts_insert_spies)
paulson@13922
   422
txt{*Now we split into two cases.  A single blast could do it, but it would take
paulson@13922
   423
  a CPU minute.*}
paulson@11264
   424
apply (safe del: impCE)
paulson@13922
   425
txt{*RA3, case 1: use lemma previously proved by induction*}
paulson@11264
   426
apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
paulson@13922
   427
txt{*RA3, case 2: K is an old key*}
paulson@11264
   428
apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
paulson@13922
   429
txt{*RA4*}
paulson@11264
   430
apply blast 
paulson@11264
   431
done
paulson@11264
   432
paulson@11264
   433
(**** Authenticity properties for Agents ****)
paulson@11264
   434
paulson@13922
   435
text{*The response never contains Hashes*}
paulson@11264
   436
lemma Hash_in_parts_respond:
paulson@11264
   437
     "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
paulson@11264
   438
         (PB,RB,K) \<in> respond evs |]
paulson@11264
   439
      ==> Hash {|Key (shrK B), M|} \<in> parts H"
paulson@11264
   440
apply (erule rev_mp)
paulson@13507
   441
apply (erule respond_imp_responses [THEN responses.induct], auto)
paulson@11264
   442
done
paulson@11264
   443
paulson@13922
   444
text{*Only RA1 or RA2 can have caused such a part of a message to appear.
paulson@11264
   445
  This result is of no use to B, who cannot verify the Hash.  Moreover,
paulson@11264
   446
  it can say nothing about how recent A's message is.  It might later be
paulson@13922
   447
  used to prove B's presence to A at the run's conclusion.*}
paulson@11264
   448
lemma Hash_auth_sender [rule_format]:
paulson@11264
   449
     "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
paulson@11264
   450
         A \<notin> bad;  evs \<in> recur |]
paulson@11264
   451
      ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs"
paulson@11264
   452
apply (unfold HPair_def)
paulson@11264
   453
apply (erule rev_mp)
paulson@11264
   454
apply (erule recur.induct,
paulson@11281
   455
       drule_tac [6] RA4_parts_spies,
paulson@11281
   456
       drule_tac [4] RA2_parts_spies,
paulson@11264
   457
       simp_all)
paulson@13922
   458
txt{*Fake, RA3*}
paulson@11281
   459
apply (blast dest: Hash_in_parts_respond)+
paulson@11264
   460
done
paulson@11264
   461
paulson@11264
   462
(** These two results subsume (for all agents) the guarantees proved
paulson@11264
   463
    separately for A and B in the Otway-Rees protocol.
paulson@11264
   464
**)
paulson@11264
   465
paulson@11264
   466
paulson@13922
   467
text{*Certificates can only originate with the Server.*}
paulson@11264
   468
lemma Cert_imp_Server_msg:
paulson@11264
   469
     "[| Crypt (shrK A) Y \<in> parts (spies evs);
paulson@11264
   470
         A \<notin> bad;  evs \<in> recur |]
paulson@11264
   471
      ==> \<exists>C RC. Says Server C RC \<in> set evs  &
paulson@11264
   472
                   Crypt (shrK A) Y \<in> parts {RC}"
paulson@11264
   473
apply (erule rev_mp, erule recur.induct, simp_all)
paulson@13922
   474
txt{*Fake*}
paulson@11264
   475
apply blast
paulson@13922
   476
txt{*RA1*}
paulson@11264
   477
apply blast
paulson@13922
   478
txt{*RA2: it cannot be a new Nonce, contradiction.*}
paulson@11264
   479
apply blast
paulson@13922
   480
txt{*RA3.  Pity that the proof is so brittle: this step requires the rewriting,
paulson@13922
   481
       which however would break all other steps.*}
paulson@11264
   482
apply (simp add: parts_insert_spies, blast)
paulson@13922
   483
txt{*RA4*}
paulson@11264
   484
apply blast
paulson@11264
   485
done
paulson@11264
   486
paulson@11264
   487
end