src/HOL/SET_Protocol/Public_SET.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 59498 50b60f501b05
child 61984 cdea44c775fa
permissions -rw-r--r--
isabelle update_cartouches;
wenzelm@33028
     1
(*  Title:      HOL/SET_Protocol/Public_SET.thy
wenzelm@32960
     2
    Author:     Giampaolo Bella
wenzelm@32960
     3
    Author:     Fabio Massacci
wenzelm@32960
     4
    Author:     Lawrence C Paulson
paulson@14199
     5
*)
paulson@14199
     6
wenzelm@58889
     7
section{*The Public-Key Theory, Modified for SET*}
paulson@14199
     8
wenzelm@33028
     9
theory Public_SET
wenzelm@33028
    10
imports Event_SET
wenzelm@33028
    11
begin
paulson@14199
    12
paulson@14199
    13
subsection{*Symmetric and Asymmetric Keys*}
paulson@14199
    14
paulson@14199
    15
text{*definitions influenced by the wish to assign asymmetric keys 
paulson@14199
    16
  - since the beginning - only to RCA and CAs, namely we need a partial 
paulson@14199
    17
  function on type Agent*}
paulson@14199
    18
paulson@14199
    19
paulson@14199
    20
text{*The SET specs mention two signature keys for CAs - we only have one*}
paulson@14199
    21
paulson@14199
    22
consts
paulson@14199
    23
  publicKey :: "[bool, agent] => key"
paulson@14199
    24
    --{*the boolean is TRUE if a signing key*}
paulson@14199
    25
wenzelm@35068
    26
abbreviation "pubEK == publicKey False"
wenzelm@35068
    27
abbreviation "pubSK == publicKey True"
paulson@14199
    28
wenzelm@35068
    29
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
wenzelm@35068
    30
abbreviation "priEK A == invKey (pubEK A)"
wenzelm@35068
    31
abbreviation "priSK A == invKey (pubSK A)"
paulson@14199
    32
paulson@14199
    33
text{*By freeness of agents, no two agents have the same key. Since
paulson@14199
    34
 @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
paulson@14199
    35
paulson@14199
    36
specification (publicKey)
paulson@14199
    37
  injective_publicKey:
paulson@14199
    38
    "publicKey b A = publicKey c A' ==> b=c & A=A'"
paulson@14218
    39
(*<*)
paulson@14199
    40
   apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) 
paulson@14199
    41
   apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) 
paulson@14199
    42
   apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
paulson@14199
    43
(*or this, but presburger won't abstract out the function applications
paulson@14199
    44
   apply presburger+
paulson@14199
    45
*)
paulson@14199
    46
   done                       
paulson@14218
    47
(*>*)
paulson@14199
    48
wenzelm@45827
    49
axiomatization where
paulson@14199
    50
  (*No private key equals any public key (essential to ensure that private
paulson@14199
    51
    keys are private!) *)
paulson@14199
    52
  privateKey_neq_publicKey [iff]:
paulson@14199
    53
      "invKey (publicKey b A) \<noteq> publicKey b' A'"
paulson@14199
    54
paulson@14199
    55
declare privateKey_neq_publicKey [THEN not_sym, iff]
paulson@14199
    56
paulson@14199
    57
  
paulson@14199
    58
subsection{*Initial Knowledge*}
paulson@14199
    59
paulson@14199
    60
text{*This information is not necessary.  Each protocol distributes any needed
paulson@14199
    61
certificates, and anyway our proofs require a formalization of the Spy's 
paulson@14199
    62
knowledge only.  However, the initial knowledge is as follows:
paulson@14199
    63
   All agents know RCA's public keys;
paulson@14199
    64
   RCA and CAs know their own respective keys;
paulson@14199
    65
   RCA (has already certified and therefore) knows all CAs public keys; 
paulson@14199
    66
   Spy knows all keys of all bad agents.*}
haftmann@39758
    67
haftmann@39758
    68
overloading initState \<equiv> "initState"
haftmann@39758
    69
begin
haftmann@39758
    70
haftmann@39758
    71
primrec initState where
paulson@14218
    72
(*<*)
paulson@14199
    73
  initState_CA:
paulson@14199
    74
    "initState (CA i)  =
