src/HOL/Auth/OtwayReesBella.thy
author berghofe
Wed Jul 11 11:14:51 2007 +0200 (2007-07-11)
changeset 23746 a455e69c31cc
parent 21588 cd0dc678a205
child 24122 fc7f857d33c8
permissions -rwxr-xr-x
Adapted to new inductive definition package.
paulson@18886
     1
(*  ID:         $Id$
paulson@18886
     2
    Author:     Giampaolo Bella, Catania University
paulson@18886
     3
*)
paulson@18886
     4
paulson@18886
     5
header{*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>
paulson@18886
    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>
paulson@18886
    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>
paulson@18886
    31
	 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, 
paulson@18886
    32
		   Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
paulson@18886
    33
	       # evs1 \<in> orb"
paulson@18886
    34
berghofe@23746
    35
| OR2:  "\<lbrakk>evs2\<in> orb;  Nonce NB \<notin> used evs2;
paulson@18886
    36
	   Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk>
paulson@18886
    37
	\<Longrightarrow> Says B Server 
paulson@18886
    38
		\<lbrace>Nonce M, Agent A, Agent B, X, 
paulson@18886
    39
	   Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
paulson@18886
    40
	       # evs2 \<in> orb"
paulson@18886
    41
berghofe@23746
    42
| OR3:  "\<lbrakk>evs3\<in> orb;  Key KAB \<notin> used evs3;
paulson@18886
    43
	  Gets Server 
paulson@18886
    44
	     \<lbrace>Nonce M, Agent A, Agent B, 
paulson@18886
    45
	       Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, 
paulson@18886
    46
	       Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
paulson@18886
    47
	  \<in> set evs3\<rbrakk>
paulson@18886
    48
	\<Longrightarrow> Says Server B \<lbrace>Nonce M,
paulson@18886
    49
		    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
paulson@18886
    50
				      Nonce NB, Key KAB\<rbrace>\<rbrace>
paulson@18886
    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>; 
paulson@18886
    56
	  Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', 
paulson@18886
    57
		Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
paulson@18886
    58
	    \<in> set evs4;
paulson@18886
    59
	  Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace>
paulson@18886
    60
	    \<in> set evs4\<rbrakk>
paulson@18886
    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;  
paulson@18886
    65
	   Says Server B \<lbrace>Nonce M,
paulson@18886
    66
		    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
paulson@18886
    67
				      Nonce NB, Key KAB\<rbrace>\<rbrace> 
paulson@18886
    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@18886
   107
apply (case_tac "B = Spy")
paulson@18886
   108
apply (blast dest!: Gets_imp_knows_Spy)
paulson@18886
   109
apply (blast dest!: Gets_imp_knows_agents)
paulson@18886
   110
done
paulson@18886
   111
paulson@18886
   112
paulson@18886
   113
lemma OR2_analz_knows_Spy: 
paulson@18886
   114
   "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
paulson@18886
   115
    \<Longrightarrow> X \<in> analz (knows Spy evs)"
paulson@18886
   116
by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
paulson@18886
   117
paulson@18886
   118
lemma OR4_parts_knows_Spy: 
paulson@18886
   119
   "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace>  \<in> set evs; 
paulson@18886
   120
      evs \<in> orb\<rbrakk>   \<Longrightarrow> X \<in> parts (knows Spy evs)"
paulson@18886
   121
by blast
paulson@18886
   122
paulson@18886
   123
lemma Oops_parts_knows_Spy: 
paulson@18886
   124
    "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs  
paulson@18886
   125
     \<Longrightarrow> K \<in> parts (knows Spy evs)"
paulson@18886
   126
by blast
paulson@18886
   127
paulson@18886
   128
lemmas OR2_parts_knows_Spy =
paulson@18886
   129
    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
paulson@18886
   130
paulson@18886
   131
ML
paulson@18886
   132
{*
paulson@18886
   133
val Oops_parts_knows_Spy = thm "Oops_parts_knows_Spy"
paulson@18886
   134
val OR4_parts_knows_Spy = thm "OR4_parts_knows_Spy"
paulson@18886
   135
val OR2_parts_knows_Spy = thm "OR2_parts_knows_Spy"
paulson@18886
   136
paulson@18886
   137
fun parts_explicit_tac i = 
paulson@18886
   138
    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
paulson@18886
   139
    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
paulson@18886
   140
    forward_tac [OR2_parts_knows_Spy]  (i+4)
paulson@18886
   141
*}
paulson@18886
   142
 
paulson@18886
   143
method_setup parts_explicit = {*
wenzelm@21588
   144
    Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
paulson@18886
   145
  "to explicitly state that some message components belong to parts knows Spy"
paulson@18886
   146
paulson@18886
   147
paulson@18886
   148
lemma Spy_see_shrK [simp]: 
paulson@18886
   149
    "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
paulson@18886
   150
by (erule orb.induct, parts_explicit, simp_all, blast+)
paulson@18886
   151
paulson@18886
   152
lemma Spy_analz_shrK [simp]: 
paulson@18886
   153
"evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
paulson@18886
   154
by auto
paulson@18886
   155
paulson@18886
   156
lemma Spy_see_shrK_D [dest!]:
paulson@18886
   157
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
paulson@18886
   158
by (blast dest: Spy_see_shrK)
paulson@18886
   159
paulson@18886
   160
lemma new_keys_not_used [simp]:
paulson@18886
   161
   "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk>  \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
paulson@18886
   162
apply (erule rev_mp)
paulson@18886
   163
apply (erule orb.induct, parts_explicit, simp_all)
paulson@18886
   164
apply (force dest!: keysFor_parts_insert)
paulson@18886
   165
apply (blast+)
paulson@18886
   166
done
paulson@18886
   167
paulson@18886
   168
paulson@18886
   169
paulson@18886
   170
subsection{* Proofs involving analz *}
paulson@18886
   171
paulson@18886
   172
text{*Describes the form of K and NA when the Server sends this message.  Also
paulson@18886
   173
  for Oops case.*}
paulson@18886
   174
lemma Says_Server_message_form: 
paulson@18886
   175
"\<lbrakk>Says Server B  \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
paulson@18886
   176
     evs \<in> orb\<rbrakk>                                            
paulson@18886
   177
 \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
paulson@18886
   178
by (erule rev_mp, erule orb.induct, simp_all)
paulson@18886
   179
paulson@18886
   180
lemma Says_Server_imp_Gets: 
paulson@18886
   181
 "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
paulson@18886
   182
                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;
paulson@18886
   183
    evs \<in> orb\<rbrakk>
paulson@18886
   184
  \<Longrightarrow>  Gets Server \<lbrace>Nonce M, Agent A, Agent B, 
paulson@18886
   185
                   Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 
paulson@18886
   186
               Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
paulson@18886
   187
         \<in> set evs"
paulson@18886
   188
by (erule rev_mp, erule orb.induct, simp_all)
paulson@18886
   189
paulson@18886
   190
paulson@18886
   191
lemma A_trusts_OR1: 
paulson@18886
   192
"\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);  
paulson@18886
   193
    A \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   194
 \<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
   195
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   196
apply (blast)
paulson@18886
   197
done
paulson@18886
   198
paulson@18886
   199
paulson@18886
   200
lemma B_trusts_OR2:
paulson@18886
   201
 "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>  
paulson@18886
   202
      \<in> parts (knows Spy evs);  B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   203
  \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X,  
paulson@18886
   204
              Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
paulson@18886
   205
          \<in> set evs)"
paulson@18886
   206
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   207
apply (blast+)
paulson@18886
   208
done
paulson@18886
   209
paulson@18886
   210
paulson@18886
   211
lemma B_trusts_OR3: 
paulson@18886
   212
"\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs);  
paulson@18886
   213
   B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   214
\<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 
paulson@18886
   215
         \<in> set evs"
paulson@18886
   216
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   217
apply (blast+)
paulson@18886
   218
done
paulson@18886
   219
paulson@18886
   220
lemma Gets_Server_message_form: 
paulson@18886
   221
"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
paulson@18886
   222
    evs \<in> orb\<rbrakk>                                              
paulson@18886
   223
 \<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
paulson@18886
   224
             | X \<in> analz (knows Spy evs)"
paulson@18886
   225
apply (case_tac "B \<in> bad")
paulson@18886
   226
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, 
paulson@18886
   227
                                 THEN analz.Decrypt, THEN analz.Fst])
