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