paulson@14199
    75
       (if i=0 then Key ` ({priEK RCA, priSK RCA} Un
wenzelm@32960
    76
                            pubEK ` (range CA) Un pubSK ` (range CA))
wenzelm@32960
    77
        else {Key (priEK (CA i)), Key (priSK (CA i)),
wenzelm@32960
    78
              Key (pubEK (CA i)), Key (pubSK (CA i)),
wenzelm@32960
    79
              Key (pubEK RCA), Key (pubSK RCA)})"
paulson@14199
    80
haftmann@39758
    81
| initState_Cardholder:
paulson@14199
    82
    "initState (Cardholder i)  =    
paulson@14199
    83
       {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
wenzelm@32960
    84
        Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
wenzelm@32960
    85
        Key (pubEK RCA), Key (pubSK RCA)}"
paulson@14199
    86
haftmann@39758
    87
| initState_Merchant:
paulson@14199
    88
    "initState (Merchant i)  =    
paulson@14199
    89
       {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
wenzelm@32960
    90
        Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
wenzelm@32960
    91
        Key (pubEK RCA), Key (pubSK RCA)}"
paulson@14199
    92
haftmann@39758
    93
| initState_PG:
paulson@14199
    94
    "initState (PG i)  = 
paulson@14199
    95
       {Key (priEK (PG i)), Key (priSK (PG i)),
wenzelm@32960
    96
        Key (pubEK (PG i)), Key (pubSK (PG i)),
wenzelm@32960
    97
        Key (pubEK RCA), Key (pubSK RCA)}"
paulson@14218
    98
(*>*)
haftmann@39758
    99
| initState_Spy:
paulson@14199
   100
    "initState Spy = Key ` (invKey ` pubEK ` bad Un
wenzelm@32960
   101
                            invKey ` pubSK ` bad Un
wenzelm@32960
   102
                            range pubEK Un range pubSK)"
paulson@14199
   103
haftmann@39758
   104
end
haftmann@39758
   105
paulson@14199
   106
paulson@14199
   107
text{*Injective mapping from agents to PANs: an agent can have only one card*}
paulson@14199
   108
paulson@14199
   109
consts  pan :: "agent => nat"
paulson@14199
   110
paulson@14199
   111
specification (pan)
paulson@14199
   112
  inj_pan: "inj pan"
paulson@14199
   113
  --{*No two agents have the same PAN*}
paulson@14218
   114
(*<*)
paulson@14199
   115
   apply (rule exI [of _ "nat_of_agent"]) 
paulson@14199
   116
   apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) 
paulson@14199
   117
   done
paulson@14218
   118
(*>*)
paulson@14199
   119
paulson@14199
   120
declare inj_pan [THEN inj_eq, iff]
paulson@14199
   121
paulson@14199
   122
consts
paulson@14199
   123
  XOR :: "nat*nat => nat"  --{*no properties are assumed of exclusive-or*}
paulson@14199
   124
paulson@14199
   125
paulson@14199
   126
subsection{*Signature Primitives*}
paulson@14199
   127
wenzelm@36866
   128
definition
paulson@14199
   129
 (* Signature = Message + signed Digest *)
paulson@14199
   130
  sign :: "[key, msg]=>msg"
wenzelm@36866
   131
  where "sign K X = {|X, Crypt K (Hash X) |}"
paulson@14199
   132
wenzelm@36866
   133
definition
paulson@14199
   134
 (* Signature Only = signed Digest Only *)
paulson@14199
   135
  signOnly :: "[key, msg]=>msg"
wenzelm@36866
   136
  where "signOnly K X = Crypt K (Hash X)"
paulson@14199
   137
wenzelm@36866
   138
definition
paulson@14199
   139
 (* Signature for Certificates = Message + signed Message *)
paulson@14199
   140
  signCert :: "[key, msg]=>msg"
wenzelm@36866
   141
  where "signCert K X = {|X, Crypt K X |}"
paulson@14199
   142
wenzelm@36866
   143
