src/HOL/Auth/Recur.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 62343 24106dc44def
permissions -rw-r--r--
eliminated old defs;
wenzelm@37936
     1
(*  Title:      HOL/Auth/Recur.thy
paulson@2449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2449
     3
    Copyright   1996  University of Cambridge
paulson@2449
     4
*)
paulson@2449
     5
wenzelm@61830
     6
section\<open>The Otway-Bull Recursive Authentication Protocol\<close>
paulson@14207
     7
haftmann@16417
     8
theory Recur imports Public begin
paulson@2449
     9
wenzelm@61830
    10
text\<open>End marker for message bundles\<close>
wenzelm@20768
    11
abbreviation
wenzelm@21404
    12
  END :: "msg" where
wenzelm@20768
    13
  "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
*)
berghofe@23746
    19
inductive_set (*Server's response to the nested message*)
berghofe@23746
    20
  respond :: "event list => (msg*msg*key)set"
berghofe@23746
    21
  for evs :: "event list"
berghofe@23746
    22
  where
paulson@11264
    23
   One:  "Key KAB \<notin> used evs
wenzelm@61956
    24
          ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>,
wenzelm@61956
    25
               \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>,
paulson@11264
    26
               KAB)   \<in> respond evs"
paulson@2449
    27
paulson@2532
    28
    (*The most recent session key is passed up to the caller*)
berghofe@23746
    29
 | Cons: "[| (PA, RA, KAB) \<in> respond evs;
paulson@11264
    30
             Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
wenzelm@61956
    31
             PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |]
wenzelm@61956
    32
          ==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>,
wenzelm@61956
    33
               \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
wenzelm@61956
    34
                 Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
wenzelm@61956
    35
                 RA\<rbrace>,
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
*)
berghofe@23746
    43
inductive_set
berghofe@23746
    44
  responses :: "event list => msg set"
berghofe@23746
    45
  for evs :: "event list"
berghofe@23746
    46
  where
paulson@2449
    47
    (*Server terminates lists*)
paulson@11264
    48
   Nil:  "END \<in> responses evs"
paulson@2449
    49
berghofe@23746
    50
 | Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
wenzelm@61956
    51
          ==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
wenzelm@61956
    52
                RA\<rbrace>  \<in> responses evs"
paulson@2449
    53
paulson@2449
    54
berghofe@23746
    55
inductive_set recur :: "event list set"
berghofe@23746
    56
  where
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.*)
berghofe@23746
    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.*)
berghofe@23746
    67
 | RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
wenzelm@61956
    68
          ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>)
paulson@11264
    69
              # evs1 \<in> recur"
paulson@2449
    70
paulson@2449
    71
         (*Bob's response to Alice's message.  C might be the Server.
wenzelm@61956
    72
           We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because
paulson@4552
    73
           it complicates proofs, so B may respond to any message at all!*)
berghofe@23746
    74
 | RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
paulson@11264
    75
             Says A' B PA \<in> set evs2 |]
wenzelm@61956
    76
          ==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>)
paulson@11264
    77
              # evs2 \<in> recur"
paulson@2449
    78
paulson@2550
    79
         (*The Server receives Bob's message and prepares a response.*)
berghofe@23746
    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.*)
berghofe@23746
    86
 | RA4:  "[| evs4 \<in> recur;
wenzelm@61956
    87
             Says B  C \<lbrace>XH, Agent B, Agent C, Nonce NB,
wenzelm@61956
    88
                         XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4;
wenzelm@61956
    89
             Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
wenzelm@61956
    90
                         Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
wenzelm@61956
    91
                         RA\<rbrace> \<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
wenzelm@24122
    97
     Recur.thy 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;
wenzelm@32960
   103
              RB \<in> responses evs';  Key K \<in> parts {RB} |]
wenzelm@61956
   104
           ==> Notes Spy \<lbrace>Key K, RB\<rbrace> # 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