paulson@18886
   228
prefer 3 apply blast
paulson@18886
   229
prefer 3 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN 
paulson@18886
   230
                                                 parts.Snd, THEN B_trusts_OR3]
paulson@18886
   231
                             Says_Server_message_form)
paulson@18886
   232
apply simp_all                                    
paulson@18886
   233
done
paulson@18886
   234
paulson@18886
   235
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
   236
         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
   237
    A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' & M=M'"
paulson@18886
   238
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
paulson@18886
   239
paulson@18886
   240
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
   241
         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
   242
    B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow>   M=M' & A=A' & X=X'"
paulson@18886
   243
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
paulson@18886
   244
paulson@18886
   245
lemma analz_image_freshCryptK_lemma:
paulson@18886
   246
"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
paulson@18886
   247
        (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)";
paulson@18886
   248
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@18886
   249
paulson@18886
   250
ML
paulson@18886
   251
{*
paulson@18886
   252
val analz_image_freshCryptK_lemma = thm "analz_image_freshCryptK_lemma";
paulson@18886
   253
val analz_image_freshK_simps = thms "analz_image_freshK_simps";
paulson@18886
   254
paulson@18886
   255
val analz_image_freshK_ss = 
paulson@18886
   256
     simpset() delsimps [image_insert, image_Un]
paulson@18886
   257
	       delsimps [imp_disjL]    (*reduces blow-up*)
paulson@18886
   258
	       addsimps thms "analz_image_freshK_simps"
paulson@18886
   259
*}
paulson@18886
   260