definition
paulson@14199
   144
 (* Certification Authority's Certificate.
paulson@14199
   145
    Contains agent name, a key, a number specifying the key's target use,
paulson@14199
   146
              a key to sign the entire certificate.
paulson@14199
   147
paulson@14199
   148
    Should prove if signK=priSK RCA and C=CA i,
paulson@14199
   149
                  then Ka=pubEK i or pubSK i depending on T  ??
paulson@14199
   150
 *)
paulson@14199
   151
  cert :: "[agent, key, msg, key] => msg"
wenzelm@36866
   152
  where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"
paulson@14199
   153
wenzelm@36866
   154
definition
paulson@14199
   155
 (* Cardholder's Certificate.
paulson@14199
   156
    Contains a PAN, the certified key Ka, the PANSecret PS,
paulson@14199
   157
    a number specifying the target use for Ka, the signing key signK.
paulson@14199
   158
 *)
paulson@14199
   159
  certC :: "[nat, key, nat, msg, key] => msg"
wenzelm@36866
   160
  where "certC PAN Ka PS T signK =
wenzelm@36866
   161
    signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
paulson@14199
   162
wenzelm@35068
   163
(*cert and certA have no repeated elements, so they could be abbreviations,
wenzelm@35068
   164
  but that's tricky and makes proofs slower*)
paulson@14199
   165
wenzelm@35068
   166
abbreviation "onlyEnc == Number 0"
wenzelm@35068
   167
abbreviation "onlySig == Number (Suc 0)"
wenzelm@35068
   168
abbreviation "authCode == Number (Suc (Suc 0))"
paulson@14199
   169
paulson@14199
   170
subsection{*Encryption Primitives*}
paulson@14199
   171
haftmann@35416
   172
definition EXcrypt :: "[key,key,msg,msg] => msg" where
paulson@14199
   173
  --{*Extra Encryption*}
paulson@14199
   174
    (*K: the symmetric key   EK: the public encryption key*)
wenzelm@36866
   175
    "EXcrypt K EK M m =
paulson@14199
   176
       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
paulson@14199
   177
haftmann@35416
   178
definition EXHcrypt :: "[key,key,msg,msg] => msg" where
paulson@14199
   179
  --{*Extra Encryption with Hashing*}
paulson@14199
   180
    (*K: the symmetric key   EK: the public encryption key*)
wenzelm@36866
   181
    "EXHcrypt K EK M m =
paulson@14199
   182
       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
paulson@14199
   183
haftmann@35416
   184
definition Enc :: "[key,key,key,msg] => msg" where
paulson@14199
   185
  --{*Simple Encapsulation with SIGNATURE*}
paulson@14199
   186
    (*SK: the sender's signing key
paulson@14199
   187
      K: the symmetric key
paulson@14199
   188
      EK: the public encryption key*)
wenzelm@36866
   189
    "Enc SK K EK M =
paulson@14199
   190
       {|Crypt K (sign SK M), Crypt EK (Key K)|}"
paulson@14199
   191
haftmann@35416
   192
definition EncB :: "[key,key,key,msg,msg] => msg" where
paulson@14199
   193
  --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
wenzelm@36866
   194
    "EncB SK K EK M b =
paulson@14199
   195
       {|Enc SK K EK {|M, Hash b|}, b|}"
paulson@14199
   196
paulson@14199
   197
paulson@14199
   198
subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
paulson@14199
   199
paulson@14199
   200
lemma publicKey_eq_iff [iff]:
paulson@14199
   201
     "(publicKey b A = publicKey b' A') = (b=b' & A=A')"
paulson@14199
   202
by (blast dest: injective_publicKey)
paulson@14199
   203
paulson@14199
   204
lemma privateKey_eq_iff [iff]:
paulson@14199
   205
     "(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' & A=A')"
paulson@14199
   206
by auto
paulson@14199
   207
paulson@14199
   208
lemma not_symKeys_publicKey [iff]: "publicKey b A \<notin> symKeys"
paulson@14199
   209
by (simp add: symKeys_def)
paulson@14199
   210
paulson@14199
   211
lemma not_symKeys_privateKey [iff]: "invKey (publicKey b A) \<notin> symKeys"
paulson@14199
   212
by (simp add: symKeys_def)
paulson@14199
   213
paulson@14199
   214
lemma symKeys_invKey_eq [simp]: "K \<in> symKeys ==> invKey K = K"
paulson@14199
   215
by (simp add: symKeys_def)
paulson@14199
   216
paulson@14199
   217
lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
paulson@14199
   218
by (unfold symKeys_def, auto)
paulson@14199
   219
paulson@14199
   220
text{*Can be slow (or even loop) as a simprule*}
paulson@14199
   221
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
paulson@14199
   222
by blast
paulson@14199
   223
paulson@14199
   224
text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
paulson@14199
   225
in practice.*}
paulson@14199
   226
lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
paulson@14199
   227
by blast
paulson@14199
   228
paulson@14199
   229
lemma symKey_neq_publicKey: "K \<in> symKeys ==> K \<noteq> publicKey b A"
paulson@14199
   230
by blast
paulson@14199
   231
paulson@14199
   232
lemma privateKey_neq_symKey: "K \<in> symKeys ==> invKey (publicKey b A) \<noteq> K"
paulson@14199
   233
by blast
paulson@14199
   234
paulson@14199
   235
lemma symKey_neq_privateKey: "K \<in> symKeys ==> K \<noteq> invKey (publicKey b A)"
paulson@14199
   236
by blast
paulson@14199
   237
paulson@14199
   238
lemma analz_symKeys_Decrypt:
paulson@14199
   239
     "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
paulson@14199
   240
      ==> X \<in> analz H"
paulson@14199
   241
by auto
paulson@14199
   242
paulson@14199
   243
paulson@14199
   244
subsection{*"Image" Equations That Hold for Injective Functions *}
paulson@14199
   245
paulson@14199
   246
lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
paulson@14199
   247
by auto
paulson@14199
   248
paulson@14199
   249
text{*holds because invKey is injective*}
paulson@14199
   250
lemma publicKey_image_eq [iff]:
paulson@14199
   251
     "(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
paulson@14199
   252
by auto
paulson@14199
   253
paulson@14199
   254
lemma privateKey_image_eq [iff]:
paulson@14199
   255
     "(invKey (publicKey b A) \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
paulson@14199
   256
by auto
paulson@14199
   257
paulson@14199
   258
lemma privateKey_notin_image_publicKey [iff]:
paulson@14199
   259
     "invKey (publicKey b A) \<notin> publicKey c ` AS"
paulson@14199
   260
by auto
paulson@14199
   261
paulson@14199
   262
lemma publicKey_notin_image_privateKey [iff]:
paulson@14199
   263
     "publicKey b A \<notin> invKey ` publicKey c ` AS"
paulson@14199
   264
by auto
paulson@14199
   265
paulson@14199
   266
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
paulson@14199
   267
apply (simp add: keysFor_def)
paulson@14199
   268
apply (induct_tac "C")
paulson@14199
   269
apply (auto intro: range_eqI)
paulson@14199
   270
done
paulson@14199
   271
paulson@14199
   272
text{*for proving @{text new_keys_not_used}*}
paulson@14199
   273
lemma keysFor_parts_insert:
paulson@14199
   274
     "[| K \<in> keysFor (parts (insert X H));  X \<in> synth (analz H) |]  
paulson@14199
   275
      ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
paulson@14218
   276
by (force dest!: 
paulson@14199
   277
         parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@14199
   278
         analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] 
paulson@14199
   279
            intro: analz_into_parts)
paulson@14199
   280
paulson@14199
   281
lemma Crypt_imp_keysFor [intro]:
paulson@14199
   282
     "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
paulson@14199
   283
by (drule Crypt_imp_invKey_keysFor, simp)
paulson@14199
   284
paulson@14199
   285
text{*Agents see their own private keys!*}
paulson@14199
   286
lemma privateKey_in_initStateCA [iff]:
paulson@14199
   287
     "Key (invKey (publicKey b A)) \<in> initState A"
paulson@14199
   288
by (case_tac "A", auto)
paulson@14199
   289
paulson@14199
   290
text{*Agents see their own public keys!*}
paulson@14199
   291
lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
paulson@14199
   292
by (case_tac "A", auto)
paulson@14199
   293
paulson@14199
   294