wenzelm@61830
   120
text\<open>Simplest case: Alice goes directly to the server\<close>
paulson@14200
   121
lemma "Key K \<notin> used [] 
paulson@14200
   122
       ==> \<exists>NA. \<exists>evs \<in> recur.
wenzelm@61956
   123
              Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>,
wenzelm@61956
   124
                    END\<rbrace>  \<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
wenzelm@61830
   132
text\<open>Case two: Alice, Bob and the server\<close>
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.
wenzelm@61956
   136
        Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
wenzelm@61956
   137
                   END\<rbrace>  \<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], 
wenzelm@32960
   142
            THEN recur.RA2 [of _ NB],
wenzelm@32960
   143
            THEN recur.RA3 [OF _ _ respond.One 
paulson@14207
   144
                                     [THEN respond.Cons [of _ _ K _ K']]],
wenzelm@32960
   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.
wenzelm@61956
   155
             Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
wenzelm@61956
   156
                        END\<rbrace>  \<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])
wenzelm@23894
   165
apply basic_possibility
wenzelm@58963
   166
apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [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
wenzelm@61830
   179
text\<open>Simple inductive reasoning about responses\<close>
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:
wenzelm@61956
   192
     "Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<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)
wenzelm@61830
   213
txt\<open>RA3.  It's ugly to call auto twice, but it seems necessary.\<close>
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
wenzelm@32960
   243
                add: analz_image_freshK_simps, auto)
paulson@14207
   244
done 
paulson@11264
   245
paulson@11264
   246
wenzelm@61830
   247
text\<open>Version for the protocol.  Proof is easy, thanks to the lemma.\<close>
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)
wenzelm@61830
   257
txt\<open>RA3\<close>
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
wenzelm@61830
   279
text\<open>Everything that's hashed is already in past traffic.\<close>
paulson@11270
   280
lemma Hash_imp_body:
wenzelm@61956
   281
     "[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<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)
wenzelm@61830
   288
txt\<open>RA3 requires a further induction\<close>
paulson@13507
   289
apply (erule_tac [5] responses.induct, simp_all)
wenzelm@61830
   290
txt\<open>Fake\<close>
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:
wenzelm@61956
   302
  "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs);
wenzelm@61956
   303
      Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<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)
wenzelm@61830
   310
txt\<open>Fake\<close>
paulson@11264
   311
apply blast
paulson@11264
   312
apply (erule_tac [3] responses.induct)
wenzelm@61830
   313
txt\<open>RA1,2: creation of new Nonce\<close>
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)
wenzelm@61830
   342
txt\<open>Simplification using two distinct treatments of "image"\<close>
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
wenzelm@61830
   349
text\<open>The last key returned by respond indeed appears in a certificate\<close>
paulson@11264
   350
lemma respond_certificate:
wenzelm@61956
   351
     "(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs
wenzelm@61956
   352
      ==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}"
berghofe@23746
   353
apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, 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 ==>
wenzelm@61956
   364
      \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} -->
wenzelm@61956
   365
      (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<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:
wenzelm@61956
   373
     "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB};
wenzelm@61956
   374
         Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<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 -->
wenzelm@61956
   387
          Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<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)
wenzelm@61830
   395
txt\<open>Base case of respond\<close>
paulson@11264
   396
apply blast
wenzelm@61830
   397
txt\<open>Inductive step of respond\<close>
paulson@13507
   398
apply (intro allI conjI impI, simp_all)
wenzelm@61830
   399
txt\<open>by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
wenzelm@61830
   400
     if @{term "B \<in> bad"}\<close>   
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:
wenzelm@61956
   408
     "[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<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)
wenzelm@61830
   417
txt\<open>Fake\<close>
paulson@11264
   418
apply spy_analz
wenzelm@61830
   419
txt\<open>RA2\<close>
paulson@11264
   420
apply blast 
wenzelm@61830
   421