paulson@18886
   261
method_setup analz_freshCryptK = {*
wenzelm@20048
   262
    Method.ctxt_args (fn ctxt =>
wenzelm@21588
   263
     (Method.SIMPLE_METHOD
wenzelm@21588
   264
      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
paulson@18886
   265
                          REPEAT_FIRST (rtac analz_image_freshCryptK_lemma),
wenzelm@20048
   266
                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
paulson@18886
   267
  "for proving useful rewrite rule"
paulson@18886
   268
paulson@18886
   269
paulson@18886
   270
method_setup disentangle = {*
paulson@18886
   271
    Method.no_args
wenzelm@21588
   272
     (Method.SIMPLE_METHOD
wenzelm@21588
   273
      (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
paulson@18886
   274
                   ORELSE' hyp_subst_tac))) *}
paulson@18886
   275
  "for eliminating conjunctions, disjunctions and the like"
paulson@18886
   276
paulson@18886
   277
paulson@18886
   278
paulson@18886
   279
lemma analz_image_freshCryptK [rule_format]: 
paulson@18886
   280
"evs \<in> orb \<Longrightarrow>                              
paulson@18886
   281
     Key K \<notin> analz (knows Spy evs) \<longrightarrow>  
paulson@18886
   282
       (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow>                  
paulson@18886
   283
             (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) =   
paulson@18886
   284
             (Crypt K X \<in> analz (knows Spy evs)))"
paulson@18886
   285
apply (erule orb.induct)
paulson@18886
   286
apply (analz_mono_contra)
paulson@18886
   287
apply (frule_tac [7] Gets_Server_message_form)
paulson@18886
   288
apply (frule_tac [9] Says_Server_message_form)
paulson@18886
   289
apply disentangle
paulson@18886
   290
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
paulson@18886
   291
prefer 8 apply clarify
paulson@18886
   292
apply (analz_freshCryptK, spy_analz, fastsimp)
paulson@18886
   293
done
paulson@18886
   294
paulson@18886
   295
paulson@18886
   296
paulson@18886
   297
lemma analz_insert_freshCryptK: 
paulson@18886
   298
"\<lbrakk>evs \<in> orb;  Key K \<notin> analz (knows Spy evs);  
paulson@18886
   299
         Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow>   
paulson@18886
   300
         (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) =  
paulson@18886
   301
         (Crypt K X \<in> analz (knows Spy evs))"
paulson@18886
   302
by (simp only: analz_image_freshCryptK analz_image_freshK_simps)
paulson@18886
   303
paulson@18886
   304
paulson@18886
   305
lemma analz_hard: 
paulson@18886
   306
"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
paulson@18886
   307
             Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
paulson@18886
   308
   Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs);  
paulson@18886
   309
   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>                   
paulson@18886
   310
 \<Longrightarrow>  Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
paulson@18886
   311
apply (erule rev_mp)
paulson@18886
   312
apply (erule rev_mp)
paulson@18886
   313
apply (erule orb.induct)
paulson@18886
   314
apply (frule_tac [7] Gets_Server_message_form)
paulson@18886
   315
apply (frule_tac [9] Says_Server_message_form)
paulson@18886
   316
apply disentangle
paulson@18886
   317
txt{*letting the simplifier solve OR2*}
paulson@18886
   318
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
paulson@18886
   319
apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
paulson@18886
   320
apply (spy_analz)
paulson@18886
   321
txt{*OR1*}
paulson@18886
   322
apply blast
paulson@18886
   323
txt{*Oops*}
paulson@18886
   324
prefer 4 apply (blast dest: analz_insert_freshCryptK)
paulson@18886
   325
txt{*OR4 - ii*}
paulson@18886
   326
prefer 3 apply (blast)
paulson@18886
   327
txt{*OR3*}
paulson@18886
   328
(*adding Gets_imp_ and Says_imp_ for efficiency*)
paulson@18886
   329
apply (blast dest: 
paulson@18886
   330
       A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
paulson@18886
   331
txt{*OR4 - i *}
paulson@18886
   332
apply clarify
paulson@18886
   333
apply (simp add: pushes split_ifs)
paulson@18886
   334
apply (case_tac "Aaa\<in>bad")
paulson@18886
   335
apply (blast dest: analz_insert_freshCryptK)
paulson@18886
   336
apply clarify
paulson@18886
   337
apply simp
paulson@18886
   338
apply (case_tac "Ba\<in>bad")
paulson@18886
   339
apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
paulson@18886
   340
apply (simp (no_asm_simp))
paulson@18886
   341
apply clarify
paulson@18886
   342
apply (frule Gets_imp_knows_Spy 
paulson@18886
   343
             [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
paulson@18886
   344
       assumption, assumption, assumption, erule exE)
paulson@18886
   345
apply (frule Says_Server_imp_Gets 
paulson@18886
   346
            [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
paulson@18886
   347
            THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
paulson@18886
   348
       assumption, assumption, assumption, assumption)
paulson@18886
   349
apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
paulson@18886
   350
done
paulson@18886
   351
paulson@18886
   352
paulson@18886
   353
lemma Gets_Server_message_form': 
paulson@18886
   354
"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace>  \<in> set evs;  
paulson@18886
   355
   B \<notin> bad; evs \<in> orb\<rbrakk>                              
paulson@18886
   356
  \<Longrightarrow> K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
paulson@18886
   357
by (blast dest!: B_trusts_OR3 Says_Server_message_form)
paulson@18886
   358
paulson@18886
   359
paulson@18886
   360
lemma OR4_imp_Gets: 
paulson@18886
   361
"\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;   
paulson@18886
   362
   B \<notin> bad; evs \<in> orb\<rbrakk>  
paulson@18886
   363
 \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
paulson@18886
   364
                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)"
paulson@18886
   365
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
paulson@18886
   366
prefer 3 apply (blast dest: Gets_Server_message_form')
paulson@18886
   367
apply blast+
paulson@18886
   368
done
paulson@18886
   369
paulson@18886
   370
paulson@18886
   371
lemma A_keydist_to_B: 
paulson@18886
   372
"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
paulson@18886
   373
            Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
paulson@18886
   374
   Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;    
paulson@18886
   375
   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>  
paulson@18886
   376
  \<Longrightarrow> Key K \<in> analz (knows B evs)"
paulson@18886
   377
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
paulson@18886
   378
apply (drule analz_hard, assumption, assumption, assumption, assumption)
paulson@18886
   379
apply (drule OR4_imp_Gets, assumption, assumption)
paulson@18886
   380
apply (erule exE)
paulson@18886
   381
(*blast doesn't do because it can't infer that Key (shrK P) \<in> (knows P evs)*)
paulson@18886
   382
apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
paulson@18886
   383
done
paulson@18886
   384
paulson@18886
   385
paulson@18886
   386
text{*Other properties as for the original protocol*}
paulson@18886
   387
paulson@18886
   388
paulson@18886
   389
end