text{*RCA sees CAs' public keys! *}
paulson@14199
   295
lemma pubK_CA_in_initState_RCA [iff]:
paulson@14199
   296
     "Key (publicKey b (CA i)) \<in> initState RCA"
paulson@14199
   297
by auto
paulson@14199
   298
paulson@14199
   299
paulson@14199
   300
text{*Spy knows all public keys*}
paulson@14199
   301
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
paulson@14199
   302
apply (induct_tac "evs")
paulson@14199
   303
apply (simp_all add: imageI knows_Cons split add: event.split)
paulson@14199
   304
done
paulson@14199
   305
paulson@14199
   306
declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
paulson@14199
   307
                            (*needed????*)
paulson@14199
   308
paulson@14199
   309
text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
paulson@14199
   310
lemma knows_Spy_bad_privateKey [intro!]:
paulson@14199
   311
     "A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
paulson@14206
   312
by (rule initState_subset_knows [THEN subsetD], simp)
paulson@14199
   313
paulson@14199
   314
paulson@14199
   315
subsection{*Fresh Nonces for Possibility Theorems*}
paulson@14199
   316
paulson@14199
   317
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
paulson@14199
   318
by (induct_tac "B", auto)
paulson@14199
   319
paulson@14199
   320
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
paulson@14199
   321
by (simp add: used_Nil)
paulson@14199
   322
paulson@14199
   323
text{*In any trace, there is an upper bound N on the greatest nonce in use.*}
paulson@14199
   324
lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
paulson@14199
   325
apply (induct_tac "evs")
paulson@14199
   326
apply (rule_tac x = 0 in exI)
paulson@14199
   327
apply (simp_all add: used_Cons split add: event.split, safe)
paulson@14199
   328
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
paulson@14199
   329
done
paulson@14199
   330
paulson@14199
   331
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
paulson@14199
   332
by (rule Nonce_supply_lemma [THEN exE], blast)
paulson@14199
   333
paulson@14199
   334
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
paulson@14199
   335
apply (rule Nonce_supply_lemma [THEN exE])
paulson@14199
   336
apply (rule someI, fast)
paulson@14199
   337
done
paulson@14199
   338
paulson@14199
   339
paulson@14199
   340
subsection{*Specialized Methods for Possibility Theorems*}
paulson@14199
   341
paulson@14199
   342
ML
paulson@14199
   343
{*
wenzelm@30607
   344
(*Tactic for possibility theorems*)
wenzelm@30607
   345
fun possibility_tac ctxt =
paulson@14199
   346
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
wenzelm@51717
   347
    (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
paulson@14199
   348
     THEN
paulson@14199
   349
     REPEAT_FIRST (eq_assume_tac ORELSE' 
wenzelm@59498
   350
                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))
paulson@14199
   351
paulson@14199
   352
(*For harder protocols (such as SET_CR!), where we have to set up some
paulson@14199
   353
  nonces and keys initially*)
wenzelm@30607
   354
fun basic_possibility_tac ctxt =
paulson@14199
   355
    REPEAT 
wenzelm@51717
   356
    (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
paulson@14199
   357
     THEN
wenzelm@59498
   358
     REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
paulson@14199
   359
*}
paulson@14199
   360
paulson@14199
   361
method_setup possibility = {*
wenzelm@33028
   362
    Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
paulson@14199
   363
    "for proving possibility theorems"
paulson@14199
   364
wenzelm@30607
   365
method_setup basic_possibility = {*
wenzelm@33028
   366
    Scan.succeed (SIMPLE_METHOD o basic_possibility_tac) *}
wenzelm@30607
   367
    "for proving possibility theorems"
paulson@14199
   368
paulson@14199
   369
paulson@14199
   370
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
paulson@14199
   371
paulson@14199
   372
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
paulson@14199
   373
by blast
paulson@14199
   374
paulson@14199
   375
lemma insert_Key_image:
paulson@14199
   376
     "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
paulson@14199
   377
by blast
paulson@14199
   378
paulson@14199
   379
text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
paulson@14199
   380
lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
paulson@14199
   381
by auto
paulson@14199
   382
paulson@14199
   383
lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
paulson@14199
   384
by (blast intro!: initState_into_used)
paulson@14199
   385
paulson@14199
   386
text{*Reverse the normal simplification of "image" to build up (not break down)
paulson@14199
   387
  the set of keys.  Based on @{text analz_image_freshK_ss}, but simpler.*}
paulson@14199
   388
lemmas analz_image_keys_simps =
paulson@14199
   389
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
paulson@14199
   390
       image_insert [THEN sym] image_Un [THEN sym] 
paulson@14199
   391
       rangeI symKeys_neq_imp_neq
paulson@14199
   392
       insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
paulson@14199
   393
paulson@14199
   394
paulson@14199
   395
(*General lemmas proved by Larry*)
paulson@14199
   396
paulson@14199
   397
subsection{*Controlled Unfolding of Abbreviations*}
paulson@14199
   398
paulson@14199
   399
text{*A set is expanded only if a relation is applied to it*}
paulson@14199
   400
lemma def_abbrev_simp_relation:
wenzelm@36866
   401
     "A = B ==> (A \<in> X) = (B \<in> X) &  
paulson@14199
   402
                 (u = A) = (u = B) &  
paulson@14199
   403
                 (A = u) = (B = u)"
paulson@14199
   404
by auto
paulson@14199
   405
paulson@14199
   406
text{*A set is expanded only if one of the given functions is applied to it*}
paulson@14199
   407
lemma def_abbrev_simp_function:
wenzelm@36866
   408
     "A = B  
paulson@14199
   409
      ==> parts (insert A X) = parts (insert B X) &  
paulson@14199
   410
          analz (insert A X) = analz (insert B X) &  
paulson@14199
   411
          keysFor (insert A X) = keysFor (insert B X)"
paulson@14199
   412
by auto
paulson@14199
   413
paulson@14199
   414
subsubsection{*Special Simplification Rules for @{term signCert}*}
paulson@14199
   415
paulson@14199
   416
text{*Avoids duplicating X and its components!*}
paulson@14199
   417
lemma parts_insert_signCert:
paulson@14199
   418
     "parts (insert (signCert K X) H) =  
paulson@14199
   419
      insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"
paulson@14199
   420
by (simp add: signCert_def insert_commute [of X])
paulson@14199
   421
paulson@14199
   422
text{*Avoids a case split! [X is always available]*}
paulson@14199
   423
lemma analz_insert_signCert:
paulson@14199
   424
     "analz (insert (signCert K X) H) =  
paulson@14199
   425
      insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"
paulson@14199
   426
by (simp add: signCert_def insert_commute [of X])
paulson@14199
   427
paulson@14199
   428
lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
paulson@14199
   429
by (simp add: signCert_def)
paulson@14199
   430
paulson@14199
   431
text{*Controlled rewrite rules for @{term signCert}, just the definitions
paulson@14199
   432
  of the others. Encryption primitives are just expanded, despite their huge
paulson@14199
   433
  redundancy!*}
paulson@14199
   434
lemmas abbrev_simps [simp] =
paulson@14199
   435
    parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
wenzelm@32960
   436
    sign_def     [THEN def_abbrev_simp_relation]
wenzelm@32960
   437
    sign_def     [THEN def_abbrev_simp_function]
paulson@14199
   438
    signCert_def [THEN def_abbrev_simp_relation]
paulson@14199
   439
    signCert_def [THEN def_abbrev_simp_function]
wenzelm@32960
   440
    certC_def    [THEN def_abbrev_simp_relation]
wenzelm@32960
   441
    certC_def    [THEN def_abbrev_simp_function]
wenzelm@32960
   442
    cert_def     [THEN def_abbrev_simp_relation]
wenzelm@32960
   443
    cert_def     [THEN def_abbrev_simp_function]
wenzelm@32960
   444
    EXcrypt_def  [THEN def_abbrev_simp_relation]
wenzelm@32960
   445
    EXcrypt_def  [THEN def_abbrev_simp_function]
paulson@14199
   446
    EXHcrypt_def [THEN def_abbrev_simp_relation]
paulson@14199
   447
    EXHcrypt_def [THEN def_abbrev_simp_function]
wenzelm@32960
   448
    Enc_def      [THEN def_abbrev_simp_relation]
wenzelm@32960
   449
    Enc_def      [THEN def_abbrev_simp_function]
wenzelm@32960
   450
    EncB_def     [THEN def_abbrev_simp_relation]
wenzelm@32960
   451
    EncB_def     [THEN def_abbrev_simp_function]
paulson@14199
   452
paulson@14199
   453
paulson@14199
   454
subsubsection{*Elimination Rules for Controlled Rewriting *}
paulson@14199
   455
paulson@14199
   456
lemma Enc_partsE: 
paulson@14199
   457
     "!!R. [|Enc SK K EK M \<in> parts H;  
paulson@14199
   458
             [|Crypt K (sign SK M) \<in> parts H;  
paulson@14199
   459
               Crypt EK (Key K) \<in> parts H|] ==> R|]  
paulson@14199
   460
           ==> R"
paulson@14199
   461
paulson@14199
   462
by (unfold Enc_def, blast)
paulson@14199
   463
paulson@14199
   464
lemma EncB_partsE: 
paulson@14199
   465
     "!!R. [|EncB SK K EK M b \<in> parts H;  
paulson@14199
   466
             [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;  
paulson@14199
   467
               Crypt EK (Key K) \<in> parts H;  
paulson@14199
   468
               b \<in> parts H|] ==> R|]  
paulson@14199
   469
           ==> R"
paulson@14199
   470
by (unfold EncB_def Enc_def, blast)
paulson@14199
   471
paulson@14199
   472
lemma EXcrypt_partsE: 
paulson@14199
   473
     "!!R. [|EXcrypt K EK M m \<in> parts H;  
paulson@14199
   474
             [|Crypt K {|M, Hash m|} \<in> parts H;  
paulson@14199
   475
               Crypt EK {|Key K, m|} \<in> parts H|] ==> R|]  