txt\<open>RA3\<close>
paulson@11264
   422
apply (simp add: parts_insert_spies)
paulson@32404
   423
apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert 
paulson@32404
   424
             respond_Spy_not_see_session_key usedI)
wenzelm@61830
   425
txt\<open>RA4\<close>
paulson@11264
   426
apply blast 
paulson@11264
   427
done
paulson@11264
   428
paulson@11264
   429
(**** Authenticity properties for Agents ****)
paulson@11264
   430
wenzelm@61830
   431
text\<open>The response never contains Hashes\<close>
paulson@11264
   432
lemma Hash_in_parts_respond:
wenzelm@61956
   433
     "[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H);
paulson@11264
   434
         (PB,RB,K) \<in> respond evs |]
wenzelm@61956
   435
      ==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H"
paulson@11264
   436
apply (erule rev_mp)
paulson@13507
   437
apply (erule respond_imp_responses [THEN responses.induct], auto)
paulson@11264
   438
done
paulson@11264
   439
wenzelm@61830
   440
text\<open>Only RA1 or RA2 can have caused such a part of a message to appear.
paulson@11264
   441
  This result is of no use to B, who cannot verify the Hash.  Moreover,
paulson@11264
   442
  it can say nothing about how recent A's message is.  It might later be
wenzelm@61830
   443
  used to prove B's presence to A at the run's conclusion.\<close>
paulson@11264
   444
lemma Hash_auth_sender [rule_format]:
wenzelm@61956
   445
     "[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs);
paulson@11264
   446
         A \<notin> bad;  evs \<in> recur |]
wenzelm@61956
   447
      ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs"
paulson@11264
   448
apply (unfold HPair_def)
paulson@11264
   449
apply (erule rev_mp)
paulson@11264
   450
apply (erule recur.induct,
paulson@11281
   451
       drule_tac [6] RA4_parts_spies,
paulson@11281
   452
       drule_tac [4] RA2_parts_spies,
paulson@11264
   453
       simp_all)
wenzelm@61830
   454
txt\<open>Fake, RA3\<close>
paulson@11281
   455
apply (blast dest: Hash_in_parts_respond)+
paulson@11264
   456
done
paulson@11264
   457
paulson@11264
   458
(** These two results subsume (for all agents) the guarantees proved
paulson@11264
   459
    separately for A and B in the Otway-Rees protocol.
paulson@11264
   460
**)
paulson@11264
   461
paulson@11264
   462
wenzelm@61830
   463
text\<open>Certificates can only originate with the Server.\<close>
paulson@11264
   464
lemma Cert_imp_Server_msg:
paulson@11264
   465
     "[| Crypt (shrK A) Y \<in> parts (spies evs);
paulson@11264
   466
         A \<notin> bad;  evs \<in> recur |]
paulson@11264
   467
      ==> \<exists>C RC. Says Server C RC \<in> set evs  &
paulson@11264
   468
                   Crypt (shrK A) Y \<in> parts {RC}"
paulson@11264
   469
apply (erule rev_mp, erule recur.induct, simp_all)
wenzelm@61830
   470
txt\<open>Fake\<close>
paulson@11264
   471
apply blast
wenzelm@61830
   472
txt\<open>RA1\<close>
paulson@11264
   473
apply blast
wenzelm@61830
   474
txt\<open>RA2: it cannot be a new Nonce, contradiction.\<close>
paulson@11264
   475
apply blast
wenzelm@61830
   476
txt\<open>RA3.  Pity that the proof is so brittle: this step requires the rewriting,
wenzelm@61830
   477
       which however would break all other steps.\<close>
paulson@11264
   478
apply (simp add: parts_insert_spies, blast)
wenzelm@61830
   479
txt\<open>RA4\<close>
paulson@11264
   480
apply blast
paulson@11264
   481
done
paulson@11264
   482
paulson@11264
   483
end