src/HOL/Auth/OtwayReesBella.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 51798 ad3a241def73
child 59498 50b60f501b05
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@37936
     1
(*  Title:      HOL/Auth/OtwayReesBella.thy
paulson@18886
     2
    Author:     Giampaolo Bella, Catania University
paulson@18886
     3
*)
paulson@18886
     4
wenzelm@58889
     5
section{*Bella's version of the Otway-Rees protocol*}
paulson@18886
     6
paulson@18886
     7
paulson@18886
     8
theory OtwayReesBella imports Public begin
paulson@18886
     9
paulson@18886
    10
text{*Bella's modifications to a version of the Otway-Rees protocol taken from
paulson@18886
    11
the BAN paper only concern message 7. The updated protocol makes the goal of
paulson@18886
    12
key distribution of the session key available to A. Investigating the
paulson@18886
    13
principle of Goal Availability undermines the BAN claim about the original
paulson@18886
    14
protocol, that "this protocol does not make use of Kab as an encryption key,
paulson@18886
    15
so neither principal can know whether the key is known to the other". The
paulson@18886
    16
updated protocol makes no use of the session key to encrypt but informs A that
paulson@18886
    17
B knows it.*}
paulson@18886
    18
berghofe@23746
    19
inductive_set orb :: "event list set"
berghofe@23746
    20
 where
paulson@18886
    21
paulson@18886
    22
  Nil:  "[]\<in> orb"
paulson@18886
    23
berghofe@23746
    24
| Fake: "\<lbrakk>evsa\<in> orb;  X\<in> synth (analz (knows Spy evsa))\<rbrakk>
wenzelm@32960
    25
         \<Longrightarrow> Says Spy B X  # evsa \<in> orb"
paulson@18886
    26
berghofe@23746
    27
| Reception: "\<lbrakk>evsr\<in> orb;  Says A B X \<in> set evsr\<rbrakk>
wenzelm@32960
    28
              \<Longrightarrow> Gets B X # evsr \<in> orb"
paulson@18886
    29
berghofe@23746
    30
| OR1:  "\<lbrakk>evs1\<in> orb;  Nonce NA \<notin> used evs1\<rbrakk>
wenzelm@32960
    31
         \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, 
wenzelm@32960
    32
                   Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
wenzelm@32960
    33
               # evs1 \<in> orb"
paulson@18886
    34
berghofe@23746
    35
| OR2:  "\<lbrakk>evs2\<in> orb;  Nonce NB \<notin> used evs2;
wenzelm@32960
    36
           Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk>
wenzelm@32960
    37
        \<Longrightarrow> Says B Server 
wenzelm@32960
    38
                \<lbrace>Nonce M, Agent A, Agent B, X, 
wenzelm@32960
    39
           Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
wenzelm@32960
    40
               # evs2 \<in> orb"
paulson@18886
    41
berghofe@23746
    42
| OR3:  "\<lbrakk>evs3\<in> orb;  Key KAB \<notin> used evs3;
wenzelm@32960
    43
          Gets Server 
wenzelm@32960
    44
             \<lbrace>Nonce M, Agent A, Agent B, 
wenzelm@32960
    45
               Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, 
wenzelm@32960
    46
               Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
wenzelm@32960
    47
          \<in> set evs3\<rbrakk>
wenzelm@32960
    48
        \<Longrightarrow> Says Server B \<lbrace>Nonce M,
wenzelm@32960
    49
                    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
wenzelm@32960
    50
                                      Nonce NB, Key KAB\<rbrace>\<rbrace>
wenzelm@32960
    51
               # evs3 \<in> orb"
paulson@18886
    52
paulson@18886
    53
  (*B can only check that the message he is bouncing is a ciphertext*)
paulson@18886
    54
  (*Sending M back is omitted*)   
berghofe@23746
    55
| OR4:  "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; 
wenzelm@32960
    56
          Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', 
wenzelm@32960
    57
                Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
wenzelm@32960
    58
            \<in> set evs4;
wenzelm@32960
    59
          Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace>
wenzelm@32960
    60
            \<in> set evs4\<rbrakk>
wenzelm@32960
    61
        \<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb"
paulson@18886
    62
paulson@18886
    63
berghofe@23746
    64
| Oops: "\<lbrakk>evso\<in> orb;  
wenzelm@32960
    65
           Says Server B \<lbrace>Nonce M,
wenzelm@32960
    66
                    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
wenzelm@32960
    67
                                      Nonce NB, Key KAB\<rbrace>\<rbrace> 
wenzelm@32960
    68
             \<in> set evso\<rbrakk>
paulson@18886
    69
 \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso 
paulson@18886
    70
     \<in> orb"
paulson@18886
    71
paulson@18886
    72
paulson@18886
    73
paulson@18886
    74
declare knows_Spy_partsEs [elim]
paulson@18886
    75
declare analz_into_parts [dest]
paulson@18886
    76
declare Fake_parts_insert_in_Un  [dest]
paulson@18886
    77
paulson@18886
    78
paulson@18886
    79
text{*Fragile proof, with backtracking in the possibility call.*}
paulson@18886
    80
lemma possibility_thm: "\<lbrakk>A \<noteq> Server; B \<noteq> Server; Key K \<notin> used[]\<rbrakk>    
paulson@18886
    81
      \<Longrightarrow>   \<exists> evs \<in> orb.           
paulson@18886
    82
     Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
    83
apply (intro exI bexI)
paulson@18886
    84
apply (rule_tac [2] orb.Nil
paulson@18886
    85
                    [THEN orb.OR1, THEN orb.Reception,
paulson@18886
    86
                     THEN orb.OR2, THEN orb.Reception,
paulson@18886
    87
                     THEN orb.OR3, THEN orb.Reception, THEN orb.OR4]) 
paulson@18886
    88
apply (possibility, simp add: used_Cons)  
paulson@18886
    89
done
paulson@18886
    90
paulson@18886
    91
paulson@18886
    92
lemma Gets_imp_Says :
paulson@18886
    93
     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
paulson@18886
    94
apply (erule rev_mp)
paulson@18886
    95
apply (erule orb.induct)
paulson@18886
    96
apply auto
paulson@18886
    97
done
paulson@18886
    98
paulson@18886
    99
lemma Gets_imp_knows_Spy: 
paulson@18886
   100
     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
paulson@18886
   101
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
paulson@18886
   102
paulson@18886
   103
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
paulson@18886
   104
paulson@18886
   105
lemma Gets_imp_knows:
paulson@18886
   106
     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
paulson@39251
   107
by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
paulson@18886
   108
paulson@18886
   109
lemma OR2_analz_knows_Spy: 
paulson@18886
   110
   "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
paulson@18886
   111
    \<Longrightarrow> X \<in> analz (knows Spy evs)"
paulson@18886
   112
by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
paulson@18886
   113
paulson@18886
   114
lemma OR4_parts_knows_Spy: 
paulson@18886
   115
   "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace>  \<in> set evs; 
paulson@18886
   116
      evs \<in> orb\<rbrakk>   \<Longrightarrow> X \<in> parts (knows Spy evs)"
paulson@18886
   117
by blast
paulson@18886
   118
paulson@18886
   119
lemma Oops_parts_knows_Spy: 
paulson@18886
   120
    "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs  
paulson@18886
   121
     \<Longrightarrow> K \<in> parts (knows Spy evs)"
paulson@18886
   122
by blast
paulson@18886
   123
paulson@18886
   124
lemmas OR2_parts_knows_Spy =
wenzelm@45605
   125
    OR2_analz_knows_Spy [THEN analz_into_parts]
paulson@18886
   126
paulson@18886
   127
ML
paulson@18886
   128
{*
paulson@18886
   129
fun parts_explicit_tac i = 
wenzelm@24122
   130
    forward_tac [@{thm Oops_parts_knows_Spy}] (i+7) THEN
wenzelm@24122
   131
    forward_tac [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
wenzelm@24122
   132
    forward_tac [@{thm OR2_parts_knows_Spy}]  (i+4)
paulson@18886
   133
*}
paulson@18886
   134
 
paulson@18886
   135
method_setup parts_explicit = {*
wenzelm@30549
   136
    Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
paulson@18886
   137
  "to explicitly state that some message components belong to parts knows Spy"
paulson@18886
   138
paulson@18886
   139
paulson@18886
   140
lemma Spy_see_shrK [simp]: 
paulson@18886
   141
    "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
paulson@18886
   142
by (erule orb.induct, parts_explicit, simp_all, blast+)
paulson@18886
   143
paulson@18886
   144
lemma Spy_analz_shrK [simp]: 
paulson@18886
   145
"evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
paulson@18886
   146
by auto
paulson@18886
   147
paulson@18886
   148
lemma Spy_see_shrK_D [dest!]:
paulson@18886
   149
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
paulson@18886
   150
by (blast dest: Spy_see_shrK)
paulson@18886
   151
paulson@18886
   152
lemma new_keys_not_used [simp]:
paulson@18886
   153
   "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk>  \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
paulson@18886
   154
apply (erule rev_mp)
paulson@18886
   155
apply (erule orb.induct, parts_explicit, simp_all)
paulson@18886
   156
apply (force dest!: keysFor_parts_insert)
paulson@18886
   157
apply (blast+)
paulson@18886
   158
done
paulson@18886
   159
paulson@18886
   160
paulson@18886
   161
paulson@18886
   162
subsection{* Proofs involving analz *}
paulson@18886
   163
paulson@18886
   164
text{*Describes the form of K and NA when the Server sends this message.  Also
paulson@18886
   165
  for Oops case.*}
paulson@18886
   166
lemma Says_Server_message_form: 
paulson@18886
   167
"\<lbrakk>Says Server B  \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
paulson@18886
   168
     evs \<in> orb\<rbrakk>                                            
paulson@18886
   169
 \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
paulson@18886
   170
by (erule rev_mp, erule orb.induct, simp_all)
paulson@18886
   171
paulson@18886
   172
lemma Says_Server_imp_Gets: 
paulson@18886
   173
 "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
paulson@18886
   174
                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
   175
    evs \<in> orb\<rbrakk>
paulson@18886
   176
  \<Longrightarrow>  Gets Server \<lbrace>Nonce M, Agent A, Agent B, 
paulson@18886
   177
                   Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 
paulson@18886
   178
               Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
paulson@18886
   179
         \<in> set evs"
paulson@18886
   180
by (erule rev_mp, erule orb.induct, simp_all)
paulson@18886
   181
paulson@18886
   182
paulson@18886
   183
lemma A_trusts_OR1: 
paulson@18886
   184
"\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);  
paulson@18886
   185
    A \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   186
 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   187
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   188
apply (blast)
paulson@18886
   189
done
paulson@18886
   190
paulson@18886
   191
paulson@18886
   192
lemma B_trusts_OR2:
paulson@18886
   193
 "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>  
paulson@18886
   194
      \<in> parts (knows Spy evs);  B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   195
  \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X,  
paulson@18886
   196
              Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
paulson@18886
   197
          \<in> set evs)"
paulson@18886
   198
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   199
apply (blast+)
paulson@18886
   200
done
paulson@18886
   201
paulson@18886
   202
paulson@18886
   203
lemma B_trusts_OR3: 
paulson@18886
   204
"\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs);  
paulson@18886
   205
   B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   206
\<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 
paulson@18886
   207
         \<in> set evs"
paulson@18886
   208
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   209
apply (blast+)
paulson@18886
   210
done
paulson@18886
   211
paulson@18886
   212
lemma Gets_Server_message_form: 
paulson@18886
   213
"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
paulson@18886
   214
    evs \<in> orb\<rbrakk>                                              
paulson@18886
   215
 \<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
paulson@18886
   216
             | X \<in> analz (knows Spy evs)"
paulson@39251
   217
by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
paulson@39251
   218
          Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
paulson@18886
   219
paulson@18886
   220
lemma unique_Na: "\<lbrakk>Says A B  \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
paulson@18886
   221
         Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;  
paulson@18886
   222
    A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' & M=M'"
paulson@18886
   223
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
paulson@18886
   224
paulson@18886
   225
lemma unique_Nb: "\<lbrakk>Says B Server \<lbrace>Nonce M, Agent A, Agent B, X, Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
paulson@18886
   226
         Says B Server \<lbrace>Nonce M', Agent A', Agent B, X', Crypt (shrK B) \<lbrace>Nonce Nb,Nonce M', Nonce M', Agent A', Agent B\<rbrace>\<rbrace> \<in> set evs;   
paulson@18886
   227
    B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow>   M=M' & A=A' & X=X'"
paulson@18886
   228
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
paulson@18886
   229
paulson@18886
   230
lemma analz_image_freshCryptK_lemma:
paulson@18886
   231
"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
paulson@39251
   232
        (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
paulson@18886
   233
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@18886
   234
paulson@18886
   235
ML
paulson@18886
   236
{*
wenzelm@24122
   237
structure OtwayReesBella =
wenzelm@24122
   238
struct
paulson@18886
   239
wenzelm@51717
   240
val analz_image_freshK_ss =
wenzelm@51717
   241
  simpset_of
wenzelm@51717
   242
   (@{context} delsimps [image_insert, image_Un]
wenzelm@24122
   243
      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
wenzelm@51717
   244
      addsimps @{thms analz_image_freshK_simps})
wenzelm@24122
   245
wenzelm@24122
   246
end
paulson@18886
   247
*}
paulson@18886
   248
paulson@18886
   249
method_setup analz_freshCryptK = {*
wenzelm@30549
   250
    Scan.succeed (fn ctxt =>
wenzelm@30510
   251
     (SIMPLE_METHOD
wenzelm@21588
   252
      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
wenzelm@24122
   253
          REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
wenzelm@24122
   254
          ALLGOALS (asm_simp_tac
wenzelm@51717
   255
            (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))]))) *}
paulson@18886
   256
  "for proving useful rewrite rule"
paulson@18886
   257
paulson@18886
   258
paulson@18886
   259
method_setup disentangle = {*
wenzelm@30549
   260
    Scan.succeed
wenzelm@51798
   261
     (fn ctxt => SIMPLE_METHOD
wenzelm@21588
   262
      (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
wenzelm@51798
   263
                   ORELSE' hyp_subst_tac ctxt))) *}
paulson@18886
   264
  "for eliminating conjunctions, disjunctions and the like"
paulson@18886
   265
paulson@18886
   266
paulson@18886
   267
paulson@18886
   268
lemma analz_image_freshCryptK [rule_format]: 
paulson@18886
   269
"evs \<in> orb \<Longrightarrow>                              
paulson@18886
   270
     Key K \<notin> analz (knows Spy evs) \<longrightarrow>  
paulson@18886
   271
       (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow>                  
paulson@18886
   272
             (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) =   
paulson@18886
   273
             (Crypt K X \<in> analz (knows Spy evs)))"
paulson@18886
   274
apply (erule orb.induct)
paulson@18886
   275
apply (analz_mono_contra)
paulson@18886
   276
apply (frule_tac [7] Gets_Server_message_form)
paulson@18886
   277
apply (frule_tac [9] Says_Server_message_form)
paulson@18886
   278
apply disentangle
paulson@18886
   279
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
paulson@18886
   280
prefer 8 apply clarify
nipkow@44890
   281
apply (analz_freshCryptK, spy_analz, fastforce)
paulson@18886
   282
done
paulson@18886
   283
paulson@18886
   284
paulson@18886
   285
paulson@18886
   286
lemma analz_insert_freshCryptK: 
paulson@18886
   287
"\<lbrakk>evs \<in> orb;  Key K \<notin> analz (knows Spy evs);  
paulson@18886
   288
         Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow>   
paulson@18886
   289
         (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) =  
paulson@18886
   290
         (Crypt K X \<in> analz (knows Spy evs))"
paulson@18886
   291
by (simp only: analz_image_freshCryptK analz_image_freshK_simps)
paulson@18886
   292
paulson@18886
   293
paulson@18886
   294
lemma analz_hard: 
paulson@18886
   295
"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
paulson@18886
   296
             Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
paulson@18886
   297
   Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs);  
paulson@18886
   298
   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   299
 \<Longrightarrow>  Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   300
apply (erule rev_mp)
paulson@18886
   301
apply (erule rev_mp)
paulson@18886
   302
apply (erule orb.induct)
paulson@18886
   303
apply (frule_tac [7] Gets_Server_message_form)
paulson@18886
   304
apply (frule_tac [9] Says_Server_message_form)
paulson@18886
   305
apply disentangle
paulson@18886
   306
txt{*letting the simplifier solve OR2*}
paulson@18886
   307
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
paulson@18886
   308
apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
paulson@18886
   309
apply (spy_analz)
paulson@18886
   310
txt{*OR1*}
paulson@18886
   311
apply blast
paulson@18886
   312
txt{*Oops*}
paulson@18886
   313
prefer 4 apply (blast dest: analz_insert_freshCryptK)
paulson@18886
   314
txt{*OR4 - ii*}
paulson@18886
   315
prefer 3 apply (blast)
paulson@18886
   316
txt{*OR3*}
paulson@18886
   317
(*adding Gets_imp_ and Says_imp_ for efficiency*)
paulson@18886
   318
apply (blast dest: 
paulson@18886
   319
       A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
paulson@18886
   320
txt{*OR4 - i *}
paulson@18886
   321
apply clarify
paulson@18886
   322
apply (simp add: pushes split_ifs)
paulson@18886
   323
apply (case_tac "Aaa\<in>bad")
paulson@18886
   324
apply (blast dest: analz_insert_freshCryptK)
paulson@18886
   325
apply clarify
paulson@18886
   326
apply simp
paulson@18886
   327
apply (case_tac "Ba\<in>bad")
paulson@18886
   328
apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
paulson@18886
   329
apply (simp (no_asm_simp))
paulson@18886
   330
apply clarify
paulson@18886
   331
apply (frule Gets_imp_knows_Spy 
paulson@18886
   332
             [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
paulson@18886
   333
       assumption, assumption, assumption, erule exE)
paulson@18886
   334
apply (frule Says_Server_imp_Gets 
paulson@18886
   335
            [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
paulson@18886
   336
            THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
paulson@18886
   337
       assumption, assumption, assumption, assumption)
paulson@18886
   338
apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
paulson@18886
   339
done
paulson@18886
   340
paulson@18886
   341
paulson@18886
   342
lemma Gets_Server_message_form': 
paulson@18886
   343
"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace>  \<in> set evs;  
paulson@18886
   344
   B \<notin> bad; evs \<in> orb\<rbrakk>                              
paulson@18886
   345
  \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
paulson@18886
   346
by (blast dest!: B_trusts_OR3 Says_Server_message_form)
paulson@18886
   347
paulson@18886
   348
paulson@18886
   349
lemma OR4_imp_Gets: 
paulson@18886
   350
"\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;   
paulson@18886
   351
   B \<notin> bad; evs \<in> orb\<rbrakk>  
paulson@18886
   352
 \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
paulson@18886
   353
                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)"
paulson@18886
   354
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   355
prefer 3 apply (blast dest: Gets_Server_message_form')
paulson@18886
   356
apply blast+
paulson@18886
   357
done
paulson@18886
   358
paulson@18886
   359
paulson@18886
   360
lemma A_keydist_to_B: 
paulson@18886
   361
"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
paulson@18886
   362
            Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
paulson@18886
   363
   Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;    
paulson@18886
   364
   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>  
paulson@18886
   365
  \<Longrightarrow> Key K \<in> analz (knows B evs)"
paulson@18886
   366
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
paulson@18886
   367
apply (drule analz_hard, assumption, assumption, assumption, assumption)
paulson@18886
   368
apply (drule OR4_imp_Gets, assumption, assumption)
nipkow@44890
   369
apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
paulson@18886
   370
done
paulson@18886
   371
paulson@18886
   372
paulson@18886
   373
text{*Other properties as for the original protocol*}
paulson@18886
   374
paulson@18886
   375
paulson@18886
   376
end