paulson@14199
   476
           ==> R"
paulson@14199
   477
by (unfold EXcrypt_def, blast)
paulson@14199
   478
paulson@14199
   479
paulson@14199
   480
subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
paulson@14199
   481
paulson@14199
   482
lemma analz_knows_absorb:
paulson@14199
   483
     "Key K \<in> analz (knows Spy evs)  
paulson@14199
   484
      ==> analz (Key ` (insert K H) \<union> knows Spy evs) =  
paulson@14199
   485
          analz (Key ` H \<union> knows Spy evs)"
paulson@14199
   486
by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
paulson@14199
   487
paulson@14199
   488
lemma analz_knows_absorb2:
paulson@14199
   489
     "Key K \<in> analz (knows Spy evs)  
paulson@14199
   490
      ==> analz (Key ` (insert X (insert K H)) \<union> knows Spy evs) =  
paulson@14199
   491
          analz (Key ` (insert X H) \<union> knows Spy evs)"
paulson@14199
   492
apply (subst insert_commute)
paulson@14199
   493
apply (erule analz_knows_absorb)
paulson@14199
   494
done
paulson@14199
   495
paulson@14199
   496
lemma analz_insert_subset_eq:
paulson@14199
   497
     "[|X \<in> analz (knows Spy evs);  knows Spy evs \<subseteq> H|]  
paulson@14199
   498
      ==> analz (insert X H) = analz H"
paulson@14199
   499
apply (rule analz_insert_eq)
paulson@14199
   500
apply (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   501
done
paulson@14199
   502
paulson@14199
   503
lemmas analz_insert_simps = 
paulson@14199
   504
         analz_insert_subset_eq Un_upper2
wenzelm@32960
   505
         subset_insertI [THEN [2] subset_trans] 
paulson@14199
   506
paulson@14199
   507
paulson@14199
   508
subsection{*Freshness Lemmas*}
paulson@14199
   509
paulson@14199
   510
lemma in_parts_Says_imp_used:
paulson@14199
   511
     "[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
paulson@14199
   512
by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
paulson@14199
   513
paulson@14199
   514
text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
paulson@14199
   515
lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
paulson@14199
   516
by auto
paulson@14199
   517
paulson@14199
   518
lemma fresh_notin_analz_knows_Spy:
paulson@14199
   519
     "Key K \<notin> used evs ==> Key K \<notin> analz (knows Spy evs)"
paulson@14199
   520
by (auto dest: analz_into_parts)
paulson@14199
   521
paulson@14199
   522
end