src/HOL/SET-Protocol/Cardholder_Registration.thy
author berghofe
Wed Jul 11 11:28:13 2007 +0200 (2007-07-11)
changeset 23755 1c4672d130b1
parent 16417 9bc16273c2d4
child 24123 a0fc58900606
permissions -rw-r--r--
Adapted to new inductive definition package.
paulson@14199
     1
(*  Title:      HOL/Auth/SET/Cardholder_Registration
paulson@14199
     2
    ID:         $Id$
paulson@14199
     3
    Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
paulson@14199
     4
                Piero Tramontano
paulson@14199
     5
*)
paulson@14199
     6
paulson@14199
     7
header{*The SET Cardholder Registration Protocol*}
paulson@14199
     8
haftmann@16417
     9
theory Cardholder_Registration imports PublicSET begin
paulson@14199
    10
paulson@14199
    11
text{*Note: nonces seem to consist of 20 bytes.  That includes both freshness
paulson@14199
    12
challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
paulson@14199
    13
*}
paulson@14199
    14
paulson@14199
    15
text{*Simplifications involving @{text analz_image_keys_simps} appear to
paulson@14199
    16
have become much slower. The cause is unclear. However, there is a big blow-up
paulson@14199
    17
and the rewriting is very sensitive to the set of rewrite rules given.*}
paulson@14199
    18
paulson@14199
    19
subsection{*Predicate Formalizing the Encryption Association between Keys *}
paulson@14199
    20
paulson@14199
    21
consts
paulson@14199
    22
  KeyCryptKey :: "[key, key, event list] => bool"
paulson@14199
    23
paulson@14199
    24
primrec
paulson@14199
    25
paulson@14199
    26
KeyCryptKey_Nil:
paulson@14199
    27
  "KeyCryptKey DK K [] = False"
paulson@14199
    28
paulson@14199
    29
KeyCryptKey_Cons:
paulson@14199
    30
      --{*Says is the only important case.
paulson@14199
    31
	1st case: CR5, where KC3 encrypts KC2.
paulson@14199
    32
	2nd case: any use of priEK C.
paulson@14199
    33
	Revision 1.12 has a more complicated version with separate treatment of
paulson@14199
    34
	  the dependency of KC1, KC2 and KC3 on priEK (CA i.)  Not needed since
paulson@14199
    35
	  priEK C is never sent (and so can't be lost except at the start). *}
paulson@14199
    36
  "KeyCryptKey DK K (ev # evs) =
paulson@14199
    37
   (KeyCryptKey DK K evs |
paulson@14199
    38
    (case ev of
paulson@14199
    39
      Says A B Z =>
paulson@14199
    40
       ((\<exists>N X Y. A \<noteq> Spy &
paulson@14199
    41
	         DK \<in> symKeys &
paulson@14199
    42
		 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
paulson@14199
    43
	(\<exists>C. DK = priEK C))
paulson@14199
    44
    | Gets A' X => False
paulson@14199
    45
    | Notes A' X => False))"
paulson@14199
    46
paulson@14199
    47
paulson@14199
    48
subsection{*Predicate formalizing the association between keys and nonces *}
paulson@14199
    49
paulson@14199
    50
consts
paulson@14199
    51
  KeyCryptNonce :: "[key, key, event list] => bool"
paulson@14199
    52
paulson@14199
    53
primrec
paulson@14199
    54
paulson@14199
    55
KeyCryptNonce_Nil:
paulson@14199
    56
  "KeyCryptNonce EK K [] = False"
paulson@14199
    57
paulson@14199
    58
KeyCryptNonce_Cons:
paulson@14199
    59
  --{*Says is the only important case.
paulson@14199
    60
    1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
paulson@14199
    61
    2nd case: CR5, where KC3 encrypts NC3;
paulson@14199
    62
    3rd case: CR6, where KC2 encrypts NC3;
paulson@14199
    63
    4th case: CR6, where KC2 encrypts NonceCCA;
paulson@14199
    64
    5th case: any use of @{term "priEK C"} (including CardSecret).
paulson@14199
    65
    NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
paulson@14199
    66
    But we can't prove @{text Nonce_compromise} unless the relation covers ALL
paulson@14199
    67
	nonces that the protocol keeps secret.
paulson@14199
    68
  *}
paulson@14199
    69
  "KeyCryptNonce DK N (ev # evs) =
paulson@14199
    70
   (KeyCryptNonce DK N evs |
paulson@14199
    71
    (case ev of
paulson@14199
    72
      Says A B Z =>
paulson@14199
    73
       A \<noteq> Spy &
paulson@14199
    74
       ((\<exists>X Y. DK \<in> symKeys &
paulson@14199
    75
	       Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
paulson@14199
    76
	(\<exists>X Y. DK \<in> symKeys &
paulson@14199
    77
	       Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
paulson@14199
    78
	(\<exists>K i X Y.
paulson@14199
    79
	  K \<in> symKeys &
paulson@14199
    80
          Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
paulson@14199
    81
	  (DK=K | KeyCryptKey DK K evs)) |
paulson@14199
    82
	(\<exists>K C NC3 Y.
paulson@14199
    83
	  K \<in> symKeys &
paulson@14199
    84
          Z = Crypt K
paulson@14199
    85
 	        {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
paulson@14199
    86
                  Y|} &
paulson@14199
    87
	  (DK=K | KeyCryptKey DK K evs)) |
paulson@14199
    88
	(\<exists>C. DK = priEK C))
paulson@14199
    89
    | Gets A' X => False
paulson@14199
    90
    | Notes A' X => False))"
paulson@14199
    91
paulson@14199
    92
paulson@14199
    93
subsection{*Formal protocol definition *}
paulson@14199
    94
berghofe@23755
    95
inductive_set
berghofe@23755
    96
  set_cr :: "event list set"
berghofe@23755
    97
where
paulson@14199
    98
paulson@14199
    99
  Nil:    --{*Initial trace is empty*}
paulson@14199
   100
	  "[] \<in> set_cr"
paulson@14199
   101
berghofe@23755
   102
| Fake:    --{*The spy MAY say anything he CAN say.*}
paulson@14199
   103
	   "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
paulson@14199
   104
	    ==> Says Spy B X  # evsf \<in> set_cr"
paulson@14199
   105
berghofe@23755
   106
| Reception: --{*If A sends a message X to B, then B might receive it*}
paulson@14199
   107
	     "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
paulson@14199
   108
              ==> Gets B X  # evsr \<in> set_cr"
paulson@14199
   109
berghofe@23755
   110
| SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
paulson@14199
   111
	     "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
paulson@14199
   112
	      ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
paulson@14199
   113
berghofe@23755
   114
| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
paulson@14199
   115
	     "[| evs2 \<in> set_cr;
paulson@14199
   116
		 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
paulson@14199
   117
	      ==> Says (CA i) C
paulson@14199
   118
		       {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
paulson@14199
   119
			 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
paulson@14199
   120
			 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
paulson@14199
   121
		    # evs2 \<in> set_cr"
paulson@14199
   122
berghofe@23755
   123
| SET_CR3:
paulson@14199
   124
   --{*RegFormReq: C sends his PAN and a new nonce to CA.
paulson@14199
   125
   C verifies that
paulson@14199
   126
    - nonce received is the same as that sent;
paulson@14199
   127
    - certificates are signed by RCA;
paulson@14199
   128
    - certificates are an encryption certificate (flag is onlyEnc) and a
paulson@14199
   129
      signature certificate (flag is onlySig);
paulson@14199
   130
    - certificates pertain to the CA that C contacted (this is done by
paulson@14199
   131
      checking the signature).
paulson@14199
   132
   C generates a fresh symmetric key KC1.
paulson@14199
   133
   The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
paulson@14199
   134
   is not clear. *}
paulson@14199
   135
"[| evs3 \<in> set_cr;  C = Cardholder k;
paulson@14199
   136
    Nonce NC2 \<notin> used evs3;
paulson@14199
   137
    Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
paulson@14199
   138
    Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
paulson@14199
   139
	     cert (CA i) EKi onlyEnc (priSK RCA),
paulson@14199
   140
	     cert (CA i) SKi onlySig (priSK RCA)|}
paulson@14199
   141
       \<in> set evs3;
paulson@14199
   142
    Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
paulson@14199
   143
 ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
paulson@14199
   144
       # Notes C {|Key KC1, Agent (CA i)|}
paulson@14199
   145
       # evs3 \<in> set_cr"
paulson@14199
   146
berghofe@23755
   147
| SET_CR4:
paulson@14199
   148
    --{*RegFormRes:
paulson@14199
   149
    CA responds sending NC2 back with a new nonce NCA, after checking that
paulson@14199
   150
     - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
paulson@14199
   151
     - the entire message is encrypted with the same key found inside the
paulson@14199
   152
       envelope (here, KC1) *}
paulson@14199
   153
"[| evs4 \<in> set_cr;
paulson@14199
   154
    Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
paulson@14199
   155
    Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
paulson@14199
   156
       \<in> set evs4 |]
paulson@14199
   157
  ==> Says (CA i) C
paulson@14199
   158
	  {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
paulson@14199
   159
	    cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
paulson@14199
   160
	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
paulson@14199
   161
       # evs4 \<in> set_cr"
paulson@14199
   162
berghofe@23755
   163
| SET_CR5:
paulson@14199
   164
   --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
paulson@14199
   165
       and its half of the secret value to CA.
paulson@14199
   166
       We now assume that C has a fixed key pair, and he submits (pubSK C).
paulson@14199
   167
       The protocol does not require this key to be fresh.
paulson@14199
   168
       The encryption below is actually EncX.*}
paulson@14199
   169
"[| evs5 \<in> set_cr;  C = Cardholder k;
paulson@14199
   170
    Nonce NC3 \<notin> used evs5;  Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
paulson@14199
   171
    Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
paulson@14199
   172
    Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
paulson@14199
   173
    Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
paulson@14199
   174
             cert (CA i) EKi onlyEnc (priSK RCA),
paulson@14199
   175
             cert (CA i) SKi onlySig (priSK RCA) |}
paulson@14199
   176
        \<in> set evs5;
paulson@14199
   177
    Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
paulson@14199
   178
         \<in> set evs5 |]
paulson@14199
   179
==> Says C (CA i)
paulson@14199
   180
         {|Crypt KC3
paulson@14199
   181
	     {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
paulson@14199
   182
	       Crypt (priSK C)
paulson@14199
   183
	         (Hash {|Agent C, Nonce NC3, Key KC2,
paulson@14199
   184
			 Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
paulson@14199
   185
           Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
paulson@14199
   186
    # Notes C {|Key KC2, Agent (CA i)|}
paulson@14199
   187
    # Notes C {|Key KC3, Agent (CA i)|}
paulson@14199
   188
    # evs5 \<in> set_cr"
paulson@14199
   189
paulson@14199
   190
paulson@14199
   191
  --{* CertRes: CA responds sending NC3 back with its half of the secret value,
paulson@14199
   192
   its signature certificate and the new cardholder signature
paulson@14199
   193
   certificate.  CA checks to have never certified the key proposed by C.
paulson@14199
   194
   NOTE: In Merchant Registration, the corresponding rule (4)
paulson@14199
   195
   uses the "sign" primitive. The encryption below is actually @{term EncK}, 
paulson@14199
   196
   which is just @{term "Crypt K (sign SK X)"}.
paulson@14199
   197
*}
paulson@14199
   198
berghofe@23755
   199
| SET_CR6:
paulson@14199
   200
"[| evs6 \<in> set_cr;
paulson@14199
   201
    Nonce NonceCCA \<notin> used evs6;
paulson@14199
   202
    KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
paulson@14199
   203
    Notes (CA i) (Key cardSK) \<notin> set evs6;
paulson@14199
   204
    Gets (CA i)
paulson@14199
   205
      {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
paulson@14199
   206
                    Crypt (invKey cardSK)
paulson@14199
   207
                      (Hash {|Agent C, Nonce NC3, Key KC2,
paulson@14199
   208
			      Key cardSK, Pan (pan C), Nonce CardSecret|})|},
paulson@14199
   209
        Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
paulson@14199
   210
      \<in> set evs6 |]
paulson@14199
   211
==> Says (CA i) C
paulson@14199
   212
         (Crypt KC2
paulson@14199
   213
	  {|sign (priSK (CA i))
paulson@14199
   214
	         {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
paulson@14199
   215
	    certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
paulson@14199
   216
	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
paulson@14199
   217
      # Notes (CA i) (Key cardSK)
paulson@14199
   218
      # evs6 \<in> set_cr"
paulson@14199
   219
paulson@14199
   220
paulson@14199
   221
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14199
   222
declare parts.Body [dest]
paulson@14199
   223
declare analz_into_parts [dest]
paulson@14199
   224
declare Fake_parts_insert_in_Un [dest]
paulson@14199
   225
paulson@14199
   226
text{*A "possibility property": there are traces that reach the end.
paulson@14199
   227
      An unconstrained proof with many subgoals.*}
paulson@14199
   228
paulson@14199
   229
lemma Says_to_Gets:
paulson@14199
   230
     "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
paulson@14199
   231
by (rule set_cr.Reception, auto)
paulson@14199
   232
paulson@14199
   233
text{*The many nonces and keys generated, some simultaneously, force us to
paulson@14199
   234
  introduce them explicitly as shown below.*}
paulson@14199
   235
lemma possibility_CR6:
paulson@14199
   236
     "[|NC1 < (NC2::nat);  NC2 < NC3;  NC3 < NCA ;
paulson@14199
   237
        NCA < NonceCCA;  NonceCCA < CardSecret;
paulson@14199
   238
        KC1 < (KC2::key);  KC2 < KC3;
paulson@14199
   239
        KC1 \<in> symKeys;  Key KC1 \<notin> used [];
paulson@14199
   240
        KC2 \<in> symKeys;  Key KC2 \<notin> used [];
paulson@14199
   241
        KC3 \<in> symKeys;  Key KC3 \<notin> used [];
paulson@14199
   242
        C = Cardholder k|]
paulson@14199
   243
   ==> \<exists>evs \<in> set_cr.
paulson@14199
   244
       Says (CA i) C
paulson@14199
   245
            (Crypt KC2
paulson@14199
   246
             {|sign (priSK (CA i))
paulson@14199
   247
                    {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
paulson@14199
   248
               certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
paulson@14199
   249
                     onlySig (priSK (CA i)),
paulson@14199
   250
               cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
paulson@14199
   251
          \<in> set evs"
paulson@14199
   252
apply (intro exI bexI)
paulson@14206
   253
apply (rule_tac [2] 
paulson@14206
   254
       set_cr.Nil 
paulson@14206
   255
        [THEN set_cr.SET_CR1 [of concl: C i NC1], 
paulson@14206
   256
         THEN Says_to_Gets, 
paulson@14206
   257
	 THEN set_cr.SET_CR2 [of concl: i C NC1], 
paulson@14206
   258
	 THEN Says_to_Gets,  
paulson@14206
   259
	 THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2], 
paulson@14206
   260
	 THEN Says_to_Gets,  
paulson@14206
   261
	 THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], 
paulson@14206
   262
	 THEN Says_to_Gets,  
paulson@14206
   263
	 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
paulson@14206
   264
	 THEN Says_to_Gets,  
paulson@14206
   265
	 THEN set_cr.SET_CR6 [of concl: i C KC2]])
paulson@14206
   266
apply (tactic "basic_possibility_tac")
paulson@14199
   267
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
paulson@14199
   268
done
paulson@14199
   269
paulson@14199
   270
text{*General facts about message reception*}
paulson@14199
   271
lemma Gets_imp_Says:
paulson@14199
   272
     "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
paulson@14199
   273
apply (erule rev_mp)
paulson@14199
   274
apply (erule set_cr.induct, auto)
paulson@14199
   275
done
paulson@14199
   276
paulson@14199
   277
lemma Gets_imp_knows_Spy:
paulson@14199
   278
     "[| Gets B X \<in> set evs; evs \<in> set_cr |]  ==> X \<in> knows Spy evs"
paulson@14199
   279
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
paulson@14199
   280
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14199
   281
paulson@14199
   282
paulson@14199
   283
subsection{*Proofs on keys *}
paulson@14199
   284
paulson@14199
   285
text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
paulson@14199
   286
paulson@14199
   287
lemma Spy_see_private_Key [simp]:
paulson@14199
   288
     "evs \<in> set_cr
paulson@14199
   289
      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
paulson@14199
   290
by (erule set_cr.induct, auto)
paulson@14199
   291
paulson@14199
   292
lemma Spy_analz_private_Key [simp]:
paulson@14199
   293
     "evs \<in> set_cr ==>
paulson@14199
   294
     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
paulson@14199
   295
by auto
paulson@14199
   296
paulson@14199
   297
declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
paulson@14199
   298
declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
paulson@14199
   299
paulson@14199
   300
paulson@14199
   301
subsection{*Begin Piero's Theorems on Certificates*}
paulson@14199
   302
text{*Trivial in the current model, where certificates by RCA are secure *}
paulson@14199
   303
paulson@14199
   304
lemma Crypt_valid_pubEK:
paulson@14199
   305
     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
paulson@14199
   306
           \<in> parts (knows Spy evs);
paulson@14199
   307
         evs \<in> set_cr |] ==> EKi = pubEK C"
paulson@14199
   308
apply (erule rev_mp)
paulson@14199
   309
apply (erule set_cr.induct, auto)
paulson@14199
   310
done
paulson@14199
   311
paulson@14199
   312
lemma certificate_valid_pubEK:
paulson@14199
   313
    "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   314
        evs \<in> set_cr |]
paulson@14199
   315
     ==> EKi = pubEK C"
paulson@14199
   316
apply (unfold cert_def signCert_def)
paulson@14199
   317
apply (blast dest!: Crypt_valid_pubEK)
paulson@14199
   318
done
paulson@14199
   319
paulson@14199
   320
lemma Crypt_valid_pubSK:
paulson@14199
   321
     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
paulson@14199
   322
           \<in> parts (knows Spy evs);
paulson@14199
   323
         evs \<in> set_cr |] ==> SKi = pubSK C"
paulson@14199
   324
apply (erule rev_mp)
paulson@14199
   325
apply (erule set_cr.induct, auto)
paulson@14199
   326
done
paulson@14199
   327
paulson@14199
   328
lemma certificate_valid_pubSK:
paulson@14199
   329
    "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   330
        evs \<in> set_cr |] ==> SKi = pubSK C"
paulson@14199
   331
apply (unfold cert_def signCert_def)
paulson@14199
   332
apply (blast dest!: Crypt_valid_pubSK)
paulson@14199
   333
done
paulson@14199
   334
paulson@14199
   335
lemma Gets_certificate_valid:
paulson@14199
   336
     "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
paulson@14199
   337
                      cert C SKi onlySig (priSK RCA)|} \<in> set evs;
paulson@14199
   338
         evs \<in> set_cr |]
paulson@14199
   339
      ==> EKi = pubEK C & SKi = pubSK C"
paulson@14199
   340
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
paulson@14199
   341
paulson@14199
   342
text{*Nobody can have used non-existent keys!*}
paulson@14199
   343
lemma new_keys_not_used:
paulson@14199
   344
     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
paulson@14199
   345
      ==> K \<notin> keysFor (parts (knows Spy evs))"
paulson@14199
   346
apply (erule rev_mp)
paulson@14199
   347
apply (erule rev_mp)
paulson@14199
   348
apply (erule set_cr.induct)
paulson@14199
   349
apply (frule_tac [8] Gets_certificate_valid)
paulson@14199
   350
apply (frule_tac [6] Gets_certificate_valid, simp_all)
paulson@14218
   351
apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
paulson@14218
   352
apply (blast,auto)  --{*Others*}
paulson@14199
   353
done
paulson@14199
   354
paulson@14199
   355
paulson@14199
   356
subsection{*New versions: as above, but generalized to have the KK argument *}
paulson@14199
   357
paulson@14199
   358
lemma gen_new_keys_not_used:
paulson@14199
   359
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
paulson@14199
   360
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
paulson@14199
   361
          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
paulson@14199
   362
by (auto simp add: new_keys_not_used)
paulson@14199
   363
paulson@14199
   364
lemma gen_new_keys_not_analzd:
paulson@14199
   365
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
paulson@14199
   366
      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
paulson@14199
   367
by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
paulson@14199
   368
          dest: gen_new_keys_not_used)
paulson@14199
   369
paulson@14199
   370
lemma analz_Key_image_insert_eq:
paulson@14199
   371
     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
paulson@14199
   372
      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
paulson@14199
   373
          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
paulson@14199
   374
by (simp add: gen_new_keys_not_analzd)
paulson@14199
   375
paulson@14199
   376
lemma Crypt_parts_imp_used:
paulson@14199
   377
     "[|Crypt K X \<in> parts (knows Spy evs);
paulson@14199
   378
        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
paulson@14199
   379
apply (rule ccontr)
paulson@14199
   380
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
paulson@14199
   381
done
paulson@14199
   382
paulson@14199
   383
lemma Crypt_analz_imp_used:
paulson@14199
   384
     "[|Crypt K X \<in> analz (knows Spy evs);
paulson@14199
   385
        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
paulson@14199
   386
by (blast intro: Crypt_parts_imp_used)
paulson@14199
   387
paulson@14199
   388
paulson@14218
   389
(*<*) 
paulson@14199
   390
subsection{*Messages signed by CA*}
paulson@14199
   391
paulson@14199
   392
text{*Message @{text SET_CR2}: C can check CA's signature if he has received
paulson@14199
   393
     CA's certificate.*}
paulson@14199
   394
lemma CA_Says_2_lemma:
paulson@14199
   395
     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
paulson@14199
   396
           \<in> parts (knows Spy evs);
paulson@14199
   397
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   398
     ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
paulson@14199
   399
                 \<in> set evs"
paulson@14199
   400
apply (erule rev_mp)
paulson@14199
   401
apply (erule set_cr.induct, auto)
paulson@14199
   402
done
paulson@14199
   403
paulson@14199
   404
text{*Ever used?*}
paulson@14199
   405
lemma CA_Says_2:
paulson@14199
   406
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
paulson@14199
   407
           \<in> parts (knows Spy evs);
paulson@14199
   408
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   409
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   410
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
paulson@14199
   411
                  \<in> set evs"
paulson@14199
   412
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
paulson@14199
   413
paulson@14199
   414
paulson@14199
   415
text{*Message @{text SET_CR4}: C can check CA's signature if he has received
paulson@14199
   416
      CA's certificate.*}
paulson@14199
   417
lemma CA_Says_4_lemma:
paulson@14199
   418
     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
paulson@14199
   419
           \<in> parts (knows Spy evs);
paulson@14199
   420
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   421
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
paulson@14199
   422
                     {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
paulson@14199
   423
apply (erule rev_mp)
paulson@14199
   424
apply (erule set_cr.induct, auto)
paulson@14199
   425
done
paulson@14199
   426
paulson@14199
   427
text{*NEVER USED*}
paulson@14199
   428
lemma CA_Says_4:
paulson@14199
   429
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
paulson@14199
   430
           \<in> parts (knows Spy evs);
paulson@14199
   431
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   432
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   433
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
paulson@14199
   434
                   {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
paulson@14199
   435
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
paulson@14199
   436
paulson@14199
   437
paulson@14199
   438
text{*Message @{text SET_CR6}: C can check CA's signature if he has
paulson@14199
   439
      received CA's certificate.*}
paulson@14199
   440
lemma CA_Says_6_lemma:
paulson@14199
   441
     "[| Crypt (priSK (CA i)) 
paulson@14199
   442
               (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
paulson@14199
   443
           \<in> parts (knows Spy evs);
paulson@14199
   444
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   445
      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
paulson@14199
   446
      {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
paulson@14199
   447
apply (erule rev_mp)
paulson@14199
   448
apply (erule set_cr.induct, auto)
paulson@14199
   449
done
paulson@14199
   450
paulson@14199
   451
text{*NEVER USED*}
paulson@14199
   452
lemma CA_Says_6:
paulson@14199
   453
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
paulson@14199
   454
           \<in> parts (knows Spy evs);
paulson@14199
   455
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   456
         evs \<in> set_cr; (CA i) \<notin> bad |]
paulson@14199
   457
      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
paulson@14199
   458
                    {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
paulson@14199
   459
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
paulson@14218
   460
(*>*)
paulson@14199
   461
paulson@14199
   462
paulson@14199
   463
subsection{*Useful lemmas *}
paulson@14199
   464
paulson@14199
   465
text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
paulson@14199
   466
for other keys aren't needed.*}
paulson@14199
   467
paulson@14199
   468
lemma parts_image_priEK:
paulson@14199
   469
     "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
paulson@14199
   470
        evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
paulson@14199
   471
by auto
paulson@14199
   472
paulson@14199
   473
text{*trivial proof because (priEK C) never appears even in (parts evs)*}
paulson@14199
   474
lemma analz_image_priEK:
paulson@14199
   475
     "evs \<in> set_cr ==>
paulson@14199
   476
          (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   477
          (priEK C \<in> KK | C \<in> bad)"
paulson@14199
   478
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   479
paulson@14199
   480
paulson@14199
   481
subsection{*Secrecy of Session Keys *}
paulson@14199
   482
paulson@14199
   483
subsubsection{*Lemmas about the predicate KeyCryptKey *}
paulson@14199
   484
paulson@14199
   485
text{*A fresh DK cannot be associated with any other
paulson@14199
   486
  (with respect to a given trace). *}
paulson@14199
   487
lemma DK_fresh_not_KeyCryptKey:
paulson@14199
   488
     "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
paulson@14199
   489
apply (erule rev_mp)
paulson@14199
   490
apply (erule set_cr.induct)
paulson@14199
   491
apply (simp_all (no_asm_simp))
paulson@14199
   492
apply (blast dest: Crypt_analz_imp_used)+
paulson@14199
   493
done
paulson@14199
   494
paulson@14199
   495
text{*A fresh K cannot be associated with any other.  The assumption that
paulson@14199
   496
  DK isn't a private encryption key may be an artifact of the particular
paulson@14199
   497
  definition of KeyCryptKey.*}
paulson@14199
   498
lemma K_fresh_not_KeyCryptKey:
paulson@14199
   499
     "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
paulson@14199
   500
apply (induct evs)
paulson@14199
   501
apply (auto simp add: parts_insert2 split add: event.split)
paulson@14199
   502
done
paulson@14199
   503
paulson@14199
   504
paulson@14199
   505
text{*This holds because if (priEK (CA i)) appears in any traffic then it must
paulson@14199
   506
  be known to the Spy, by @{term Spy_see_private_Key}*}
paulson@14199
   507
lemma cardSK_neq_priEK:
paulson@14199
   508
     "[|Key cardSK \<notin> analz (knows Spy evs);
paulson@14199
   509
        Key cardSK : parts (knows Spy evs);
paulson@14199
   510
        evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
paulson@14199
   511
by blast
paulson@14199
   512
paulson@14199
   513
lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
paulson@14199
   514
     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
paulson@14199
   515
      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
paulson@14199
   516
by (erule set_cr.induct, analz_mono_contra, auto)
paulson@14199
   517
paulson@14199
   518
text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
paulson@14199
   519
lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
paulson@14199
   520
apply (induct_tac "evs")
paulson@14199
   521
apply (auto simp add: parts_insert2 split add: event.split)
paulson@14199
   522
done
paulson@14199
   523
paulson@14199
   524
text{*Lemma for message 6: either cardSK is compromised (when we don't care)
paulson@14199
   525
  or else cardSK hasn't been used to encrypt K.  Previously we treated
paulson@14199
   526
  message 5 in the same way, but the current model assumes that rule
paulson@14199
   527
  @{text SET_CR5} is executed only by honest agents.*}
paulson@14199
   528
lemma msg6_KeyCryptKey_disj:
paulson@14199
   529
     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
paulson@14199
   530
          \<in> set evs;
paulson@14199
   531
        cardSK \<notin> symKeys;  evs \<in> set_cr|]
paulson@14199
   532
      ==> Key cardSK \<in> analz (knows Spy evs) |
paulson@14199
   533
          (\<forall>K. ~ KeyCryptKey cardSK K evs)"
paulson@14199
   534
by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
paulson@14199
   535
paulson@14199
   536
text{*As usual: we express the property as a logical equivalence*}
paulson@14199
   537
lemma Key_analz_image_Key_lemma:
paulson@14199
   538
     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K \<in> KK | Key K \<in> analz H)
paulson@14199
   539
      ==>
paulson@14199
   540
      P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
paulson@14199
   541
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   542
paulson@14199
   543
ML
paulson@14199
   544
{*
paulson@14199
   545
val Gets_certificate_valid = thm "Gets_certificate_valid";
paulson@14199
   546
paulson@14199
   547
fun valid_certificate_tac i =
paulson@14199
   548
    EVERY [ftac Gets_certificate_valid i,
paulson@14199
   549
           assume_tac i,
paulson@14199
   550
           etac conjE i, REPEAT (hyp_subst_tac i)];
paulson@14199
   551
*}
paulson@14199
   552
paulson@14199
   553
text{*The @{text "(no_asm)"} attribute is essential, since it retains
paulson@14199
   554
  the quantifier and allows the simprule's condition to itself be simplified.*}
paulson@14199
   555
lemma symKey_compromise [rule_format (no_asm)]:
paulson@14199
   556
     "evs \<in> set_cr ==>
paulson@14199
   557
      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs)   -->
paulson@14199
   558
               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   559
               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
paulson@14199
   560
apply (erule set_cr.induct)
paulson@14199
   561
apply (rule_tac [!] allI) +
paulson@14199
   562
apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
paulson@14199
   563
apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
paulson@14199
   564
apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
paulson@14199
   565
apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
paulson@14199
   566
apply (simp_all
paulson@14199
   567
         del: image_insert image_Un imp_disjL
paulson@14199
   568
         add: analz_image_keys_simps analz_knows_absorb
paulson@14199
   569
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   570
              K_fresh_not_KeyCryptKey
paulson@14199
   571
              DK_fresh_not_KeyCryptKey ball_conj_distrib
paulson@14199
   572
              analz_image_priEK disj_simps)
paulson@14199
   573
  --{*46 seconds on a 1.8GHz machine*}
paulson@14199
   574
apply spy_analz
paulson@14218
   575
apply blast  --{*3*}
paulson@14218
   576
apply blast  --{*5*}
paulson@14199
   577
done
paulson@14199
   578
paulson@14199
   579
text{*The remaining quantifiers seem to be essential.
paulson@14199
   580
  NO NEED to assume the cardholder's OK: bad cardholders don't do anything
paulson@14199
   581
  wrong!!*}
paulson@14199
   582
lemma symKey_secrecy [rule_format]:
paulson@14199
   583
     "[|CA i \<notin> bad;  K \<in> symKeys;  evs \<in> set_cr|]
paulson@14199
   584
      ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
paulson@14199
   585
                Key K \<in> parts{X} -->
paulson@14199
   586
                Cardholder c \<notin> bad -->
paulson@14199
   587
                Key K \<notin> analz (knows Spy evs)"
paulson@14199
   588
apply (erule set_cr.induct)
paulson@14199
   589
apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
paulson@14199
   590
apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
paulson@14199
   591
apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
paulson@14199
   592
apply (simp_all del: image_insert image_Un imp_disjL
paulson@14199
   593
         add: symKey_compromise fresh_notin_analz_knows_Spy
paulson@14199
   594
              analz_image_keys_simps analz_knows_absorb
paulson@14199
   595
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   596
              K_fresh_not_KeyCryptKey
paulson@14199
   597
              DK_fresh_not_KeyCryptKey
paulson@14199
   598
              analz_image_priEK)
paulson@14199
   599
  --{*13 seconds on a 1.8GHz machine*}
paulson@14218
   600
apply spy_analz  --{*Fake*}
paulson@14199
   601
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
paulson@14199
   602
done
paulson@14199
   603
paulson@14199
   604
paulson@14199
   605
subsection{*Primary Goals of Cardholder Registration *}
paulson@14199
   606
paulson@14199
   607
text{*The cardholder's certificate really was created by the CA, provided the
paulson@14199
   608
    CA is uncompromised *}
paulson@14199
   609
paulson@14199
   610
text{*Lemma concerning the actual signed message digest*}
paulson@14199
   611
lemma cert_valid_lemma:
paulson@14199
   612
     "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
paulson@14199
   613
          \<in> parts (knows Spy evs);
paulson@14199
   614
        CA i \<notin> bad; evs \<in> set_cr|]
paulson@14199
   615
  ==> \<exists>KC2 X Y. Says (CA i) C
paulson@14199
   616
                     (Crypt KC2 
paulson@14199
   617
                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
paulson@14199
   618
                  \<in> set evs"
paulson@14199
   619
apply (erule rev_mp)
paulson@14199
   620
apply (erule set_cr.induct)
paulson@14199
   621
apply (simp_all (no_asm_simp))
paulson@14199
   622
apply auto
paulson@14199
   623
done
paulson@14199
   624
paulson@14199
   625
text{*Pre-packaged version for cardholder.  We don't try to confirm the values
paulson@14199
   626
  of KC2, X and Y, since they are not important.*}
paulson@14199
   627
lemma certificate_valid_cardSK:
paulson@14199
   628
    "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
paulson@14199
   629
                              cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
paulson@14199
   630
        CA i \<notin> bad; evs \<in> set_cr|]
paulson@14199
   631
  ==> \<exists>KC2 X Y. Says (CA i) C
paulson@14199
   632
                     (Crypt KC2 
paulson@14199
   633
                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
paulson@14199
   634
                   \<in> set evs"
paulson@14199
   635
by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
paulson@14199
   636
                    certificate_valid_pubSK cert_valid_lemma)
paulson@14199
   637
paulson@14199
   638
paulson@14199
   639
lemma Hash_imp_parts [rule_format]:
paulson@14199
   640
     "evs \<in> set_cr
paulson@14199
   641
      ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
paulson@14199
   642
          Nonce N \<in> parts (knows Spy evs)"
paulson@14199
   643
apply (erule set_cr.induct, force)
paulson@14199
   644
apply (simp_all (no_asm_simp))
paulson@14199
   645
apply (blast intro: parts_mono [THEN [2] rev_subsetD])
paulson@14199
   646
done
paulson@14199
   647
paulson@14199
   648
lemma Hash_imp_parts2 [rule_format]:
paulson@14199
   649
     "evs \<in> set_cr
paulson@14199
   650
      ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
paulson@14199
   651
          Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
paulson@14199
   652
apply (erule set_cr.induct, force)
paulson@14199
   653
apply (simp_all (no_asm_simp))
paulson@14199
   654
apply (blast intro: parts_mono [THEN [2] rev_subsetD])
paulson@14199
   655
done
paulson@14199
   656
paulson@14199
   657
paulson@14199
   658
subsection{*Secrecy of Nonces*}
paulson@14199
   659
paulson@14199
   660
subsubsection{*Lemmas about the predicate KeyCryptNonce *}
paulson@14199
   661
paulson@14199
   662
text{*A fresh DK cannot be associated with any other
paulson@14199
   663
  (with respect to a given trace). *}
paulson@14199
   664
lemma DK_fresh_not_KeyCryptNonce:
paulson@14199
   665
     "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
paulson@14199
   666
      ==> ~ KeyCryptNonce DK K evs"
paulson@14199
   667
apply (erule rev_mp)
paulson@14199
   668
apply (erule rev_mp)
paulson@14199
   669
apply (erule set_cr.induct)
paulson@14199
   670
apply (simp_all (no_asm_simp))
paulson@14199
   671
apply blast
paulson@14199
   672
apply blast
paulson@14199
   673
apply (auto simp add: DK_fresh_not_KeyCryptKey)
paulson@14199
   674
done
paulson@14199
   675
paulson@14199
   676
text{*A fresh N cannot be associated with any other
paulson@14199
   677
      (with respect to a given trace). *}
paulson@14199
   678
lemma N_fresh_not_KeyCryptNonce:
paulson@14199
   679
     "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
paulson@14199
   680
apply (induct_tac "evs")
paulson@14199
   681
apply (case_tac [2] "a")
paulson@14199
   682
apply (auto simp add: parts_insert2)
paulson@14199
   683
done
paulson@14199
   684
paulson@14199
   685
lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
paulson@14199
   686
     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
paulson@14199
   687
      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
paulson@14199
   688
apply (erule set_cr.induct, analz_mono_contra, simp_all)
paulson@14218
   689
apply (blast dest: not_KeyCryptKey_cardSK)  --{*6*}
paulson@14199
   690
done
paulson@14199
   691
paulson@14199
   692
subsubsection{*Lemmas for message 5 and 6:
paulson@14199
   693
  either cardSK is compromised (when we don't care)
paulson@14199
   694
  or else cardSK hasn't been used to encrypt K. *}
paulson@14199
   695
paulson@14199
   696
text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
paulson@14199
   697
lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
paulson@14199
   698
apply (induct_tac "evs")
paulson@14199
   699
apply (auto simp add: parts_insert2 split add: event.split)
paulson@14199
   700
done
paulson@14199
   701
paulson@14199
   702
text{*Lemma for message 6: either cardSK is compromised (when we don't care)
paulson@14199
   703
  or else cardSK hasn't been used to encrypt K.*}
paulson@14199
   704
lemma msg6_KeyCryptNonce_disj:
paulson@14199
   705
     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
paulson@14199
   706
          \<in> set evs;
paulson@14199
   707
        cardSK \<notin> symKeys;  evs \<in> set_cr|]
paulson@14199
   708
      ==> Key cardSK \<in> analz (knows Spy evs) |
paulson@14199
   709
          ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
paulson@14199
   710
           (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
paulson@14199
   711
by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
paulson@14199
   712
          intro: cardSK_neq_priEK)
paulson@14199
   713
paulson@14199
   714
paulson@14199
   715
text{*As usual: we express the property as a logical equivalence*}
paulson@14199
   716
lemma Nonce_analz_image_Key_lemma:
paulson@14199
   717
     "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
paulson@14199
   718
      ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
paulson@14199
   719
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   720
paulson@14199
   721
text{*The @{text "(no_asm)"} attribute is essential, since it retains
paulson@14199
   722
  the quantifier and allows the simprule's condition to itself be simplified.*}
paulson@14199
   723
lemma Nonce_compromise [rule_format (no_asm)]:
paulson@14199
   724
     "evs \<in> set_cr ==>
paulson@14199
   725
      (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs)   -->
paulson@14199
   726
               (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   727
               (Nonce N \<in> analz (knows Spy evs)))"
paulson@14199
   728
apply (erule set_cr.induct)
paulson@14199
   729
apply (rule_tac [!] allI)+
paulson@14199
   730
apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
paulson@14199
   731
apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
paulson@14199
   732
apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
paulson@14199
   733
apply (frule_tac [11] msg6_KeyCryptNonce_disj)
paulson@14199
   734
apply (erule_tac [13] disjE)
paulson@14199
   735
apply (simp_all del: image_insert image_Un
paulson@14199
   736
         add: symKey_compromise
paulson@14199
   737
              analz_image_keys_simps analz_knows_absorb
paulson@14199
   738
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   739
              N_fresh_not_KeyCryptNonce
paulson@14199
   740
              DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
paulson@14199
   741
              ball_conj_distrib analz_image_priEK)
paulson@14199
   742
  --{*71 seconds on a 1.8GHz machine*}
paulson@14218
   743
apply spy_analz  --{*Fake*}
paulson@14218
   744
apply blast  --{*3*}
paulson@14218
   745
apply blast  --{*5*}
paulson@14218
   746
txt{*Message 6*}
paulson@14199
   747
apply (force del: allE ballE impCE simp add: symKey_compromise)
paulson@14218
   748
  --{*cardSK compromised*}
paulson@14199
   749
txt{*Simplify again--necessary because the previous simplification introduces
paulson@14199
   750
  some logical connectives*}
paulson@14218
   751
apply (force del: allE ballE impCE
paulson@14199
   752
          simp del: image_insert image_Un imp_disjL
paulson@14199
   753
          simp add: analz_image_keys_simps symKey_compromise)
paulson@14218
   754
done
paulson@14199
   755
paulson@14199
   756
paulson@14199
   757
subsection{*Secrecy of CardSecret: the Cardholder's secret*}
paulson@14199
   758
paulson@14199
   759
lemma NC2_not_CardSecret:
paulson@14199
   760
     "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
paulson@14199
   761
          \<in> parts (knows Spy evs);
paulson@14199
   762
        Key K \<notin> analz (knows Spy evs);
paulson@14199
   763
        Nonce N \<notin> analz (knows Spy evs);
paulson@14199
   764
       evs \<in> set_cr|]
paulson@14199
   765
      ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
paulson@14199
   766
apply (erule rev_mp)
paulson@14199
   767
apply (erule rev_mp)
paulson@14199
   768
apply (erule rev_mp)
paulson@14199
   769
apply (erule set_cr.induct, analz_mono_contra, simp_all)
paulson@14199
   770
apply (blast dest: Hash_imp_parts)+
paulson@14199
   771
done
paulson@14199
   772
paulson@14199
   773
lemma KC2_secure_lemma [rule_format]:
paulson@14199
   774
     "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
paulson@14199
   775
        U \<in> parts (knows Spy evs);
paulson@14199
   776
        evs \<in> set_cr|]
paulson@14199
   777
  ==> Nonce N \<notin> analz (knows Spy evs) -->
paulson@14199
   778
      (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
paulson@14199
   779
               Cardholder k \<notin> bad & CA i \<notin> bad)"
paulson@14199
   780
apply (erule_tac P = "U \<in> ?H" in rev_mp)
paulson@14199
   781
apply (erule set_cr.induct)
paulson@14199
   782
apply (tactic{*valid_certificate_tac 8*})  --{*for message 5*}
paulson@14199
   783
apply (simp_all del: image_insert image_Un imp_disjL
paulson@14199
   784
         add: analz_image_keys_simps analz_knows_absorb
paulson@14199
   785
              analz_knows_absorb2 notin_image_iff)
paulson@14199
   786
  --{*19 seconds on a 1.8GHz machine*}
paulson@14199
   787
apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
paulson@14199
   788
apply (blast intro!: analz_insertI)+
paulson@14199
   789
done
paulson@14199
   790
paulson@14199
   791
lemma KC2_secrecy:
paulson@14199
   792
     "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
paulson@14199
   793
        Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
paulson@14199
   794
        evs \<in> set_cr|]
paulson@14199
   795
       ==> Key KC2 \<notin> analz (knows Spy evs)"
paulson@14199
   796
by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
paulson@14199
   797
paulson@14199
   798
paulson@14199
   799
text{*Inductive version*}
paulson@14199
   800
lemma CardSecret_secrecy_lemma [rule_format]:
paulson@14199
   801
     "[|CA i \<notin> bad;  evs \<in> set_cr|]
paulson@14199
   802
      ==> Key K \<notin> analz (knows Spy evs) -->
paulson@14199
   803
          Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
paulson@14199
   804
             \<in> parts (knows Spy evs) -->
paulson@14199
   805
          Nonce CardSecret \<notin> analz (knows Spy evs)"
paulson@14199
   806
apply (erule set_cr.induct, analz_mono_contra)
paulson@14199
   807
apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
paulson@14199
   808
apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
paulson@14199
   809
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
paulson@14199
   810
apply (simp_all
paulson@14199
   811
         del: image_insert image_Un imp_disjL
paulson@14199
   812
         add: analz_image_keys_simps analz_knows_absorb
paulson@14199
   813
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   814
              EXHcrypt_def Crypt_notin_image_Key
paulson@14199
   815
              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
paulson@14199
   816
              ball_conj_distrib Nonce_compromise symKey_compromise
paulson@14199
   817
              analz_image_priEK)
paulson@14199
   818
  --{*12 seconds on a 1.8GHz machine*}
paulson@14218
   819
apply spy_analz  --{*Fake*}
paulson@14199
   820
apply (simp_all (no_asm_simp))
paulson@14218
   821
apply blast  --{*1*}
paulson@14218
   822
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
paulson@14218
   823
apply blast  --{*3*}
paulson@14218
   824
apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)  --{*4*}
paulson@14218
   825
apply blast  --{*5*}
paulson@14218
   826
apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
paulson@14199
   827
done
paulson@14199
   828
paulson@14199
   829
paulson@14199
   830
text{*Packaged version for cardholder*}
paulson@14199
   831
lemma CardSecret_secrecy:
paulson@14199
   832
     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
paulson@14199
   833
        Says (Cardholder k) (CA i)
paulson@14199
   834
           {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
paulson@14199
   835
        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
paulson@14199
   836
                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
paulson@14199
   837
        KC3 \<in> symKeys;  evs \<in> set_cr|]
paulson@14199
   838
      ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
paulson@14199
   839
apply (frule Gets_certificate_valid, assumption)
paulson@14199
   840
apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
paulson@14199
   841
apply (blast dest: CardSecret_secrecy_lemma)
paulson@14199
   842
apply (rule symKey_secrecy)
paulson@14199
   843
apply (auto simp add: parts_insert2)
paulson@14199
   844
done
paulson@14199
   845
paulson@14199
   846
paulson@14199
   847
subsection{*Secrecy of NonceCCA [the CA's secret] *}
paulson@14199
   848
paulson@14199
   849
lemma NC2_not_NonceCCA:
paulson@14199
   850
     "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
paulson@14199
   851
          \<in> parts (knows Spy evs);
paulson@14199
   852
        Nonce N \<notin> analz (knows Spy evs);
paulson@14199
   853
       evs \<in> set_cr|]
paulson@14199
   854
      ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
paulson@14199
   855
apply (erule rev_mp)
paulson@14199
   856
apply (erule rev_mp)
paulson@14199
   857
apply (erule set_cr.induct, analz_mono_contra, simp_all)
paulson@14199
   858
apply (blast dest: Hash_imp_parts2)+
paulson@14199
   859
done
paulson@14199
   860
paulson@14199
   861
paulson@14199
   862
text{*Inductive version*}
paulson@14199
   863
lemma NonceCCA_secrecy_lemma [rule_format]:
paulson@14199
   864
     "[|CA i \<notin> bad;  evs \<in> set_cr|]
paulson@14199
   865
      ==> Key K \<notin> analz (knows Spy evs) -->
paulson@14199
   866
          Crypt K
paulson@14199
   867
            {|sign (priSK (CA i))
paulson@14199
   868
                   {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
paulson@14199
   869
              X, Y|}
paulson@14199
   870
             \<in> parts (knows Spy evs) -->
paulson@14199
   871
          Nonce NonceCCA \<notin> analz (knows Spy evs)"
paulson@14199
   872
apply (erule set_cr.induct, analz_mono_contra)
paulson@14199
   873
apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
paulson@14199
   874
apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
paulson@14199
   875
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
paulson@14199
   876
apply (simp_all
paulson@14199
   877
         del: image_insert image_Un imp_disjL
paulson@14199
   878
         add: analz_image_keys_simps analz_knows_absorb sign_def
paulson@14199
   879
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   880
              EXHcrypt_def Crypt_notin_image_Key
paulson@14199
   881
              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
paulson@14199
   882
              ball_conj_distrib Nonce_compromise symKey_compromise
paulson@14199
   883
              analz_image_priEK)
paulson@14199
   884
  --{*15 seconds on a 1.8GHz machine*}
paulson@14218
   885
apply spy_analz  --{*Fake*}
paulson@14218
   886
apply blast  --{*1*}
paulson@14218
   887
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
paulson@14218
   888
apply blast  --{*3*}
paulson@14218
   889
apply (blast dest: NC2_not_NonceCCA)  --{*4*}
paulson@14218
   890
apply blast  --{*5*}
paulson@14218
   891
apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
paulson@14199
   892
done
paulson@14199
   893
paulson@14199
   894
paulson@14199
   895
text{*Packaged version for cardholder*}
paulson@14199
   896
lemma NonceCCA_secrecy:
paulson@14199
   897
     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
paulson@14199
   898
        Gets (Cardholder k)
paulson@14199
   899
           (Crypt KC2
paulson@14199
   900
            {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
paulson@14199
   901
              X, Y|}) \<in> set evs;
paulson@14199
   902
        Says (Cardholder k) (CA i)
paulson@14199
   903
           {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
paulson@14199
   904
        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
paulson@14199
   905
                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
paulson@14199
   906
        KC2 \<in> symKeys;  evs \<in> set_cr|]
paulson@14199
   907
      ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
paulson@14199
   908
apply (frule Gets_certificate_valid, assumption)
paulson@14199
   909
apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
paulson@14199
   910
apply (blast dest: NonceCCA_secrecy_lemma)
paulson@14199
   911
apply (rule symKey_secrecy)
paulson@14199
   912
apply (auto simp add: parts_insert2)
paulson@14199
   913
done
paulson@14199
   914
paulson@14199
   915
text{*We don't bother to prove guarantees for the CA.  He doesn't care about
paulson@14199
   916
  the PANSecret: it isn't his credit card!*}
paulson@14199
   917
paulson@14199
   918
paulson@14199
   919
subsection{*Rewriting Rule for PANs*}
paulson@14199
   920
paulson@14199
   921
text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
paulson@14199
   922
  or if it is then (because it appears in traffic) that CA is bad,
paulson@14199
   923
  and so the Spy knows that key already.  Either way, we can simplify
paulson@14199
   924
  the expression @{term "analz (insert (Key cardSK) X)"}.*}
paulson@14199
   925
lemma msg6_cardSK_disj:
paulson@14199
   926
     "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
paulson@14199
   927
          \<in> set evs;  evs \<in> set_cr |]
paulson@14199
   928
      ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
paulson@14199
   929
by auto
paulson@14199
   930
paulson@14199
   931
lemma analz_image_pan_lemma:
paulson@14199
   932
     "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
paulson@14199
   933
      (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
paulson@14199
   934
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   935
paulson@14199
   936
lemma analz_image_pan [rule_format]:
paulson@14199
   937
     "evs \<in> set_cr ==>
paulson@14199
   938
       \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
paulson@14199
   939
            (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   940
            (Pan P \<in> analz (knows Spy evs))"
paulson@14199
   941
apply (erule set_cr.induct)
paulson@14199
   942
apply (rule_tac [!] allI impI)+
paulson@14199
   943
apply (rule_tac [!] analz_image_pan_lemma)
paulson@14199
   944
apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
paulson@14199
   945
apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
paulson@14199
   946
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
paulson@14199
   947
apply (simp_all
paulson@14199
   948
         del: image_insert image_Un
paulson@14199
   949
         add: analz_image_keys_simps disjoint_image_iff
paulson@14199
   950
              notin_image_iff analz_image_priEK)
paulson@14199
   951
  --{*33 seconds on a 1.8GHz machine*}
paulson@14199
   952
apply spy_analz
paulson@14218
   953
apply (simp add: insert_absorb)  --{*6*}
paulson@14199
   954
done
paulson@14199
   955
paulson@14199
   956
lemma analz_insert_pan:
paulson@14199
   957
     "[| evs \<in> set_cr;  K \<notin> invKey ` pubEK ` range CA |] ==>
paulson@14199
   958
          (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
paulson@14199
   959
          (Pan P \<in> analz (knows Spy evs))"
paulson@14199
   960
by (simp del: image_insert image_Un
paulson@14199
   961
         add: analz_image_keys_simps analz_image_pan)
paulson@14199
   962
paulson@14199
   963
paulson@14199
   964
text{*Confidentiality of the PAN\@.  Maybe we could combine the statements of
paulson@14199
   965
  this theorem with @{term analz_image_pan}, requiring a single induction but
paulson@14199
   966
  a much more difficult proof.*}
paulson@14199
   967
lemma pan_confidentiality:
paulson@14199
   968
     "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
paulson@14199
   969
    ==> \<exists>i X K HN.
paulson@14199
   970
        Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
paulson@14199
   971
           \<in> set evs
paulson@14199
   972
      & (CA i) \<in> bad"
paulson@14199
   973
apply (erule rev_mp)
paulson@14199
   974
apply (erule set_cr.induct)
paulson@14199
   975
apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
paulson@14199
   976
apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
paulson@14199
   977
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
paulson@14199
   978
apply (simp_all
paulson@14199
   979
         del: image_insert image_Un
paulson@14199
   980
         add: analz_image_keys_simps analz_insert_pan analz_image_pan
paulson@14199
   981
              notin_image_iff analz_image_priEK)
paulson@14199
   982
  --{*18 seconds on a 1.8GHz machine*}
paulson@14218
   983
apply spy_analz  --{*fake*}
paulson@14218
   984
apply blast  --{*3*}
paulson@14218
   985
apply blast  --{*5*}
paulson@14218
   986
apply (simp (no_asm_simp) add: insert_absorb)  --{*6*}
paulson@14199
   987
done
paulson@14199
   988
paulson@14199
   989
paulson@14199
   990
subsection{*Unicity*}
paulson@14199
   991
paulson@14199
   992
lemma CR6_Says_imp_Notes:
paulson@14199
   993
     "[|Says (CA i) C (Crypt KC2
paulson@14199
   994
          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
paulson@14199
   995
            certC (pan C) cardSK X onlySig (priSK (CA i)),
paulson@14199
   996
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
paulson@14199
   997
        evs \<in> set_cr |]
paulson@14199
   998
      ==> Notes (CA i) (Key cardSK) \<in> set evs"
paulson@14199
   999
apply (erule rev_mp)
paulson@14199
  1000
apply (erule set_cr.induct)
paulson@14199
  1001
apply (simp_all (no_asm_simp))
paulson@14199
  1002
done
paulson@14199
  1003
paulson@14199
  1004
text{*Unicity of cardSK: it uniquely identifies the other components.  
paulson@14199
  1005
      This holds because a CA accepts a cardSK at most once.*}
paulson@14199
  1006
lemma cardholder_key_unicity:
paulson@14199
  1007
     "[|Says (CA i) C (Crypt KC2
paulson@14199
  1008
          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
paulson@14199
  1009
            certC (pan C) cardSK X onlySig (priSK (CA i)),
paulson@14199
  1010
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
paulson@14199
  1011
          \<in> set evs;
paulson@14199
  1012
        Says (CA i) C' (Crypt KC2'
paulson@14199
  1013
          {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
paulson@14199
  1014
            certC (pan C') cardSK X' onlySig (priSK (CA i)),
paulson@14199
  1015
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
paulson@14199
  1016
          \<in> set evs;
paulson@14199
  1017
        evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
paulson@14199
  1018
apply (erule rev_mp)
paulson@14199
  1019
apply (erule rev_mp)
paulson@14199
  1020
apply (erule set_cr.induct)
paulson@14199
  1021
apply (simp_all (no_asm_simp))
paulson@14199
  1022
apply (blast dest!: CR6_Says_imp_Notes)
paulson@14199
  1023
done
paulson@14199
  1024
paulson@14199
  1025
paulson@14218
  1026
(*<*)
paulson@14199
  1027
text{*UNUSED unicity result*}
paulson@14199
  1028
lemma unique_KC1:
paulson@14199
  1029
     "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
paulson@14199
  1030
          \<in> set evs;
paulson@14199
  1031
        Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
paulson@14199
  1032
          \<in> set evs;
paulson@14199
  1033
        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
paulson@14199
  1034
apply (erule rev_mp)
paulson@14199
  1035
apply (erule rev_mp)
paulson@14199
  1036
apply (erule set_cr.induct, auto)
paulson@14199
  1037
done
paulson@14199
  1038
paulson@14199
  1039
text{*UNUSED unicity result*}
paulson@14199
  1040
lemma unique_KC2:
paulson@14199
  1041
     "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
paulson@14199
  1042
        Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
paulson@14199
  1043
        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
paulson@14199
  1044
apply (erule rev_mp)
paulson@14199
  1045
apply (erule rev_mp)
paulson@14199
  1046
apply (erule set_cr.induct, auto)
paulson@14199
  1047
done
paulson@14218
  1048
(*>*)
paulson@14218
  1049
paulson@14199
  1050
paulson@14199
  1051
text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
paulson@14199
  1052
  it could be a previously compromised cardSK [e.g. involving a bad CA]*}
paulson@14199
  1053
paulson@14199
  1054
paulson@14199
  1055
end