new session HOL-SET-Protocol
authorpaulson
Tue Sep 23 15:40:27 2003 +0200 (2003-09-23)
changeset 14199d3b8d972a488
parent 14198 8ea2645b8132
child 14200 d8598e24f8fa
new session HOL-SET-Protocol
NEWS
src/HOL/IsaMakefile
src/HOL/SET-Protocol/Cardholder_Registration.thy
src/HOL/SET-Protocol/EventSET.thy
src/HOL/SET-Protocol/Merchant_Registration.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/SET-Protocol/Purchase.thy
src/HOL/SET-Protocol/ROOT.ML
src/HOL/SET-Protocol/document/root.tex
     1.1 --- a/NEWS	Mon Sep 22 16:19:46 2003 +0200
     1.2 +++ b/NEWS	Tue Sep 23 15:40:27 2003 +0200
     1.3 @@ -38,6 +38,8 @@
     1.4  * 'specification' command added, allowing for definition by
     1.5  specification.
     1.6  
     1.7 +* SET-Protocol: formalization and verification of the SET protocol suite;
     1.8 +
     1.9  
    1.10  New in Isabelle2003 (May 2003)
    1.11  --------------------------------
     2.1 --- a/src/HOL/IsaMakefile	Mon Sep 22 16:19:46 2003 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Sep 23 15:40:27 2003 +0200
     2.3 @@ -35,6 +35,7 @@
     2.4    HOL-NanoJava \
     2.5    HOL-NumberTheory \
     2.6    HOL-Prolog \
     2.7 +  HOL-SET-Protocol \
     2.8    HOL-Subst \
     2.9        TLA-Buffer \
    2.10        TLA-Inc \
    2.11 @@ -386,8 +387,7 @@
    2.12    UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
    2.13    UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
    2.14    UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
    2.15 -  UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy  \
    2.16 -  UNITY/Simple/Network.thy\
    2.17 +  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
    2.18    UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
    2.19    UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
    2.20    UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
    2.21 @@ -615,6 +615,22 @@
    2.22  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    2.23  
    2.24  
    2.25 +## HOL-SET-Protocol
    2.26 +
    2.27 +HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
    2.28 +
    2.29 +$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
    2.30 +  SET-Protocol/MessageSET.thy\
    2.31 +  SET-Protocol/EventSET.thy\
    2.32 +  SET-Protocol/PublicSET.thy\
    2.33 +  SET-Protocol/Cardholder_Registration.thy\
    2.34 +  SET-Protocol/Merchant_Registration.thy\
    2.35 +  SET-Protocol/Purchase.thy\
    2.36 +  SET-Protocol/document/root.tex 
    2.37 +	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
    2.38 +
    2.39 +
    2.40 +
    2.41  ## TLA
    2.42  
    2.43  TLA: HOL $(OUT)/TLA
    2.44 @@ -679,6 +695,6 @@
    2.45  		$(LOG)/HOL-Lattice \
    2.46  		$(LOG)/HOL-Complex.gz \
    2.47  		$(LOG)/HOL-Complex-ex.gz \
    2.48 -		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/TLA-Inc.gz \
    2.49 -		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
    2.50 +		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
    2.51 +                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
    2.52  		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz 
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Tue Sep 23 15:40:27 2003 +0200
     3.3 @@ -0,0 +1,1084 @@
     3.4 +(*  Title:      HOL/Auth/SET/Cardholder_Registration
     3.5 +    ID:         $Id$
     3.6 +    Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
     3.7 +                Piero Tramontano
     3.8 +*)
     3.9 +
    3.10 +header{*The SET Cardholder Registration Protocol*}
    3.11 +
    3.12 +theory Cardholder_Registration = PublicSET:
    3.13 +
    3.14 +text{*Note: nonces seem to consist of 20 bytes.  That includes both freshness
    3.15 +challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
    3.16 +*}
    3.17 +
    3.18 +text{*Simplifications involving @{text analz_image_keys_simps} appear to
    3.19 +have become much slower. The cause is unclear. However, there is a big blow-up
    3.20 +and the rewriting is very sensitive to the set of rewrite rules given.*}
    3.21 +
    3.22 +subsection{*Predicate Formalizing the Encryption Association between Keys *}
    3.23 +
    3.24 +consts
    3.25 +  KeyCryptKey :: "[key, key, event list] => bool"
    3.26 +
    3.27 +primrec
    3.28 +
    3.29 +KeyCryptKey_Nil:
    3.30 +  "KeyCryptKey DK K [] = False"
    3.31 +
    3.32 +KeyCryptKey_Cons:
    3.33 +      --{*Says is the only important case.
    3.34 +	1st case: CR5, where KC3 encrypts KC2.
    3.35 +	2nd case: any use of priEK C.
    3.36 +	Revision 1.12 has a more complicated version with separate treatment of
    3.37 +	  the dependency of KC1, KC2 and KC3 on priEK (CA i.)  Not needed since
    3.38 +	  priEK C is never sent (and so can't be lost except at the start). *}
    3.39 +  "KeyCryptKey DK K (ev # evs) =
    3.40 +   (KeyCryptKey DK K evs |
    3.41 +    (case ev of
    3.42 +      Says A B Z =>
    3.43 +       ((\<exists>N X Y. A \<noteq> Spy &
    3.44 +	         DK \<in> symKeys &
    3.45 +		 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
    3.46 +	(\<exists>C. DK = priEK C))
    3.47 +    | Gets A' X => False
    3.48 +    | Notes A' X => False))"
    3.49 +
    3.50 +
    3.51 +subsection{*Predicate formalizing the association between keys and nonces *}
    3.52 +
    3.53 +consts
    3.54 +  KeyCryptNonce :: "[key, key, event list] => bool"
    3.55 +
    3.56 +primrec
    3.57 +
    3.58 +KeyCryptNonce_Nil:
    3.59 +  "KeyCryptNonce EK K [] = False"
    3.60 +
    3.61 +KeyCryptNonce_Cons:
    3.62 +  --{*Says is the only important case.
    3.63 +    1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
    3.64 +    2nd case: CR5, where KC3 encrypts NC3;
    3.65 +    3rd case: CR6, where KC2 encrypts NC3;
    3.66 +    4th case: CR6, where KC2 encrypts NonceCCA;
    3.67 +    5th case: any use of @{term "priEK C"} (including CardSecret).
    3.68 +    NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
    3.69 +    But we can't prove @{text Nonce_compromise} unless the relation covers ALL
    3.70 +	nonces that the protocol keeps secret.
    3.71 +  *}
    3.72 +  "KeyCryptNonce DK N (ev # evs) =
    3.73 +   (KeyCryptNonce DK N evs |
    3.74 +    (case ev of
    3.75 +      Says A B Z =>
    3.76 +       A \<noteq> Spy &
    3.77 +       ((\<exists>X Y. DK \<in> symKeys &
    3.78 +	       Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
    3.79 +	(\<exists>X Y. DK \<in> symKeys &
    3.80 +	       Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
    3.81 +	(\<exists>K i X Y.
    3.82 +	  K \<in> symKeys &
    3.83 +          Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
    3.84 +	  (DK=K | KeyCryptKey DK K evs)) |
    3.85 +	(\<exists>K C NC3 Y.
    3.86 +	  K \<in> symKeys &
    3.87 +          Z = Crypt K
    3.88 + 	        {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
    3.89 +                  Y|} &
    3.90 +	  (DK=K | KeyCryptKey DK K evs)) |
    3.91 +	(\<exists>C. DK = priEK C))
    3.92 +    | Gets A' X => False
    3.93 +    | Notes A' X => False))"
    3.94 +
    3.95 +
    3.96 +subsection{*Formal protocol definition *}
    3.97 +
    3.98 +consts  set_cr  :: "event list set"
    3.99 +inductive set_cr
   3.100 + intros
   3.101 +
   3.102 +  Nil:    --{*Initial trace is empty*}
   3.103 +	  "[] \<in> set_cr"
   3.104 +
   3.105 +  Fake:    --{*The spy MAY say anything he CAN say.*}
   3.106 +	   "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
   3.107 +	    ==> Says Spy B X  # evsf \<in> set_cr"
   3.108 +
   3.109 +  Reception: --{*If A sends a message X to B, then B might receive it*}
   3.110 +	     "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
   3.111 +              ==> Gets B X  # evsr \<in> set_cr"
   3.112 +
   3.113 +  SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
   3.114 +	     "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
   3.115 +	      ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
   3.116 +
   3.117 +  SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
   3.118 +	     "[| evs2 \<in> set_cr;
   3.119 +		 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
   3.120 +	      ==> Says (CA i) C
   3.121 +		       {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
   3.122 +			 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
   3.123 +			 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   3.124 +		    # evs2 \<in> set_cr"
   3.125 +
   3.126 +  SET_CR3:
   3.127 +   --{*RegFormReq: C sends his PAN and a new nonce to CA.
   3.128 +   C verifies that
   3.129 +    - nonce received is the same as that sent;
   3.130 +    - certificates are signed by RCA;
   3.131 +    - certificates are an encryption certificate (flag is onlyEnc) and a
   3.132 +      signature certificate (flag is onlySig);
   3.133 +    - certificates pertain to the CA that C contacted (this is done by
   3.134 +      checking the signature).
   3.135 +   C generates a fresh symmetric key KC1.
   3.136 +   The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
   3.137 +   is not clear. *}
   3.138 +"[| evs3 \<in> set_cr;  C = Cardholder k;
   3.139 +    Nonce NC2 \<notin> used evs3;
   3.140 +    Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
   3.141 +    Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
   3.142 +	     cert (CA i) EKi onlyEnc (priSK RCA),
   3.143 +	     cert (CA i) SKi onlySig (priSK RCA)|}
   3.144 +       \<in> set evs3;
   3.145 +    Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
   3.146 + ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
   3.147 +       # Notes C {|Key KC1, Agent (CA i)|}
   3.148 +       # evs3 \<in> set_cr"
   3.149 +
   3.150 +  SET_CR4:
   3.151 +    --{*RegFormRes:
   3.152 +    CA responds sending NC2 back with a new nonce NCA, after checking that
   3.153 +     - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
   3.154 +     - the entire message is encrypted with the same key found inside the
   3.155 +       envelope (here, KC1) *}
   3.156 +"[| evs4 \<in> set_cr;
   3.157 +    Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
   3.158 +    Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
   3.159 +       \<in> set evs4 |]
   3.160 +  ==> Says (CA i) C
   3.161 +	  {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
   3.162 +	    cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
   3.163 +	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   3.164 +       # evs4 \<in> set_cr"
   3.165 +
   3.166 +  SET_CR5:
   3.167 +   --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
   3.168 +       and its half of the secret value to CA.
   3.169 +       We now assume that C has a fixed key pair, and he submits (pubSK C).
   3.170 +       The protocol does not require this key to be fresh.
   3.171 +       The encryption below is actually EncX.*}
   3.172 +"[| evs5 \<in> set_cr;  C = Cardholder k;
   3.173 +    Nonce NC3 \<notin> used evs5;  Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
   3.174 +    Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
   3.175 +    Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
   3.176 +    Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
   3.177 +             cert (CA i) EKi onlyEnc (priSK RCA),
   3.178 +             cert (CA i) SKi onlySig (priSK RCA) |}
   3.179 +        \<in> set evs5;
   3.180 +    Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
   3.181 +         \<in> set evs5 |]
   3.182 +==> Says C (CA i)
   3.183 +         {|Crypt KC3
   3.184 +	     {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
   3.185 +	       Crypt (priSK C)
   3.186 +	         (Hash {|Agent C, Nonce NC3, Key KC2,
   3.187 +			 Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
   3.188 +           Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
   3.189 +    # Notes C {|Key KC2, Agent (CA i)|}
   3.190 +    # Notes C {|Key KC3, Agent (CA i)|}
   3.191 +    # evs5 \<in> set_cr"
   3.192 +
   3.193 +
   3.194 +  --{* CertRes: CA responds sending NC3 back with its half of the secret value,
   3.195 +   its signature certificate and the new cardholder signature
   3.196 +   certificate.  CA checks to have never certified the key proposed by C.
   3.197 +   NOTE: In Merchant Registration, the corresponding rule (4)
   3.198 +   uses the "sign" primitive. The encryption below is actually @{term EncK}, 
   3.199 +   which is just @{term "Crypt K (sign SK X)"}.
   3.200 +*}
   3.201 +
   3.202 +SET_CR6:
   3.203 +"[| evs6 \<in> set_cr;
   3.204 +    Nonce NonceCCA \<notin> used evs6;
   3.205 +    KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
   3.206 +    Notes (CA i) (Key cardSK) \<notin> set evs6;
   3.207 +    Gets (CA i)
   3.208 +      {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
   3.209 +                    Crypt (invKey cardSK)
   3.210 +                      (Hash {|Agent C, Nonce NC3, Key KC2,
   3.211 +			      Key cardSK, Pan (pan C), Nonce CardSecret|})|},
   3.212 +        Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
   3.213 +      \<in> set evs6 |]
   3.214 +==> Says (CA i) C
   3.215 +         (Crypt KC2
   3.216 +	  {|sign (priSK (CA i))
   3.217 +	         {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
   3.218 +	    certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
   3.219 +	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
   3.220 +      # Notes (CA i) (Key cardSK)
   3.221 +      # evs6 \<in> set_cr"
   3.222 +
   3.223 +
   3.224 +declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   3.225 +declare parts.Body [dest]
   3.226 +declare analz_into_parts [dest]
   3.227 +declare Fake_parts_insert_in_Un [dest]
   3.228 +
   3.229 +text{*A "possibility property": there are traces that reach the end.
   3.230 +      An unconstrained proof with many subgoals.*}
   3.231 +
   3.232 +lemma Says_to_Gets:
   3.233 +     "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
   3.234 +by (rule set_cr.Reception, auto)
   3.235 +
   3.236 +text{*The many nonces and keys generated, some simultaneously, force us to
   3.237 +  introduce them explicitly as shown below.*}
   3.238 +lemma possibility_CR6:
   3.239 +     "[|NC1 < (NC2::nat);  NC2 < NC3;  NC3 < NCA ;
   3.240 +        NCA < NonceCCA;  NonceCCA < CardSecret;
   3.241 +        KC1 < (KC2::key);  KC2 < KC3;
   3.242 +        KC1 \<in> symKeys;  Key KC1 \<notin> used [];
   3.243 +        KC2 \<in> symKeys;  Key KC2 \<notin> used [];
   3.244 +        KC3 \<in> symKeys;  Key KC3 \<notin> used [];
   3.245 +        C = Cardholder k|]
   3.246 +   ==> \<exists>evs \<in> set_cr.
   3.247 +       Says (CA i) C
   3.248 +            (Crypt KC2
   3.249 +             {|sign (priSK (CA i))
   3.250 +                    {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
   3.251 +               certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
   3.252 +                     onlySig (priSK (CA i)),
   3.253 +               cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
   3.254 +          \<in> set evs"
   3.255 +apply (intro exI bexI)
   3.256 +apply (rule_tac [2] ?NC1.8 = NC1 and ?NC1.10 = NC1
   3.257 +                and ?NC2.4 = NC2 and ?NC2.6 = NC2
   3.258 +                and ?NC3.0 = NC3 and ?NC3.2 = NC3
   3.259 +                and NCA2 = NCA and NCA4 = NCA
   3.260 +                and CardSecret = CardSecret and CardSecret2 = CardSecret
   3.261 +                and ?KC1.4 = KC1 and ?KC1.6 = KC1
   3.262 +                and ?KC2.0 = KC2 and ?KC2.2 = KC2
   3.263 +                and ?KC3.0 = KC3 and ?KC3.2 = KC3
   3.264 +       in
   3.265 +       set_cr.Nil [THEN set_cr.SET_CR1, THEN Says_to_Gets, 
   3.266 +                   THEN set_cr.SET_CR2, THEN Says_to_Gets, 
   3.267 +                   THEN set_cr.SET_CR3, THEN Says_to_Gets, 
   3.268 +                   THEN set_cr.SET_CR4, THEN Says_to_Gets, 
   3.269 +                   THEN set_cr.SET_CR5, THEN Says_to_Gets, 
   3.270 +                   THEN set_cr.SET_CR6])
   3.271 +apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
   3.272 +apply auto
   3.273 +done
   3.274 +
   3.275 +
   3.276 +text{*General facts about message reception*}
   3.277 +lemma Gets_imp_Says:
   3.278 +     "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
   3.279 +apply (erule rev_mp)
   3.280 +apply (erule set_cr.induct, auto)
   3.281 +done
   3.282 +
   3.283 +lemma Gets_imp_knows_Spy:
   3.284 +     "[| Gets B X \<in> set evs; evs \<in> set_cr |]  ==> X \<in> knows Spy evs"
   3.285 +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   3.286 +declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   3.287 +
   3.288 +
   3.289 +subsection{*Proofs on keys *}
   3.290 +
   3.291 +text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   3.292 +
   3.293 +lemma Spy_see_private_Key [simp]:
   3.294 +     "evs \<in> set_cr
   3.295 +      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   3.296 +by (erule set_cr.induct, auto)
   3.297 +
   3.298 +lemma Spy_analz_private_Key [simp]:
   3.299 +     "evs \<in> set_cr ==>
   3.300 +     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   3.301 +by auto
   3.302 +
   3.303 +declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   3.304 +declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   3.305 +
   3.306 +
   3.307 +subsection{*Begin Piero's Theorems on Certificates*}
   3.308 +text{*Trivial in the current model, where certificates by RCA are secure *}
   3.309 +
   3.310 +lemma Crypt_valid_pubEK:
   3.311 +     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
   3.312 +           \<in> parts (knows Spy evs);
   3.313 +         evs \<in> set_cr |] ==> EKi = pubEK C"
   3.314 +apply (erule rev_mp)
   3.315 +apply (erule set_cr.induct, auto)
   3.316 +done
   3.317 +
   3.318 +lemma certificate_valid_pubEK:
   3.319 +    "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   3.320 +        evs \<in> set_cr |]
   3.321 +     ==> EKi = pubEK C"
   3.322 +apply (unfold cert_def signCert_def)
   3.323 +apply (blast dest!: Crypt_valid_pubEK)
   3.324 +done
   3.325 +
   3.326 +lemma Crypt_valid_pubSK:
   3.327 +     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
   3.328 +           \<in> parts (knows Spy evs);
   3.329 +         evs \<in> set_cr |] ==> SKi = pubSK C"
   3.330 +apply (erule rev_mp)
   3.331 +apply (erule set_cr.induct, auto)
   3.332 +done
   3.333 +
   3.334 +lemma certificate_valid_pubSK:
   3.335 +    "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   3.336 +        evs \<in> set_cr |] ==> SKi = pubSK C"
   3.337 +apply (unfold cert_def signCert_def)
   3.338 +apply (blast dest!: Crypt_valid_pubSK)
   3.339 +done
   3.340 +
   3.341 +lemma Gets_certificate_valid:
   3.342 +     "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
   3.343 +                      cert C SKi onlySig (priSK RCA)|} \<in> set evs;
   3.344 +         evs \<in> set_cr |]
   3.345 +      ==> EKi = pubEK C & SKi = pubSK C"
   3.346 +by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
   3.347 +
   3.348 +text{*Nobody can have used non-existent keys!*}
   3.349 +lemma new_keys_not_used:
   3.350 +     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
   3.351 +      ==> K \<notin> keysFor (parts (knows Spy evs))"
   3.352 +apply (erule rev_mp)
   3.353 +apply (erule rev_mp)
   3.354 +apply (erule set_cr.induct)
   3.355 +apply (frule_tac [8] Gets_certificate_valid)
   3.356 +apply (frule_tac [6] Gets_certificate_valid, simp_all)
   3.357 +txt{*Fake*}
   3.358 +apply (force dest!: usedI keysFor_parts_insert)
   3.359 +txt{*Others*}
   3.360 +apply blast
   3.361 +apply auto
   3.362 +done
   3.363 +
   3.364 +
   3.365 +subsection{*New versions: as above, but generalized to have the KK argument *}
   3.366 +
   3.367 +lemma gen_new_keys_not_used:
   3.368 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
   3.369 +      ==> Key K \<notin> used evs --> K \<in> symKeys -->
   3.370 +          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   3.371 +by (auto simp add: new_keys_not_used)
   3.372 +
   3.373 +lemma gen_new_keys_not_analzd:
   3.374 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
   3.375 +      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   3.376 +by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
   3.377 +          dest: gen_new_keys_not_used)
   3.378 +
   3.379 +lemma analz_Key_image_insert_eq:
   3.380 +     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
   3.381 +      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   3.382 +          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   3.383 +by (simp add: gen_new_keys_not_analzd)
   3.384 +
   3.385 +lemma Crypt_parts_imp_used:
   3.386 +     "[|Crypt K X \<in> parts (knows Spy evs);
   3.387 +        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
   3.388 +apply (rule ccontr)
   3.389 +apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   3.390 +done
   3.391 +
   3.392 +lemma Crypt_analz_imp_used:
   3.393 +     "[|Crypt K X \<in> analz (knows Spy evs);
   3.394 +        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
   3.395 +by (blast intro: Crypt_parts_imp_used)
   3.396 +
   3.397 +
   3.398 +subsection{*Messages signed by CA*}
   3.399 +
   3.400 +text{*Message @{text SET_CR2}: C can check CA's signature if he has received
   3.401 +     CA's certificate.*}
   3.402 +lemma CA_Says_2_lemma:
   3.403 +     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
   3.404 +           \<in> parts (knows Spy evs);
   3.405 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.406 +     ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
   3.407 +                 \<in> set evs"
   3.408 +apply (erule rev_mp)
   3.409 +apply (erule set_cr.induct, auto)
   3.410 +done
   3.411 +
   3.412 +text{*Ever used?*}
   3.413 +lemma CA_Says_2:
   3.414 +     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
   3.415 +           \<in> parts (knows Spy evs);
   3.416 +         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   3.417 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.418 +      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
   3.419 +                  \<in> set evs"
   3.420 +by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
   3.421 +
   3.422 +
   3.423 +text{*Message @{text SET_CR4}: C can check CA's signature if he has received
   3.424 +      CA's certificate.*}
   3.425 +lemma CA_Says_4_lemma:
   3.426 +     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
   3.427 +           \<in> parts (knows Spy evs);
   3.428 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.429 +      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
   3.430 +                     {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
   3.431 +apply (erule rev_mp)
   3.432 +apply (erule set_cr.induct, auto)
   3.433 +done
   3.434 +
   3.435 +text{*NEVER USED*}
   3.436 +lemma CA_Says_4:
   3.437 +     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
   3.438 +           \<in> parts (knows Spy evs);
   3.439 +         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   3.440 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.441 +      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
   3.442 +                   {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
   3.443 +by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
   3.444 +
   3.445 +
   3.446 +text{*Message @{text SET_CR6}: C can check CA's signature if he has
   3.447 +      received CA's certificate.*}
   3.448 +lemma CA_Says_6_lemma:
   3.449 +     "[| Crypt (priSK (CA i)) 
   3.450 +               (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
   3.451 +           \<in> parts (knows Spy evs);
   3.452 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.453 +      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
   3.454 +      {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
   3.455 +apply (erule rev_mp)
   3.456 +apply (erule set_cr.induct, auto)
   3.457 +done
   3.458 +
   3.459 +text{*NEVER USED*}
   3.460 +lemma CA_Says_6:
   3.461 +     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
   3.462 +           \<in> parts (knows Spy evs);
   3.463 +         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   3.464 +         evs \<in> set_cr; (CA i) \<notin> bad |]
   3.465 +      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
   3.466 +                    {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
   3.467 +by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
   3.468 +
   3.469 +
   3.470 +
   3.471 +subsection{*Useful lemmas *}
   3.472 +
   3.473 +text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
   3.474 +for other keys aren't needed.*}
   3.475 +
   3.476 +lemma parts_image_priEK:
   3.477 +     "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
   3.478 +        evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
   3.479 +by auto
   3.480 +
   3.481 +text{*trivial proof because (priEK C) never appears even in (parts evs)*}
   3.482 +lemma analz_image_priEK:
   3.483 +     "evs \<in> set_cr ==>
   3.484 +          (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
   3.485 +          (priEK C \<in> KK | C \<in> bad)"
   3.486 +by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   3.487 +
   3.488 +
   3.489 +subsection{*Secrecy of Session Keys *}
   3.490 +
   3.491 +subsubsection{*Lemmas about the predicate KeyCryptKey *}
   3.492 +
   3.493 +text{*A fresh DK cannot be associated with any other
   3.494 +  (with respect to a given trace). *}
   3.495 +lemma DK_fresh_not_KeyCryptKey:
   3.496 +     "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
   3.497 +apply (erule rev_mp)
   3.498 +apply (erule set_cr.induct)
   3.499 +apply (simp_all (no_asm_simp))
   3.500 +apply (blast dest: Crypt_analz_imp_used)+
   3.501 +done
   3.502 +
   3.503 +text{*A fresh K cannot be associated with any other.  The assumption that
   3.504 +  DK isn't a private encryption key may be an artifact of the particular
   3.505 +  definition of KeyCryptKey.*}
   3.506 +lemma K_fresh_not_KeyCryptKey:
   3.507 +     "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
   3.508 +apply (induct evs)
   3.509 +apply (auto simp add: parts_insert2 split add: event.split)
   3.510 +done
   3.511 +
   3.512 +
   3.513 +text{*This holds because if (priEK (CA i)) appears in any traffic then it must
   3.514 +  be known to the Spy, by @{term Spy_see_private_Key}*}
   3.515 +lemma cardSK_neq_priEK:
   3.516 +     "[|Key cardSK \<notin> analz (knows Spy evs);
   3.517 +        Key cardSK : parts (knows Spy evs);
   3.518 +        evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
   3.519 +by blast
   3.520 +
   3.521 +lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
   3.522 +     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
   3.523 +      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
   3.524 +by (erule set_cr.induct, analz_mono_contra, auto)
   3.525 +
   3.526 +text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
   3.527 +lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
   3.528 +apply (induct_tac "evs")
   3.529 +apply (auto simp add: parts_insert2 split add: event.split)
   3.530 +done
   3.531 +
   3.532 +text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   3.533 +  or else cardSK hasn't been used to encrypt K.  Previously we treated
   3.534 +  message 5 in the same way, but the current model assumes that rule
   3.535 +  @{text SET_CR5} is executed only by honest agents.*}
   3.536 +lemma msg6_KeyCryptKey_disj:
   3.537 +     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
   3.538 +          \<in> set evs;
   3.539 +        cardSK \<notin> symKeys;  evs \<in> set_cr|]
   3.540 +      ==> Key cardSK \<in> analz (knows Spy evs) |
   3.541 +          (\<forall>K. ~ KeyCryptKey cardSK K evs)"
   3.542 +by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
   3.543 +
   3.544 +text{*As usual: we express the property as a logical equivalence*}
   3.545 +lemma Key_analz_image_Key_lemma:
   3.546 +     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K \<in> KK | Key K \<in> analz H)
   3.547 +      ==>
   3.548 +      P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
   3.549 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   3.550 +
   3.551 +ML
   3.552 +{*
   3.553 +val Gets_certificate_valid = thm "Gets_certificate_valid";
   3.554 +
   3.555 +fun valid_certificate_tac i =
   3.556 +    EVERY [ftac Gets_certificate_valid i,
   3.557 +           assume_tac i,
   3.558 +           etac conjE i, REPEAT (hyp_subst_tac i)];
   3.559 +*}
   3.560 +
   3.561 +text{*The @{text "(no_asm)"} attribute is essential, since it retains
   3.562 +  the quantifier and allows the simprule's condition to itself be simplified.*}
   3.563 +lemma symKey_compromise [rule_format (no_asm)]:
   3.564 +     "evs \<in> set_cr ==>
   3.565 +      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs)   -->
   3.566 +               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
   3.567 +               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
   3.568 +apply (erule set_cr.induct)
   3.569 +apply (rule_tac [!] allI) +
   3.570 +apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
   3.571 +apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
   3.572 +apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
   3.573 +apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
   3.574 +apply (simp_all
   3.575 +         del: image_insert image_Un imp_disjL
   3.576 +         add: analz_image_keys_simps analz_knows_absorb
   3.577 +              analz_Key_image_insert_eq notin_image_iff
   3.578 +              K_fresh_not_KeyCryptKey
   3.579 +              DK_fresh_not_KeyCryptKey ball_conj_distrib
   3.580 +              analz_image_priEK disj_simps)
   3.581 +  --{*46 seconds on a 1.8GHz machine*}
   3.582 +apply spy_analz
   3.583 +txt{*3*}
   3.584 +apply blast
   3.585 +txt{*5*}
   3.586 +apply blast
   3.587 +done
   3.588 +
   3.589 +text{*The remaining quantifiers seem to be essential.
   3.590 +  NO NEED to assume the cardholder's OK: bad cardholders don't do anything
   3.591 +  wrong!!*}
   3.592 +lemma symKey_secrecy [rule_format]:
   3.593 +     "[|CA i \<notin> bad;  K \<in> symKeys;  evs \<in> set_cr|]
   3.594 +      ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
   3.595 +                Key K \<in> parts{X} -->
   3.596 +                Cardholder c \<notin> bad -->
   3.597 +                Key K \<notin> analz (knows Spy evs)"
   3.598 +apply (erule set_cr.induct)
   3.599 +apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
   3.600 +apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
   3.601 +apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
   3.602 +apply (simp_all del: image_insert image_Un imp_disjL
   3.603 +         add: symKey_compromise fresh_notin_analz_knows_Spy
   3.604 +              analz_image_keys_simps analz_knows_absorb
   3.605 +              analz_Key_image_insert_eq notin_image_iff
   3.606 +              K_fresh_not_KeyCryptKey
   3.607 +              DK_fresh_not_KeyCryptKey
   3.608 +              analz_image_priEK)
   3.609 +  --{*13 seconds on a 1.8GHz machine*}
   3.610 +txt{*Fake*}
   3.611 +apply spy_analz
   3.612 +apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
   3.613 +done
   3.614 +
   3.615 +
   3.616 +subsection{*Primary Goals of Cardholder Registration *}
   3.617 +
   3.618 +text{*The cardholder's certificate really was created by the CA, provided the
   3.619 +    CA is uncompromised *}
   3.620 +
   3.621 +text{*Lemma concerning the actual signed message digest*}
   3.622 +lemma cert_valid_lemma:
   3.623 +     "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
   3.624 +          \<in> parts (knows Spy evs);
   3.625 +        CA i \<notin> bad; evs \<in> set_cr|]
   3.626 +  ==> \<exists>KC2 X Y. Says (CA i) C
   3.627 +                     (Crypt KC2 
   3.628 +                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   3.629 +                  \<in> set evs"
   3.630 +apply (erule rev_mp)
   3.631 +apply (erule set_cr.induct)
   3.632 +apply (simp_all (no_asm_simp))
   3.633 +apply auto
   3.634 +done
   3.635 +
   3.636 +text{*Pre-packaged version for cardholder.  We don't try to confirm the values
   3.637 +  of KC2, X and Y, since they are not important.*}
   3.638 +lemma certificate_valid_cardSK:
   3.639 +    "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
   3.640 +                              cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
   3.641 +        CA i \<notin> bad; evs \<in> set_cr|]
   3.642 +  ==> \<exists>KC2 X Y. Says (CA i) C
   3.643 +                     (Crypt KC2 
   3.644 +                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   3.645 +                   \<in> set evs"
   3.646 +by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
   3.647 +                    certificate_valid_pubSK cert_valid_lemma)
   3.648 +
   3.649 +
   3.650 +lemma Hash_imp_parts [rule_format]:
   3.651 +     "evs \<in> set_cr
   3.652 +      ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
   3.653 +          Nonce N \<in> parts (knows Spy evs)"
   3.654 +apply (erule set_cr.induct, force)
   3.655 +apply (simp_all (no_asm_simp))
   3.656 +apply (blast intro: parts_mono [THEN [2] rev_subsetD])
   3.657 +done
   3.658 +
   3.659 +lemma Hash_imp_parts2 [rule_format]:
   3.660 +     "evs \<in> set_cr
   3.661 +      ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
   3.662 +          Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
   3.663 +apply (erule set_cr.induct, force)
   3.664 +apply (simp_all (no_asm_simp))
   3.665 +apply (blast intro: parts_mono [THEN [2] rev_subsetD])
   3.666 +done
   3.667 +
   3.668 +
   3.669 +subsection{*Secrecy of Nonces*}
   3.670 +
   3.671 +subsubsection{*Lemmas about the predicate KeyCryptNonce *}
   3.672 +
   3.673 +text{*A fresh DK cannot be associated with any other
   3.674 +  (with respect to a given trace). *}
   3.675 +lemma DK_fresh_not_KeyCryptNonce:
   3.676 +     "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
   3.677 +      ==> ~ KeyCryptNonce DK K evs"
   3.678 +apply (erule rev_mp)
   3.679 +apply (erule rev_mp)
   3.680 +apply (erule set_cr.induct)
   3.681 +apply (simp_all (no_asm_simp))
   3.682 +apply blast
   3.683 +apply blast
   3.684 +apply (auto simp add: DK_fresh_not_KeyCryptKey)
   3.685 +done
   3.686 +
   3.687 +text{*A fresh N cannot be associated with any other
   3.688 +      (with respect to a given trace). *}
   3.689 +lemma N_fresh_not_KeyCryptNonce:
   3.690 +     "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
   3.691 +apply (induct_tac "evs")
   3.692 +apply (case_tac [2] "a")
   3.693 +apply (auto simp add: parts_insert2)
   3.694 +done
   3.695 +
   3.696 +lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
   3.697 +     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
   3.698 +      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
   3.699 +apply (erule set_cr.induct, analz_mono_contra, simp_all)
   3.700 +txt{*6*}
   3.701 +apply (blast dest: not_KeyCryptKey_cardSK)
   3.702 +done
   3.703 +
   3.704 +subsubsection{*Lemmas for message 5 and 6:
   3.705 +  either cardSK is compromised (when we don't care)
   3.706 +  or else cardSK hasn't been used to encrypt K. *}
   3.707 +
   3.708 +text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
   3.709 +lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
   3.710 +apply (induct_tac "evs")
   3.711 +apply (auto simp add: parts_insert2 split add: event.split)
   3.712 +done
   3.713 +
   3.714 +text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   3.715 +  or else cardSK hasn't been used to encrypt K.*}
   3.716 +lemma msg6_KeyCryptNonce_disj:
   3.717 +     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
   3.718 +          \<in> set evs;
   3.719 +        cardSK \<notin> symKeys;  evs \<in> set_cr|]
   3.720 +      ==> Key cardSK \<in> analz (knows Spy evs) |
   3.721 +          ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
   3.722 +           (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
   3.723 +by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
   3.724 +          intro: cardSK_neq_priEK)
   3.725 +
   3.726 +
   3.727 +text{*As usual: we express the property as a logical equivalence*}
   3.728 +lemma Nonce_analz_image_Key_lemma:
   3.729 +     "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
   3.730 +      ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
   3.731 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   3.732 +
   3.733 +text{*The @{text "(no_asm)"} attribute is essential, since it retains
   3.734 +  the quantifier and allows the simprule's condition to itself be simplified.*}
   3.735 +lemma Nonce_compromise [rule_format (no_asm)]:
   3.736 +     "evs \<in> set_cr ==>
   3.737 +      (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs)   -->
   3.738 +               (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
   3.739 +               (Nonce N \<in> analz (knows Spy evs)))"
   3.740 +apply (erule set_cr.induct)
   3.741 +apply (rule_tac [!] allI)+
   3.742 +apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
   3.743 +apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
   3.744 +apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
   3.745 +apply (frule_tac [11] msg6_KeyCryptNonce_disj)
   3.746 +apply (erule_tac [13] disjE)
   3.747 +apply (simp_all del: image_insert image_Un
   3.748 +         add: symKey_compromise
   3.749 +              analz_image_keys_simps analz_knows_absorb
   3.750 +              analz_Key_image_insert_eq notin_image_iff
   3.751 +              N_fresh_not_KeyCryptNonce
   3.752 +              DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
   3.753 +              ball_conj_distrib analz_image_priEK)
   3.754 +  --{*71 seconds on a 1.8GHz machine*}
   3.755 +txt{*Fake*}
   3.756 +apply spy_analz
   3.757 +txt{*3*}
   3.758 +apply blast
   3.759 +txt{*5*}
   3.760 +apply blast
   3.761 +txt{*6*}
   3.762 +txt{*cardSK compromised?*}
   3.763 +apply (force del: allE ballE impCE simp add: symKey_compromise)
   3.764 +txt{*Simplify again--necessary because the previous simplification introduces
   3.765 +  some logical connectives*}
   3.766 +by (force del: allE ballE impCE
   3.767 +          simp del: image_insert image_Un imp_disjL
   3.768 +          simp add: analz_image_keys_simps symKey_compromise)
   3.769 +
   3.770 +
   3.771 +subsection{*Secrecy of CardSecret: the Cardholder's secret*}
   3.772 +
   3.773 +lemma NC2_not_CardSecret:
   3.774 +     "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
   3.775 +          \<in> parts (knows Spy evs);
   3.776 +        Key K \<notin> analz (knows Spy evs);
   3.777 +        Nonce N \<notin> analz (knows Spy evs);
   3.778 +       evs \<in> set_cr|]
   3.779 +      ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
   3.780 +apply (erule rev_mp)
   3.781 +apply (erule rev_mp)
   3.782 +apply (erule rev_mp)
   3.783 +apply (erule set_cr.induct, analz_mono_contra, simp_all)
   3.784 +apply (blast dest: Hash_imp_parts)+
   3.785 +done
   3.786 +
   3.787 +lemma KC2_secure_lemma [rule_format]:
   3.788 +     "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
   3.789 +        U \<in> parts (knows Spy evs);
   3.790 +        evs \<in> set_cr|]
   3.791 +  ==> Nonce N \<notin> analz (knows Spy evs) -->
   3.792 +      (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
   3.793 +               Cardholder k \<notin> bad & CA i \<notin> bad)"
   3.794 +apply (erule_tac P = "U \<in> ?H" in rev_mp)
   3.795 +apply (erule set_cr.induct)
   3.796 +apply (tactic{*valid_certificate_tac 8*})  --{*for message 5*}
   3.797 +apply (simp_all del: image_insert image_Un imp_disjL
   3.798 +         add: analz_image_keys_simps analz_knows_absorb
   3.799 +              analz_knows_absorb2 notin_image_iff)
   3.800 +  --{*19 seconds on a 1.8GHz machine*}
   3.801 +apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
   3.802 +apply (blast intro!: analz_insertI)+
   3.803 +done
   3.804 +
   3.805 +lemma KC2_secrecy:
   3.806 +     "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
   3.807 +        Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
   3.808 +        evs \<in> set_cr|]
   3.809 +       ==> Key KC2 \<notin> analz (knows Spy evs)"
   3.810 +by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
   3.811 +
   3.812 +
   3.813 +text{*Inductive version*}
   3.814 +lemma CardSecret_secrecy_lemma [rule_format]:
   3.815 +     "[|CA i \<notin> bad;  evs \<in> set_cr|]
   3.816 +      ==> Key K \<notin> analz (knows Spy evs) -->
   3.817 +          Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
   3.818 +             \<in> parts (knows Spy evs) -->
   3.819 +          Nonce CardSecret \<notin> analz (knows Spy evs)"
   3.820 +apply (erule set_cr.induct, analz_mono_contra)
   3.821 +apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
   3.822 +apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
   3.823 +apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   3.824 +apply (simp_all
   3.825 +         del: image_insert image_Un imp_disjL
   3.826 +         add: analz_image_keys_simps analz_knows_absorb
   3.827 +              analz_Key_image_insert_eq notin_image_iff
   3.828 +              EXHcrypt_def Crypt_notin_image_Key
   3.829 +              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   3.830 +              ball_conj_distrib Nonce_compromise symKey_compromise
   3.831 +              analz_image_priEK)
   3.832 +  --{*12 seconds on a 1.8GHz machine*}
   3.833 +txt{*Fake*}
   3.834 +apply spy_analz
   3.835 +apply (simp_all (no_asm_simp))
   3.836 +txt{*1*}
   3.837 +apply blast
   3.838 +txt{*2*}
   3.839 +apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   3.840 +txt{*3*}
   3.841 +apply blast
   3.842 +txt{*4*}
   3.843 +apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)
   3.844 +txt{*5*}
   3.845 +apply blast
   3.846 +txt{*6*}
   3.847 +apply (blast dest: KC2_secrecy)
   3.848 +apply (blast dest: KC2_secrecy)
   3.849 +done
   3.850 +
   3.851 +
   3.852 +text{*Packaged version for cardholder*}
   3.853 +lemma CardSecret_secrecy:
   3.854 +     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   3.855 +        Says (Cardholder k) (CA i)
   3.856 +           {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
   3.857 +        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   3.858 +                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   3.859 +        KC3 \<in> symKeys;  evs \<in> set_cr|]
   3.860 +      ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
   3.861 +apply (frule Gets_certificate_valid, assumption)
   3.862 +apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
   3.863 +apply (blast dest: CardSecret_secrecy_lemma)
   3.864 +apply (rule symKey_secrecy)
   3.865 +apply (auto simp add: parts_insert2)
   3.866 +done
   3.867 +
   3.868 +
   3.869 +subsection{*Secrecy of NonceCCA [the CA's secret] *}
   3.870 +
   3.871 +lemma NC2_not_NonceCCA:
   3.872 +     "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
   3.873 +          \<in> parts (knows Spy evs);
   3.874 +        Nonce N \<notin> analz (knows Spy evs);
   3.875 +       evs \<in> set_cr|]
   3.876 +      ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
   3.877 +apply (erule rev_mp)
   3.878 +apply (erule rev_mp)
   3.879 +apply (erule set_cr.induct, analz_mono_contra, simp_all)
   3.880 +apply (blast dest: Hash_imp_parts2)+
   3.881 +done
   3.882 +
   3.883 +
   3.884 +text{*Inductive version*}
   3.885 +lemma NonceCCA_secrecy_lemma [rule_format]:
   3.886 +     "[|CA i \<notin> bad;  evs \<in> set_cr|]
   3.887 +      ==> Key K \<notin> analz (knows Spy evs) -->
   3.888 +          Crypt K
   3.889 +            {|sign (priSK (CA i))
   3.890 +                   {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   3.891 +              X, Y|}
   3.892 +             \<in> parts (knows Spy evs) -->
   3.893 +          Nonce NonceCCA \<notin> analz (knows Spy evs)"
   3.894 +apply (erule set_cr.induct, analz_mono_contra)
   3.895 +apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
   3.896 +apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
   3.897 +apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   3.898 +apply (simp_all
   3.899 +         del: image_insert image_Un imp_disjL
   3.900 +         add: analz_image_keys_simps analz_knows_absorb sign_def
   3.901 +              analz_Key_image_insert_eq notin_image_iff
   3.902 +              EXHcrypt_def Crypt_notin_image_Key
   3.903 +              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   3.904 +              ball_conj_distrib Nonce_compromise symKey_compromise
   3.905 +              analz_image_priEK)
   3.906 +  --{*15 seconds on a 1.8GHz machine*}
   3.907 +txt{*Fake*}
   3.908 +apply spy_analz
   3.909 +txt{*1*}
   3.910 +apply blast
   3.911 +txt{*2*}
   3.912 +apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   3.913 +txt{*3*}
   3.914 +apply blast
   3.915 +txt{*4*}
   3.916 +apply (blast dest: NC2_not_NonceCCA)
   3.917 +txt{*5*}
   3.918 +apply blast
   3.919 +txt{*6*}
   3.920 +apply (blast dest: KC2_secrecy)
   3.921 +apply (blast dest: KC2_secrecy)
   3.922 +done
   3.923 +
   3.924 +
   3.925 +text{*Packaged version for cardholder*}
   3.926 +lemma NonceCCA_secrecy:
   3.927 +     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   3.928 +        Gets (Cardholder k)
   3.929 +           (Crypt KC2
   3.930 +            {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   3.931 +              X, Y|}) \<in> set evs;
   3.932 +        Says (Cardholder k) (CA i)
   3.933 +           {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
   3.934 +        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   3.935 +                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   3.936 +        KC2 \<in> symKeys;  evs \<in> set_cr|]
   3.937 +      ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
   3.938 +apply (frule Gets_certificate_valid, assumption)
   3.939 +apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
   3.940 +apply (blast dest: NonceCCA_secrecy_lemma)
   3.941 +apply (rule symKey_secrecy)
   3.942 +apply (auto simp add: parts_insert2)
   3.943 +done
   3.944 +
   3.945 +text{*We don't bother to prove guarantees for the CA.  He doesn't care about
   3.946 +  the PANSecret: it isn't his credit card!*}
   3.947 +
   3.948 +
   3.949 +subsection{*Rewriting Rule for PANs*}
   3.950 +
   3.951 +text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
   3.952 +  or if it is then (because it appears in traffic) that CA is bad,
   3.953 +  and so the Spy knows that key already.  Either way, we can simplify
   3.954 +  the expression @{term "analz (insert (Key cardSK) X)"}.*}
   3.955 +lemma msg6_cardSK_disj:
   3.956 +     "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
   3.957 +          \<in> set evs;  evs \<in> set_cr |]
   3.958 +      ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
   3.959 +by auto
   3.960 +
   3.961 +lemma analz_image_pan_lemma:
   3.962 +     "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
   3.963 +      (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
   3.964 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   3.965 +
   3.966 +lemma analz_image_pan [rule_format]:
   3.967 +     "evs \<in> set_cr ==>
   3.968 +       \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
   3.969 +            (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
   3.970 +            (Pan P \<in> analz (knows Spy evs))"
   3.971 +apply (erule set_cr.induct)
   3.972 +apply (rule_tac [!] allI impI)+
   3.973 +apply (rule_tac [!] analz_image_pan_lemma)
   3.974 +apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
   3.975 +apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
   3.976 +apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
   3.977 +apply (simp_all
   3.978 +         del: image_insert image_Un
   3.979 +         add: analz_image_keys_simps disjoint_image_iff
   3.980 +              notin_image_iff analz_image_priEK)
   3.981 +  --{*33 seconds on a 1.8GHz machine*}
   3.982 +apply spy_analz
   3.983 +txt{*6*}
   3.984 +apply (simp add: insert_absorb)
   3.985 +done
   3.986 +
   3.987 +lemma analz_insert_pan:
   3.988 +     "[| evs \<in> set_cr;  K \<notin> invKey ` pubEK ` range CA |] ==>
   3.989 +          (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
   3.990 +          (Pan P \<in> analz (knows Spy evs))"
   3.991 +by (simp del: image_insert image_Un
   3.992 +         add: analz_image_keys_simps analz_image_pan)
   3.993 +
   3.994 +
   3.995 +text{*Confidentiality of the PAN\@.  Maybe we could combine the statements of
   3.996 +  this theorem with @{term analz_image_pan}, requiring a single induction but
   3.997 +  a much more difficult proof.*}
   3.998 +lemma pan_confidentiality:
   3.999 +     "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
  3.1000 +    ==> \<exists>i X K HN.
  3.1001 +        Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
  3.1002 +           \<in> set evs
  3.1003 +      & (CA i) \<in> bad"
  3.1004 +apply (erule rev_mp)
  3.1005 +apply (erule set_cr.induct)
  3.1006 +apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
  3.1007 +apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
  3.1008 +apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
  3.1009 +apply (simp_all
  3.1010 +         del: image_insert image_Un
  3.1011 +         add: analz_image_keys_simps analz_insert_pan analz_image_pan
  3.1012 +              notin_image_iff analz_image_priEK)
  3.1013 +  --{*18 seconds on a 1.8GHz machine*}
  3.1014 +txt{*fake*}
  3.1015 +apply spy_analz
  3.1016 +txt{*3*}
  3.1017 +apply blast
  3.1018 +txt{*5*}
  3.1019 +apply blast
  3.1020 +txt{*6*}
  3.1021 +apply (simp (no_asm_simp) add: insert_absorb)
  3.1022 +done
  3.1023 +
  3.1024 +
  3.1025 +subsection{*Unicity*}
  3.1026 +
  3.1027 +lemma CR6_Says_imp_Notes:
  3.1028 +     "[|Says (CA i) C (Crypt KC2
  3.1029 +          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
  3.1030 +            certC (pan C) cardSK X onlySig (priSK (CA i)),
  3.1031 +            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
  3.1032 +        evs \<in> set_cr |]
  3.1033 +      ==> Notes (CA i) (Key cardSK) \<in> set evs"
  3.1034 +apply (erule rev_mp)
  3.1035 +apply (erule set_cr.induct)
  3.1036 +apply (simp_all (no_asm_simp))
  3.1037 +done
  3.1038 +
  3.1039 +text{*Unicity of cardSK: it uniquely identifies the other components.  
  3.1040 +      This holds because a CA accepts a cardSK at most once.*}
  3.1041 +lemma cardholder_key_unicity:
  3.1042 +     "[|Says (CA i) C (Crypt KC2
  3.1043 +          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
  3.1044 +            certC (pan C) cardSK X onlySig (priSK (CA i)),
  3.1045 +            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  3.1046 +          \<in> set evs;
  3.1047 +        Says (CA i) C' (Crypt KC2'
  3.1048 +          {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
  3.1049 +            certC (pan C') cardSK X' onlySig (priSK (CA i)),
  3.1050 +            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  3.1051 +          \<in> set evs;
  3.1052 +        evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
  3.1053 +apply (erule rev_mp)
  3.1054 +apply (erule rev_mp)
  3.1055 +apply (erule set_cr.induct)
  3.1056 +apply (simp_all (no_asm_simp))
  3.1057 +apply (blast dest!: CR6_Says_imp_Notes)
  3.1058 +done
  3.1059 +
  3.1060 +
  3.1061 +text{*UNUSED unicity result*}
  3.1062 +lemma unique_KC1:
  3.1063 +     "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
  3.1064 +          \<in> set evs;
  3.1065 +        Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
  3.1066 +          \<in> set evs;
  3.1067 +        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
  3.1068 +apply (erule rev_mp)
  3.1069 +apply (erule rev_mp)
  3.1070 +apply (erule set_cr.induct, auto)
  3.1071 +done
  3.1072 +
  3.1073 +text{*UNUSED unicity result*}
  3.1074 +lemma unique_KC2:
  3.1075 +     "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
  3.1076 +        Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
  3.1077 +        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
  3.1078 +apply (erule rev_mp)
  3.1079 +apply (erule rev_mp)
  3.1080 +apply (erule set_cr.induct, auto)
  3.1081 +done
  3.1082 +
  3.1083 +text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
  3.1084 +  it could be a previously compromised cardSK [e.g. involving a bad CA]*}
  3.1085 +
  3.1086 +
  3.1087 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Tue Sep 23 15:40:27 2003 +0200
     4.3 @@ -0,0 +1,271 @@
     4.4 +(*  Title:      HOL/Auth/SET/EventSET
     4.5 +    ID:         $Id$
     4.6 +    Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     4.7 +*)
     4.8 +
     4.9 +header{*Theory of Events for SET*}
    4.10 +
    4.11 +theory EventSET = MessageSET:
    4.12 +
    4.13 +text{*The Root Certification Authority*}
    4.14 +syntax        RCA :: agent
    4.15 +translations "RCA" == "CA 0"
    4.16 +
    4.17 +
    4.18 +text{*Message events*}
    4.19 +datatype
    4.20 +  event = Says  agent agent msg
    4.21 +	| Gets  agent	    msg
    4.22 +        | Notes agent       msg
    4.23 +
    4.24 +
    4.25 +text{*compromised agents: keys known, Notes visible*}
    4.26 +consts bad :: "agent set"
    4.27 +
    4.28 +text{*Spy has access to his own key for spoof messages, but RCA is secure*}
    4.29 +specification (bad)
    4.30 +  Spy_in_bad     [iff]: "Spy \<in> bad"
    4.31 +  RCA_not_bad [iff]: "RCA \<notin> bad"
    4.32 +    by (rule exI [of _ "{Spy}"], simp)
    4.33 +
    4.34 +
    4.35 +subsection{*Agents' Knowledge*}
    4.36 +
    4.37 +consts  (*Initial states of agents -- parameter of the construction*)
    4.38 +  initState :: "agent => msg set"
    4.39 +  knows  :: "[agent, event list] => msg set"
    4.40 +
    4.41 +(* Message reception does not extend spy's knowledge because of
    4.42 +   reception invariant enforced by Reception rule in protocol definition*)
    4.43 +primrec
    4.44 +
    4.45 +knows_Nil:
    4.46 +  "knows A []       = initState A"
    4.47 +knows_Cons:
    4.48 +    "knows A (ev # evs) =
    4.49 +       (if A = Spy then
    4.50 +	(case ev of
    4.51 +	   Says A' B X => insert X (knows Spy evs)
    4.52 +	 | Gets A' X => knows Spy evs
    4.53 +	 | Notes A' X  =>
    4.54 +	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    4.55 +	else
    4.56 +	(case ev of
    4.57 +	   Says A' B X =>
    4.58 +	     if A'=A then insert X (knows A evs) else knows A evs
    4.59 +	 | Gets A' X    =>
    4.60 +	     if A'=A then insert X (knows A evs) else knows A evs
    4.61 +	 | Notes A' X    =>
    4.62 +	     if A'=A then insert X (knows A evs) else knows A evs))"
    4.63 +
    4.64 +
    4.65 +subsection{*Used Messages*}
    4.66 +
    4.67 +consts
    4.68 +  (*Set of items that might be visible to somebody:
    4.69 +    complement of the set of fresh items*)
    4.70 +  used :: "event list => msg set"
    4.71 +
    4.72 +(* As above, message reception does extend used items *)
    4.73 +primrec
    4.74 +  used_Nil:  "used []         = (UN B. parts (initState B))"
    4.75 +  used_Cons: "used (ev # evs) =
    4.76 +	         (case ev of
    4.77 +		    Says A B X => parts {X} Un (used evs)
    4.78 +         	  | Gets A X   => used evs
    4.79 +		  | Notes A X  => parts {X} Un (used evs))"
    4.80 +
    4.81 +
    4.82 +
    4.83 +(* Inserted by default but later removed.  This declaration lets the file
    4.84 +be re-loaded. Addsimps [knows_Cons, used_Nil, *)
    4.85 +
    4.86 +(** Simplifying   parts (insert X (knows Spy evs))
    4.87 +      = parts {X} Un parts (knows Spy evs) -- since general case loops*)
    4.88 +
    4.89 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    4.90 +
    4.91 +lemma knows_Spy_Says [simp]:
    4.92 +     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    4.93 +by auto
    4.94 +
    4.95 +text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
    4.96 +      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
    4.97 +lemma knows_Spy_Notes [simp]:
    4.98 +     "knows Spy (Notes A X # evs) =
    4.99 +          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
   4.100 +apply auto
   4.101 +done
   4.102 +
   4.103 +lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
   4.104 +by auto
   4.105 +
   4.106 +lemma initState_subset_knows: "initState A <= knows A evs"
   4.107 +apply (induct_tac "evs")
   4.108 +apply (auto split: event.split) 
   4.109 +done
   4.110 +
   4.111 +lemma knows_Spy_subset_knows_Spy_Says:
   4.112 +     "knows Spy evs <= knows Spy (Says A B X # evs)"
   4.113 +by auto
   4.114 +
   4.115 +lemma knows_Spy_subset_knows_Spy_Notes:
   4.116 +     "knows Spy evs <= knows Spy (Notes A X # evs)"
   4.117 +by auto
   4.118 +
   4.119 +lemma knows_Spy_subset_knows_Spy_Gets:
   4.120 +     "knows Spy evs <= knows Spy (Gets A X # evs)"
   4.121 +by auto
   4.122 +
   4.123 +(*Spy sees what is sent on the traffic*)
   4.124 +lemma Says_imp_knows_Spy [rule_format]:
   4.125 +     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
   4.126 +apply (induct_tac "evs")
   4.127 +apply (auto split: event.split) 
   4.128 +done
   4.129 +
   4.130 +(*Use with addSEs to derive contradictions from old Says events containing
   4.131 +  items known to be fresh*)
   4.132 +lemmas knows_Spy_partsEs =
   4.133 +     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   4.134 +     parts.Body [THEN revcut_rl, standard]
   4.135 +
   4.136 +
   4.137 +subsection{*Lemmas About Agents' Knowledge*}
   4.138 +
   4.139 +lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
   4.140 +by auto
   4.141 +
   4.142 +lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
   4.143 +by auto
   4.144 +
   4.145 +lemma knows_Gets:
   4.146 +     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
   4.147 +by auto
   4.148 +
   4.149 +lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A B X # evs)"
   4.150 +by auto
   4.151 +
   4.152 +lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A X # evs)"
   4.153 +by auto
   4.154 +
   4.155 +lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A X # evs)"
   4.156 +by auto
   4.157 +
   4.158 +(*Agents know what they say*)
   4.159 +lemma Says_imp_knows [rule_format]:
   4.160 +     "Says A B X \<in> set evs --> X \<in> knows A evs"
   4.161 +apply (induct_tac "evs")
   4.162 +apply (auto split: event.split) 
   4.163 +done
   4.164 +
   4.165 +(*Agents know what they note*)
   4.166 +lemma Notes_imp_knows [rule_format]:
   4.167 +     "Notes A X \<in> set evs --> X \<in> knows A evs"
   4.168 +apply (induct_tac "evs")
   4.169 +apply (auto split: event.split) 
   4.170 +done
   4.171 +
   4.172 +(*Agents know what they receive*)
   4.173 +lemma Gets_imp_knows_agents [rule_format]:
   4.174 +     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
   4.175 +apply (induct_tac "evs")
   4.176 +apply (auto split: event.split) 
   4.177 +done
   4.178 +
   4.179 +
   4.180 +(*What agents DIFFERENT FROM Spy know
   4.181 +  was either said, or noted, or got, or known initially*)
   4.182 +lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
   4.183 +     "[| X \<in> knows A evs; A \<noteq> Spy |] ==>
   4.184 +  \<exists>B. Says A B X \<in> set evs |
   4.185 +               Gets A X \<in> set evs |
   4.186 +               Notes A X \<in> set evs |
   4.187 +               X \<in> initState A"
   4.188 +apply (erule rev_mp) 
   4.189 +apply (induct_tac "evs")
   4.190 +apply (auto split: event.split) 
   4.191 +done
   4.192 +
   4.193 +(*What the Spy knows -- for the time being --
   4.194 +  was either said or noted, or known initially*)
   4.195 +lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
   4.196 +     "[| X \<in> knows Spy evs |] ==>
   4.197 +   \<exists>A B. Says A B X \<in> set evs |
   4.198 +                  Notes A X \<in> set evs |
   4.199 +                  X \<in> initState Spy"
   4.200 +apply (erule rev_mp) 
   4.201 +apply (induct_tac "evs")
   4.202 +apply (auto split: event.split) 
   4.203 +done
   4.204 +
   4.205 +
   4.206 +subsection{*The Function @{term used}*}
   4.207 +
   4.208 +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
   4.209 +apply (induct_tac "evs")
   4.210 +apply (auto simp add: parts_insert_knows_A split: event.split) 
   4.211 +done
   4.212 +
   4.213 +lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   4.214 +
   4.215 +lemma initState_subset_used: "parts (initState B) <= used evs"
   4.216 +apply (induct_tac "evs")
   4.217 +apply (auto split: event.split) 
   4.218 +done
   4.219 +
   4.220 +lemmas initState_into_used = initState_subset_used [THEN subsetD]
   4.221 +
   4.222 +lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} Un used evs"
   4.223 +by auto
   4.224 +
   4.225 +lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} Un used evs"
   4.226 +by auto
   4.227 +
   4.228 +lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   4.229 +by auto
   4.230 +
   4.231 +lemma used_nil_subset: "used [] <= used evs"
   4.232 +apply auto
   4.233 +apply (rule initState_into_used, auto)
   4.234 +done
   4.235 +
   4.236 +
   4.237 +lemma Notes_imp_parts_subset_used [rule_format]:
   4.238 +     "Notes A X \<in> set evs --> parts {X} <= used evs"
   4.239 +apply (induct_tac "evs")
   4.240 +apply (induct_tac [2] "a", auto)
   4.241 +done
   4.242 +
   4.243 +text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   4.244 +declare knows_Cons [simp del]
   4.245 +        used_Nil [simp del] used_Cons [simp del]
   4.246 +
   4.247 +
   4.248 +text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
   4.249 +  New events added by induction to "evs" are discarded.  Provided 
   4.250 +  this information isn't needed, the proof will be much shorter, since
   4.251 +  it will omit complicated reasoning about @{term analz}.*}
   4.252 +
   4.253 +lemmas analz_mono_contra =
   4.254 +       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
   4.255 +       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
   4.256 +       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
   4.257 +ML
   4.258 +{*
   4.259 +val analz_mono_contra_tac = 
   4.260 +  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   4.261 +  in
   4.262 +    rtac analz_impI THEN' 
   4.263 +    REPEAT1 o 
   4.264 +      (dresolve_tac (thms"analz_mono_contra"))
   4.265 +    THEN' mp_tac
   4.266 +  end
   4.267 +*}
   4.268 +
   4.269 +method_setup analz_mono_contra = {*
   4.270 +    Method.no_args
   4.271 +      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
   4.272 +    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   4.273 +
   4.274 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/SET-Protocol/Merchant_Registration.thy	Tue Sep 23 15:40:27 2003 +0200
     5.3 @@ -0,0 +1,435 @@
     5.4 +(*  Title:      HOL/Auth/SET/Merchant_Registration
     5.5 +    ID:         $Id$
     5.6 +    Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     5.7 +*)
     5.8 +
     5.9 +header{*The SET Merchant Registration Protocol*}
    5.10 +
    5.11 +theory Merchant_Registration = PublicSET:
    5.12 +
    5.13 +text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
    5.14 +  needed: no session key encrypts another.  Instead we
    5.15 +  prove the "key compromise" theorems for sets KK that contain no private
    5.16 +  encryption keys (@{term "priEK C"}). *}
    5.17 +
    5.18 +
    5.19 +consts  set_mr  :: "event list set"
    5.20 +inductive set_mr
    5.21 + intros
    5.22 +
    5.23 +  Nil:    --{*Initial trace is empty*}
    5.24 +	   "[] \<in> set_mr"
    5.25 +
    5.26 +
    5.27 +  Fake:    --{*The spy MAY say anything he CAN say.*}
    5.28 +	   "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
    5.29 +	    ==> Says Spy B X  # evsf \<in> set_mr"
    5.30 +	
    5.31 +
    5.32 +  Reception: --{*If A sends a message X to B, then B might receive it*}
    5.33 +	     "[| evsr \<in> set_mr; Says A B X \<in> set evsr |]
    5.34 +              ==> Gets B X  # evsr \<in> set_mr"
    5.35 +
    5.36 +
    5.37 +  SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
    5.38 + 	   "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
    5.39 +            ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
    5.40 +
    5.41 +
    5.42 +  SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
    5.43 +               certificates for her keys*}
    5.44 +  "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
    5.45 +      Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
    5.46 +   ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
    5.47 +	               cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
    5.48 +                       cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
    5.49 +	 # evs2 \<in> set_mr"
    5.50 +
    5.51 +  SET_MR3:
    5.52 +         --{*CertReq: M submits the key pair to be certified.  The Notes
    5.53 +             event allows KM1 to be lost if M is compromised. Piero remarks
    5.54 +             that the agent mentioned inside the signature is not verified to
    5.55 +             correspond to M.  As in CR, each Merchant has fixed key pairs.  M
    5.56 +             is only optionally required to send NCA back, so M doesn't do so
    5.57 +             in the model*}
    5.58 +  "[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3;
    5.59 +      Key KM1 \<notin> used evs3;  KM1 \<in> symKeys;
    5.60 +      Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
    5.61 +	       cert (CA i) EKi onlyEnc (priSK RCA),
    5.62 +	       cert (CA i) SKi onlySig (priSK RCA) |}
    5.63 +	\<in> set evs3;
    5.64 +      Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
    5.65 +   ==> Says M (CA i)
    5.66 +	    {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
    5.67 +					  Key (pubSK M), Key (pubEK M)|}),
    5.68 +	      Crypt EKi (Key KM1)|}
    5.69 +	 # Notes M {|Key KM1, Agent (CA i)|}
    5.70 +	 # evs3 \<in> set_mr"
    5.71 +
    5.72 +  SET_MR4:
    5.73 +         --{*CertRes: CA issues the certificates for merSK and merEK,
    5.74 +             while checking never to have certified the m even
    5.75 +             separately. NOTE: In Cardholder Registration the
    5.76 +             corresponding rule (6) doesn't use the "sign" primitive. "The
    5.77 +             CertRes shall be signed but not encrypted if the EE is a Merchant
    5.78 +             or Payment Gateway."-- Programmer's Guide, page 191.*}
    5.79 +    "[| evs4 \<in> set_mr; M = Merchant k;
    5.80 +	merSK \<notin> symKeys;  merEK \<notin> symKeys;
    5.81 +	Notes (CA i) (Key merSK) \<notin> set evs4;
    5.82 +	Notes (CA i) (Key merEK) \<notin> set evs4;
    5.83 +	Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
    5.84 +				 {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
    5.85 +		      Crypt (pubEK (CA i)) (Key KM1) |}
    5.86 +	  \<in> set evs4 |]
    5.87 +    ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
    5.88 +			cert  M      merSK    onlySig (priSK (CA i)),
    5.89 +			cert  M      merEK    onlyEnc (priSK (CA i)),
    5.90 +			cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
    5.91 +	  # Notes (CA i) (Key merSK)
    5.92 +	  # Notes (CA i) (Key merEK)
    5.93 +	  # evs4 \<in> set_mr"
    5.94 +
    5.95 +
    5.96 +text{*Note possibility proofs are missing.*}
    5.97 +
    5.98 +declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    5.99 +declare parts.Body [dest]
   5.100 +declare analz_into_parts [dest]
   5.101 +declare Fake_parts_insert_in_Un [dest]
   5.102 +
   5.103 +text{*General facts about message reception*}
   5.104 +lemma Gets_imp_Says:
   5.105 +     "[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> \<exists>A. Says A B X \<in> set evs"
   5.106 +apply (erule rev_mp)
   5.107 +apply (erule set_mr.induct, auto)
   5.108 +done
   5.109 +
   5.110 +lemma Gets_imp_knows_Spy:
   5.111 +     "[| Gets B X \<in> set evs; evs \<in> set_mr |]  ==> X \<in> knows Spy evs"
   5.112 +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   5.113 +
   5.114 +
   5.115 +declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   5.116 +
   5.117 +subsubsection{*Proofs on keys *}
   5.118 +
   5.119 +text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   5.120 +lemma Spy_see_private_Key [simp]:
   5.121 +     "evs \<in> set_mr
   5.122 +      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   5.123 +apply (erule set_mr.induct)
   5.124 +apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj])
   5.125 +done
   5.126 +
   5.127 +lemma Spy_analz_private_Key [simp]:
   5.128 +     "evs \<in> set_mr ==>
   5.129 +     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   5.130 +by auto
   5.131 +
   5.132 +declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   5.133 +declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   5.134 +
   5.135 +(*This is to state that the signed keys received in step 4
   5.136 +  are into parts - rather than installing sign_def each time.
   5.137 +  Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK
   5.138 +Goal "[|Gets C \<lbrace>Crypt KM1
   5.139 +                (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace>
   5.140 +          \<in> set evs;  evs \<in> set_mr |]
   5.141 +    ==> Key merSK \<in> parts (knows Spy evs) \<and>
   5.142 +        Key merEK \<in> parts (knows Spy evs)"
   5.143 +by (fast_tac (claset() addss (simpset())) 1);
   5.144 +qed "signed_keys_in_parts";
   5.145 +???*)
   5.146 +
   5.147 +text{*Proofs on certificates -
   5.148 +  they hold, as in CR, because RCA's keys are secure*}
   5.149 +
   5.150 +lemma Crypt_valid_pubEK:
   5.151 +     "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
   5.152 +           \<in> parts (knows Spy evs);
   5.153 +         evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
   5.154 +apply (erule rev_mp)
   5.155 +apply (erule set_mr.induct, auto)
   5.156 +done
   5.157 +
   5.158 +lemma certificate_valid_pubEK:
   5.159 +    "[| cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   5.160 +        evs \<in> set_mr |]
   5.161 +     ==> EKi = pubEK (CA i)"
   5.162 +apply (unfold cert_def signCert_def)
   5.163 +apply (blast dest!: Crypt_valid_pubEK)
   5.164 +done
   5.165 +
   5.166 +lemma Crypt_valid_pubSK:
   5.167 +     "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
   5.168 +           \<in> parts (knows Spy evs);
   5.169 +         evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
   5.170 +apply (erule rev_mp)
   5.171 +apply (erule set_mr.induct, auto)
   5.172 +done
   5.173 +
   5.174 +lemma certificate_valid_pubSK:
   5.175 +    "[| cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   5.176 +        evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
   5.177 +apply (unfold cert_def signCert_def)
   5.178 +apply (blast dest!: Crypt_valid_pubSK)
   5.179 +done
   5.180 +
   5.181 +lemma Gets_certificate_valid:
   5.182 +     "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
   5.183 +                      cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   5.184 +         evs \<in> set_mr |]
   5.185 +      ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
   5.186 +by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
   5.187 +
   5.188 +
   5.189 +text{*Nobody can have used non-existent keys!*}
   5.190 +lemma new_keys_not_used [rule_format,simp]:
   5.191 +     "evs \<in> set_mr
   5.192 +      ==> Key K \<notin> used evs --> K \<in> symKeys -->
   5.193 +          K \<notin> keysFor (parts (knows Spy evs))"
   5.194 +apply (erule set_mr.induct, simp_all)
   5.195 +txt{*Fake*}
   5.196 +apply (force dest!: usedI keysFor_parts_insert)
   5.197 +txt{*Message 2*}
   5.198 +apply force
   5.199 +txt{*Message 3*}
   5.200 +apply (blast dest: Gets_certificate_valid)
   5.201 +txt{*Message 4*}
   5.202 +apply force
   5.203 +done
   5.204 +
   5.205 +
   5.206 +subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*}
   5.207 +
   5.208 +lemma gen_new_keys_not_used [rule_format]:
   5.209 +     "evs \<in> set_mr
   5.210 +      ==> Key K \<notin> used evs --> K \<in> symKeys -->
   5.211 +          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   5.212 +by auto
   5.213 +
   5.214 +lemma gen_new_keys_not_analzd:
   5.215 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
   5.216 +      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   5.217 +by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
   5.218 +          dest: gen_new_keys_not_used)
   5.219 +
   5.220 +lemma analz_Key_image_insert_eq:
   5.221 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
   5.222 +      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   5.223 +          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   5.224 +by (simp add: gen_new_keys_not_analzd)
   5.225 +
   5.226 +
   5.227 +lemma Crypt_parts_imp_used:
   5.228 +     "[|Crypt K X \<in> parts (knows Spy evs);
   5.229 +        K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
   5.230 +apply (rule ccontr)
   5.231 +apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   5.232 +done
   5.233 +
   5.234 +lemma Crypt_analz_imp_used:
   5.235 +     "[|Crypt K X \<in> analz (knows Spy evs);
   5.236 +        K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
   5.237 +by (blast intro: Crypt_parts_imp_used)
   5.238 +
   5.239 +text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
   5.240 +for other keys aren't needed.*}
   5.241 +
   5.242 +lemma parts_image_priEK:
   5.243 +     "[|Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs));
   5.244 +        evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad"
   5.245 +by auto
   5.246 +
   5.247 +text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*}
   5.248 +lemma analz_image_priEK:
   5.249 +     "evs \<in> set_mr ==>
   5.250 +          (Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) =
   5.251 +          (priEK (CA i) \<in> KK | CA i \<in> bad)"
   5.252 +by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   5.253 +
   5.254 +
   5.255 +subsection{*Secrecy of Session Keys*}
   5.256 +
   5.257 +text{*This holds because if (priEK (CA i)) appears in any traffic then it must
   5.258 +  be known to the Spy, by @{text Spy_see_private_Key}*}
   5.259 +lemma merK_neq_priEK:
   5.260 +     "[|Key merK \<notin> analz (knows Spy evs);
   5.261 +        Key merK \<in> parts (knows Spy evs);
   5.262 +        evs \<in> set_mr|] ==> merK \<noteq> priEK C"
   5.263 +by blast
   5.264 +
   5.265 +text{*Lemma for message 4: either merK is compromised (when we don't care)
   5.266 +  or else merK hasn't been used to encrypt K.*}
   5.267 +lemma msg4_priEK_disj:
   5.268 +     "[|Gets B {|Crypt KM1
   5.269 +                       (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
   5.270 +                 Y|} \<in> set evs;
   5.271 +        evs \<in> set_mr|]
   5.272 +  ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
   5.273 +   &  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
   5.274 +apply (unfold sign_def)
   5.275 +apply (blast dest: merK_neq_priEK)
   5.276 +done
   5.277 +
   5.278 +
   5.279 +lemma Key_analz_image_Key_lemma:
   5.280 +     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
   5.281 +      ==>
   5.282 +      P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
   5.283 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   5.284 +
   5.285 +lemma symKey_compromise:
   5.286 +     "evs \<in> set_mr ==>
   5.287 +      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
   5.288 +               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
   5.289 +               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
   5.290 +apply (erule set_mr.induct)
   5.291 +apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
   5.292 +apply (drule_tac [7] msg4_priEK_disj)
   5.293 +apply (frule_tac [6] Gets_certificate_valid)
   5.294 +apply (safe del: impI)
   5.295 +apply (simp_all del: image_insert image_Un imp_disjL
   5.296 +         add: analz_image_keys_simps abbrev_simps analz_knows_absorb
   5.297 +              analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
   5.298 +              Spy_analz_private_Key analz_image_priEK)
   5.299 +  --{*23 seconds on a 1.8GHz machine*}
   5.300 +txt{*Fake*}
   5.301 +apply spy_analz
   5.302 +txt{*Message 3*}
   5.303 +apply auto
   5.304 +done
   5.305 +
   5.306 +lemma symKey_secrecy [rule_format]:
   5.307 +     "[|CA i \<notin> bad; K \<in> symKeys;  evs \<in> set_mr|]
   5.308 +      ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs -->
   5.309 +                Key K \<in> parts{X} -->
   5.310 +                Merchant m \<notin> bad -->
   5.311 +                Key K \<notin> analz (knows Spy evs)"
   5.312 +apply (erule set_mr.induct)
   5.313 +apply (drule_tac [7] msg4_priEK_disj)
   5.314 +apply (frule_tac [6] Gets_certificate_valid)
   5.315 +apply (safe del: impI)
   5.316 +apply (simp_all del: image_insert image_Un imp_disjL
   5.317 +         add: analz_image_keys_simps abbrev_simps analz_knows_absorb
   5.318 +              analz_knows_absorb2 analz_Key_image_insert_eq
   5.319 +              symKey_compromise notin_image_iff Spy_analz_private_Key
   5.320 +              analz_image_priEK)
   5.321 +txt{*Fake*}
   5.322 +apply spy_analz
   5.323 +txt{*Message 1*}
   5.324 +apply force
   5.325 +txt{*Message 3*}
   5.326 +apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
   5.327 +done
   5.328 +
   5.329 +subsection{*Unicity *}
   5.330 +
   5.331 +lemma msg4_Says_imp_Notes:
   5.332 + "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   5.333 +		    cert  M      merSK    onlySig (priSK (CA i)),
   5.334 +		    cert  M      merEK    onlyEnc (priSK (CA i)),
   5.335 +		    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   5.336 +    evs \<in> set_mr |]
   5.337 +  ==> Notes (CA i) (Key merSK) \<in> set evs
   5.338 +   &  Notes (CA i) (Key merEK) \<in> set evs"
   5.339 +apply (erule rev_mp)
   5.340 +apply (erule set_mr.induct)
   5.341 +apply (simp_all (no_asm_simp))
   5.342 +done
   5.343 +
   5.344 +text{*Unicity of merSK wrt a given CA:
   5.345 +  merSK uniquely identifies the other components, including merEK*}
   5.346 +lemma merSK_unicity:
   5.347 + "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   5.348 +		    cert  M      merSK    onlySig (priSK (CA i)),
   5.349 +		    cert  M      merEK    onlyEnc (priSK (CA i)),
   5.350 +		    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   5.351 +    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
   5.352 +		    cert  M'      merSK    onlySig (priSK (CA i)),
   5.353 +		    cert  M'      merEK'    onlyEnc (priSK (CA i)),
   5.354 +		    cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
   5.355 +    evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
   5.356 +apply (erule rev_mp)
   5.357 +apply (erule rev_mp)
   5.358 +apply (erule set_mr.induct)
   5.359 +apply (simp_all (no_asm_simp))
   5.360 +apply (blast dest!: msg4_Says_imp_Notes)
   5.361 +done
   5.362 +
   5.363 +text{*Unicity of merEK wrt a given CA:
   5.364 +  merEK uniquely identifies the other components, including merSK*}
   5.365 +lemma merEK_unicity:
   5.366 + "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   5.367 +		    cert  M      merSK    onlySig (priSK (CA i)),
   5.368 +		    cert  M      merEK    onlyEnc (priSK (CA i)),
   5.369 +		    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   5.370 +    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
   5.371 +		     cert  M'      merSK'    onlySig (priSK (CA i)),
   5.372 +		     cert  M'      merEK    onlyEnc (priSK (CA i)),
   5.373 +		     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
   5.374 +    evs \<in> set_mr |] 
   5.375 +  ==> M=M' & NM2=NM2' & merSK=merSK'"
   5.376 +apply (erule rev_mp)
   5.377 +apply (erule rev_mp)
   5.378 +apply (erule set_mr.induct)
   5.379 +apply (simp_all (no_asm_simp))
   5.380 +apply (blast dest!: msg4_Says_imp_Notes)
   5.381 +done
   5.382 +
   5.383 +
   5.384 +text{* -No interest on secrecy of nonces: they appear to be used
   5.385 +    only for freshness.
   5.386 +   -No interest on secrecy of merSK or merEK, as in CR.
   5.387 +   -There's no equivalent of the PAN*}
   5.388 +
   5.389 +
   5.390 +subsection{*Primary Goals of Merchant Registration *}
   5.391 +
   5.392 +subsubsection{*The merchant's certificates really were created by the CA,
   5.393 +provided the CA is uncompromised *}
   5.394 +
   5.395 +text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses 
   5.396 +  certificates of the same form.*}
   5.397 +lemma certificate_merSK_valid_lemma [intro]:
   5.398 +     "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
   5.399 +          \<in> parts (knows Spy evs);
   5.400 +        CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   5.401 + ==> \<exists>X Y Z. Says (CA i) M
   5.402 +                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
   5.403 +apply (erule rev_mp)
   5.404 +apply (erule set_mr.induct)
   5.405 +apply (simp_all (no_asm_simp))
   5.406 +apply auto
   5.407 +done
   5.408 +
   5.409 +lemma certificate_merSK_valid:
   5.410 +     "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
   5.411 +         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   5.412 + ==> \<exists>X Y Z. Says (CA i) M
   5.413 +                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
   5.414 +by auto
   5.415 +
   5.416 +lemma certificate_merEK_valid_lemma [intro]:
   5.417 +     "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
   5.418 +          \<in> parts (knows Spy evs);
   5.419 +        CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   5.420 + ==> \<exists>X Y Z. Says (CA i) M
   5.421 +                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
   5.422 +apply (erule rev_mp)
   5.423 +apply (erule set_mr.induct)
   5.424 +apply (simp_all (no_asm_simp))
   5.425 +apply auto
   5.426 +done
   5.427 +
   5.428 +lemma certificate_merEK_valid:
   5.429 +     "[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs);
   5.430 +         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   5.431 + ==> \<exists>X Y Z. Says (CA i) M
   5.432 +                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
   5.433 +by auto
   5.434 +
   5.435 +text{*The two certificates - for merSK and for merEK - cannot be proved to
   5.436 +  have originated together*}
   5.437 +
   5.438 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Sep 23 15:40:27 2003 +0200
     6.3 @@ -0,0 +1,1025 @@
     6.4 +(*  Title:      HOL/Auth/SET/MessageSET
     6.5 +    ID:         $Id$
     6.6 +    Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     6.7 +*)
     6.8 +
     6.9 +header{*The Message Theory, Modified for SET*}
    6.10 +
    6.11 +theory MessageSET = NatPair:
    6.12 +
    6.13 +subsection{*General Lemmas*}
    6.14 +
    6.15 +text{*Needed occasionally with @{text spy_analz_tac}, e.g. in
    6.16 +     @{text analz_insert_Key_newK}*}
    6.17 +
    6.18 +lemma Un_absorb3 [simp] : "A \<union> (B \<union> A) = B \<union> A"
    6.19 +by blast
    6.20 +
    6.21 +text{*Collapses redundant cases in the huge protocol proofs*}
    6.22 +lemmas disj_simps = disj_comms disj_left_absorb disj_assoc 
    6.23 +
    6.24 +text{*Effective with assumptions like @{term "K \<notin> range pubK"} and 
    6.25 +   @{term "K \<notin> invKey`range pubK"}*}
    6.26 +lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
    6.27 +by blast
    6.28 +
    6.29 +text{*Effective with the assumption @{term "KK \<subseteq> - (range(invKey o pubK))"} *}
    6.30 +lemma disjoint_image_iff: "(A <= - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)"
    6.31 +by blast
    6.32 +
    6.33 +
    6.34 +
    6.35 +types
    6.36 +  key = nat
    6.37 +
    6.38 +consts
    6.39 +  all_symmetric :: bool        --{*true if all keys are symmetric*}
    6.40 +  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    6.41 +
    6.42 +specification (invKey)
    6.43 +  invKey [simp]: "invKey (invKey K) = K"
    6.44 +  invKey_symmetric: "all_symmetric --> invKey = id"
    6.45 +    by (rule exI [of _ id], auto)
    6.46 +
    6.47 +
    6.48 +text{*The inverse of a symmetric key is itself; that of a public key
    6.49 +      is the private key and vice versa*}
    6.50 +
    6.51 +constdefs
    6.52 +  symKeys :: "key set"
    6.53 +  "symKeys == {K. invKey K = K}"
    6.54 +
    6.55 +text{*Agents. We allow any number of certification authorities, cardholders
    6.56 +            merchants, and payment gateways.*}
    6.57 +datatype
    6.58 +  agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
    6.59 +
    6.60 +text{*Messages*}
    6.61 +datatype
    6.62 +     msg = Agent  agent	    --{*Agent names*}
    6.63 +         | Number nat       --{*Ordinary integers, timestamps, ...*}
    6.64 +         | Nonce  nat       --{*Unguessable nonces*}
    6.65 +         | Pan    nat       --{*Unguessable Primary Account Numbers (??)*}
    6.66 +         | Key    key       --{*Crypto keys*}
    6.67 +	 | Hash   msg       --{*Hashing*}
    6.68 +	 | MPair  msg msg   --{*Compound messages*}
    6.69 +	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
    6.70 +
    6.71 +
    6.72 +(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    6.73 +syntax
    6.74 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    6.75 +
    6.76 +syntax (xsymbols)
    6.77 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    6.78 +
    6.79 +translations
    6.80 +  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    6.81 +  "{|x, y|}"      == "MPair x y"
    6.82 +
    6.83 +
    6.84 +constdefs
    6.85 +  nat_of_agent :: "agent => nat"
    6.86 +   "nat_of_agent == agent_case (curry nat2_to_nat 0)
    6.87 +			       (curry nat2_to_nat 1)
    6.88 +			       (curry nat2_to_nat 2)
    6.89 +			       (curry nat2_to_nat 3)
    6.90 +			       (nat2_to_nat (4,0))"
    6.91 +    --{*maps each agent to a unique natural number, for specifications*}
    6.92 +
    6.93 +text{*The function is indeed injective*}
    6.94 +lemma inj_nat_of_agent: "inj nat_of_agent"
    6.95 +by (simp add: nat_of_agent_def inj_on_def curry_def
    6.96 +              nat2_to_nat_inj [THEN inj_eq]  split: agent.split) 
    6.97 +
    6.98 +
    6.99 +constdefs
   6.100 +  (*Keys useful to decrypt elements of a message set*)
   6.101 +  keysFor :: "msg set => key set"
   6.102 +  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
   6.103 +
   6.104 +subsubsection{*Inductive definition of all "parts" of a message.*}
   6.105 +
   6.106 +consts  parts   :: "msg set => msg set"
   6.107 +inductive "parts H"
   6.108 +  intros
   6.109 +    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   6.110 +    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
   6.111 +    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   6.112 +    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
   6.113 +
   6.114 +
   6.115 +(*Monotonicity*)
   6.116 +lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
   6.117 +apply auto
   6.118 +apply (erule parts.induct)
   6.119 +apply (auto dest: Fst Snd Body)
   6.120 +done
   6.121 +
   6.122 +
   6.123 +subsubsection{*Inverse of keys*}
   6.124 +
   6.125 +(*Equations hold because constructors are injective; cannot prove for all f*)
   6.126 +lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
   6.127 +by auto
   6.128 +
   6.129 +lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
   6.130 +by auto
   6.131 +
   6.132 +lemma Cardholder_image_eq [simp]: "(Cardholder x \<in> Cardholder`A) = (x \<in> A)"
   6.133 +by auto
   6.134 +
   6.135 +lemma CA_image_eq [simp]: "(CA x \<in> CA`A) = (x \<in> A)"
   6.136 +by auto
   6.137 +
   6.138 +lemma Pan_image_eq [simp]: "(Pan x \<in> Pan`A) = (x \<in> A)"
   6.139 +by auto
   6.140 +
   6.141 +lemma Pan_Key_image_eq [simp]: "(Pan x \<notin> Key`A)"
   6.142 +by auto
   6.143 +
   6.144 +lemma Nonce_Pan_image_eq [simp]: "(Nonce x \<notin> Pan`A)"
   6.145 +by auto
   6.146 +
   6.147 +lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   6.148 +apply safe
   6.149 +apply (drule_tac f = invKey in arg_cong, simp)
   6.150 +done
   6.151 +
   6.152 +
   6.153 +subsection{*keysFor operator*}
   6.154 +
   6.155 +lemma keysFor_empty [simp]: "keysFor {} = {}"
   6.156 +by (unfold keysFor_def, blast)
   6.157 +
   6.158 +lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
   6.159 +by (unfold keysFor_def, blast)
   6.160 +
   6.161 +lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
   6.162 +by (unfold keysFor_def, blast)
   6.163 +
   6.164 +(*Monotonicity*)
   6.165 +lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
   6.166 +by (unfold keysFor_def, blast)
   6.167 +
   6.168 +lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
   6.169 +by (unfold keysFor_def, auto)
   6.170 +
   6.171 +lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
   6.172 +by (unfold keysFor_def, auto)
   6.173 +
   6.174 +lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
   6.175 +by (unfold keysFor_def, auto)
   6.176 +
   6.177 +lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
   6.178 +by (unfold keysFor_def, auto)
   6.179 +
   6.180 +lemma keysFor_insert_Pan [simp]: "keysFor (insert (Pan A) H) = keysFor H"
   6.181 +by (unfold keysFor_def, auto)
   6.182 +
   6.183 +lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
   6.184 +by (unfold keysFor_def, auto)
   6.185 +
   6.186 +lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
   6.187 +by (unfold keysFor_def, auto)
   6.188 +
   6.189 +lemma keysFor_insert_Crypt [simp]:
   6.190 +    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
   6.191 +by (unfold keysFor_def, auto)
   6.192 +
   6.193 +lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
   6.194 +by (unfold keysFor_def, auto)
   6.195 +
   6.196 +lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
   6.197 +by (unfold keysFor_def, blast)
   6.198 +
   6.199 +
   6.200 +subsection{*Inductive relation "parts"*}
   6.201 +
   6.202 +lemma MPair_parts:
   6.203 +     "[| {|X,Y|} \<in> parts H;
   6.204 +         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
   6.205 +by (blast dest: parts.Fst parts.Snd)
   6.206 +
   6.207 +declare MPair_parts [elim!]  parts.Body [dest!]
   6.208 +text{*NB These two rules are UNSAFE in the formal sense, as they discard the
   6.209 +     compound message.  They work well on THIS FILE.
   6.210 +  @{text MPair_parts} is left as SAFE because it speeds up proofs.
   6.211 +  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
   6.212 +
   6.213 +lemma parts_increasing: "H \<subseteq> parts(H)"
   6.214 +by blast
   6.215 +
   6.216 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   6.217 +
   6.218 +lemma parts_empty [simp]: "parts{} = {}"
   6.219 +apply safe
   6.220 +apply (erule parts.induct, blast+)
   6.221 +done
   6.222 +
   6.223 +lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   6.224 +by simp
   6.225 +
   6.226 +(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   6.227 +lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   6.228 +by (erule parts.induct, blast+)
   6.229 +
   6.230 +
   6.231 +subsubsection{*Unions*}
   6.232 +
   6.233 +lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   6.234 +by (intro Un_least parts_mono Un_upper1 Un_upper2)
   6.235 +
   6.236 +lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   6.237 +apply (rule subsetI)
   6.238 +apply (erule parts.induct, blast+)
   6.239 +done
   6.240 +
   6.241 +lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   6.242 +by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   6.243 +
   6.244 +lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   6.245 +apply (subst insert_is_Un [of _ H])
   6.246 +apply (simp only: parts_Un)
   6.247 +done
   6.248 +
   6.249 +(*TWO inserts to avoid looping.  This rewrite is better than nothing.
   6.250 +  Not suitable for Addsimps: its behaviour can be strange.*)
   6.251 +lemma parts_insert2:
   6.252 +     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   6.253 +apply (simp add: Un_assoc)
   6.254 +apply (simp add: parts_insert [symmetric])
   6.255 +done
   6.256 +
   6.257 +lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   6.258 +by (intro UN_least parts_mono UN_upper)
   6.259 +
   6.260 +lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   6.261 +apply (rule subsetI)
   6.262 +apply (erule parts.induct, blast+)
   6.263 +done
   6.264 +
   6.265 +lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   6.266 +by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   6.267 +
   6.268 +(*Added to simplify arguments to parts, analz and synth.
   6.269 +  NOTE: the UN versions are no longer used!*)
   6.270 +
   6.271 +
   6.272 +text{*This allows @{text blast} to simplify occurrences of
   6.273 +  @{term "parts(G\<union>H)"} in the assumption.*}
   6.274 +declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!]
   6.275 +
   6.276 +
   6.277 +lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   6.278 +by (blast intro: parts_mono [THEN [2] rev_subsetD])
   6.279 +
   6.280 +subsubsection{*Idempotence and transitivity*}
   6.281 +
   6.282 +lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   6.283 +by (erule parts.induct, blast+)
   6.284 +
   6.285 +lemma parts_idem [simp]: "parts (parts H) = parts H"
   6.286 +by blast
   6.287 +
   6.288 +lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   6.289 +by (drule parts_mono, blast)
   6.290 +
   6.291 +(*Cut*)
   6.292 +lemma parts_cut:
   6.293 +     "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
   6.294 +by (erule parts_trans, auto)
   6.295 +
   6.296 +lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   6.297 +by (force dest!: parts_cut intro: parts_insertI)
   6.298 +
   6.299 +
   6.300 +subsubsection{*Rewrite rules for pulling out atomic messages*}
   6.301 +
   6.302 +lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   6.303 +
   6.304 +
   6.305 +lemma parts_insert_Agent [simp]:
   6.306 +     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   6.307 +apply (rule parts_insert_eq_I)
   6.308 +apply (erule parts.induct, auto)
   6.309 +done
   6.310 +
   6.311 +lemma parts_insert_Nonce [simp]:
   6.312 +     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   6.313 +apply (rule parts_insert_eq_I)
   6.314 +apply (erule parts.induct, auto)
   6.315 +done
   6.316 +
   6.317 +lemma parts_insert_Number [simp]:
   6.318 +     "parts (insert (Number N) H) = insert (Number N) (parts H)"
   6.319 +apply (rule parts_insert_eq_I)
   6.320 +apply (erule parts.induct, auto)
   6.321 +done
   6.322 +
   6.323 +lemma parts_insert_Key [simp]:
   6.324 +     "parts (insert (Key K) H) = insert (Key K) (parts H)"
   6.325 +apply (rule parts_insert_eq_I)
   6.326 +apply (erule parts.induct, auto)
   6.327 +done
   6.328 +
   6.329 +lemma parts_insert_Pan [simp]:
   6.330 +     "parts (insert (Pan A) H) = insert (Pan A) (parts H)"
   6.331 +apply (rule parts_insert_eq_I)
   6.332 +apply (erule parts.induct, auto)
   6.333 +done
   6.334 +
   6.335 +lemma parts_insert_Hash [simp]:
   6.336 +     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   6.337 +apply (rule parts_insert_eq_I)
   6.338 +apply (erule parts.induct, auto)
   6.339 +done
   6.340 +
   6.341 +lemma parts_insert_Crypt [simp]:
   6.342 +     "parts (insert (Crypt K X) H) =
   6.343 +          insert (Crypt K X) (parts (insert X H))"
   6.344 +apply (rule equalityI)
   6.345 +apply (rule subsetI)
   6.346 +apply (erule parts.induct, auto)
   6.347 +apply (erule parts.induct)
   6.348 +apply (blast intro: parts.Body)+
   6.349 +done
   6.350 +
   6.351 +lemma parts_insert_MPair [simp]:
   6.352 +     "parts (insert {|X,Y|} H) =
   6.353 +          insert {|X,Y|} (parts (insert X (insert Y H)))"
   6.354 +apply (rule equalityI)
   6.355 +apply (rule subsetI)
   6.356 +apply (erule parts.induct, auto)
   6.357 +apply (erule parts.induct)
   6.358 +apply (blast intro: parts.Fst parts.Snd)+
   6.359 +done
   6.360 +
   6.361 +lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   6.362 +apply auto
   6.363 +apply (erule parts.induct, auto)
   6.364 +done
   6.365 +
   6.366 +lemma parts_image_Pan [simp]: "parts (Pan`A) = Pan`A"
   6.367 +apply auto
   6.368 +apply (erule parts.induct, auto)
   6.369 +done
   6.370 +
   6.371 +
   6.372 +(*In any message, there is an upper bound N on its greatest nonce.*)
   6.373 +lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   6.374 +apply (induct_tac "msg")
   6.375 +apply (simp_all (no_asm_simp) add: exI parts_insert2)
   6.376 +(*MPair case: blast_tac works out the necessary sum itself!*)
   6.377 +prefer 2 apply (blast elim!: add_leE)
   6.378 +(*Nonce case*)
   6.379 +apply (rule_tac x = "N + Suc nat" in exI)
   6.380 +apply (auto elim!: add_leE)
   6.381 +done
   6.382 +
   6.383 +(* Ditto, for numbers.*)
   6.384 +lemma msg_Number_supply: "\<exists>N. \<forall>n. N<=n --> Number n \<notin> parts {msg}"
   6.385 +apply (induct_tac "msg")
   6.386 +apply (simp_all (no_asm_simp) add: exI parts_insert2)
   6.387 +prefer 2 apply (blast elim!: add_leE)
   6.388 +apply (rule_tac x = "N + Suc nat" in exI, auto)
   6.389 +done
   6.390 +
   6.391 +subsection{*Inductive relation "analz"*}
   6.392 +
   6.393 +text{*Inductive definition of "analz" -- what can be broken down from a set of
   6.394 +    messages, including keys.  A form of downward closure.  Pairs can
   6.395 +    be taken apart; messages decrypted with known keys.*}
   6.396 +
   6.397 +consts  analz   :: "msg set => msg set"
   6.398 +inductive "analz H"
   6.399 +  intros
   6.400 +    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   6.401 +    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   6.402 +    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   6.403 +    Decrypt [dest]:
   6.404 +             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   6.405 +
   6.406 +
   6.407 +(*Monotonicity; Lemma 1 of Lowe's paper*)
   6.408 +lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   6.409 +apply auto
   6.410 +apply (erule analz.induct)
   6.411 +apply (auto dest: Fst Snd)
   6.412 +done
   6.413 +
   6.414 +text{*Making it safe speeds up proofs*}
   6.415 +lemma MPair_analz [elim!]:
   6.416 +     "[| {|X,Y|} \<in> analz H;
   6.417 +             [| X \<in> analz H; Y \<in> analz H |] ==> P
   6.418 +          |] ==> P"
   6.419 +by (blast dest: analz.Fst analz.Snd)
   6.420 +
   6.421 +lemma analz_increasing: "H \<subseteq> analz(H)"
   6.422 +by blast
   6.423 +
   6.424 +lemma analz_subset_parts: "analz H \<subseteq> parts H"
   6.425 +apply (rule subsetI)
   6.426 +apply (erule analz.induct, blast+)
   6.427 +done
   6.428 +
   6.429 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   6.430 +
   6.431 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   6.432 +
   6.433 +
   6.434 +lemma parts_analz [simp]: "parts (analz H) = parts H"
   6.435 +apply (rule equalityI)
   6.436 +apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
   6.437 +apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
   6.438 +done
   6.439 +
   6.440 +lemma analz_parts [simp]: "analz (parts H) = parts H"
   6.441 +apply auto
   6.442 +apply (erule analz.induct, auto)
   6.443 +done
   6.444 +
   6.445 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   6.446 +
   6.447 +subsubsection{*General equational properties*}
   6.448 +
   6.449 +lemma analz_empty [simp]: "analz{} = {}"
   6.450 +apply safe
   6.451 +apply (erule analz.induct, blast+)
   6.452 +done
   6.453 +
   6.454 +(*Converse fails: we can analz more from the union than from the
   6.455 +  separate parts, as a key in one might decrypt a message in the other*)
   6.456 +lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   6.457 +by (intro Un_least analz_mono Un_upper1 Un_upper2)
   6.458 +
   6.459 +lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   6.460 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   6.461 +
   6.462 +subsubsection{*Rewrite rules for pulling out atomic messages*}
   6.463 +
   6.464 +lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   6.465 +
   6.466 +lemma analz_insert_Agent [simp]:
   6.467 +     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   6.468 +apply (rule analz_insert_eq_I)
   6.469 +apply (erule analz.induct, auto)
   6.470 +done
   6.471 +
   6.472 +lemma analz_insert_Nonce [simp]:
   6.473 +     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   6.474 +apply (rule analz_insert_eq_I)
   6.475 +apply (erule analz.induct, auto)
   6.476 +done
   6.477 +
   6.478 +lemma analz_insert_Number [simp]:
   6.479 +     "analz (insert (Number N) H) = insert (Number N) (analz H)"
   6.480 +apply (rule analz_insert_eq_I)
   6.481 +apply (erule analz.induct, auto)
   6.482 +done
   6.483 +
   6.484 +lemma analz_insert_Hash [simp]:
   6.485 +     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   6.486 +apply (rule analz_insert_eq_I)
   6.487 +apply (erule analz.induct, auto)
   6.488 +done
   6.489 +
   6.490 +(*Can only pull out Keys if they are not needed to decrypt the rest*)
   6.491 +lemma analz_insert_Key [simp]:
   6.492 +    "K \<notin> keysFor (analz H) ==>
   6.493 +          analz (insert (Key K) H) = insert (Key K) (analz H)"
   6.494 +apply (unfold keysFor_def)
   6.495 +apply (rule analz_insert_eq_I)
   6.496 +apply (erule analz.induct, auto)
   6.497 +done
   6.498 +
   6.499 +lemma analz_insert_MPair [simp]:
   6.500 +     "analz (insert {|X,Y|} H) =
   6.501 +          insert {|X,Y|} (analz (insert X (insert Y H)))"
   6.502 +apply (rule equalityI)
   6.503 +apply (rule subsetI)
   6.504 +apply (erule analz.induct, auto)
   6.505 +apply (erule analz.induct)
   6.506 +apply (blast intro: analz.Fst analz.Snd)+
   6.507 +done
   6.508 +
   6.509 +(*Can pull out enCrypted message if the Key is not known*)
   6.510 +lemma analz_insert_Crypt:
   6.511 +     "Key (invKey K) \<notin> analz H
   6.512 +      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   6.513 +apply (rule analz_insert_eq_I)
   6.514 +apply (erule analz.induct, auto)
   6.515 +done
   6.516 +
   6.517 +lemma analz_insert_Pan [simp]:
   6.518 +     "analz (insert (Pan A) H) = insert (Pan A) (analz H)"
   6.519 +apply (rule analz_insert_eq_I)
   6.520 +apply (erule analz.induct, auto)
   6.521 +done
   6.522 +
   6.523 +lemma lemma1: "Key (invKey K) \<in> analz H ==>
   6.524 +               analz (insert (Crypt K X) H) \<subseteq>
   6.525 +               insert (Crypt K X) (analz (insert X H))"
   6.526 +apply (rule subsetI)
   6.527 +apply (erule_tac xa = x in analz.induct, auto)
   6.528 +done
   6.529 +
   6.530 +lemma lemma2: "Key (invKey K) \<in> analz H ==>
   6.531 +               insert (Crypt K X) (analz (insert X H)) \<subseteq>
   6.532 +               analz (insert (Crypt K X) H)"
   6.533 +apply auto
   6.534 +apply (erule_tac xa = x in analz.induct, auto)
   6.535 +apply (blast intro: analz_insertI analz.Decrypt)
   6.536 +done
   6.537 +
   6.538 +lemma analz_insert_Decrypt:
   6.539 +     "Key (invKey K) \<in> analz H ==>
   6.540 +               analz (insert (Crypt K X) H) =
   6.541 +               insert (Crypt K X) (analz (insert X H))"
   6.542 +by (intro equalityI lemma1 lemma2)
   6.543 +
   6.544 +(*Case analysis: either the message is secure, or it is not!
   6.545 +  Effective, but can cause subgoals to blow up!
   6.546 +  Use with split_if;  apparently split_tac does not cope with patterns
   6.547 +  such as "analz (insert (Crypt K X) H)" *)
   6.548 +lemma analz_Crypt_if [simp]:
   6.549 +     "analz (insert (Crypt K X) H) =
   6.550 +          (if (Key (invKey K) \<in> analz H)
   6.551 +           then insert (Crypt K X) (analz (insert X H))
   6.552 +           else insert (Crypt K X) (analz H))"
   6.553 +by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   6.554 +
   6.555 +
   6.556 +(*This rule supposes "for the sake of argument" that we have the key.*)
   6.557 +lemma analz_insert_Crypt_subset:
   6.558 +     "analz (insert (Crypt K X) H) \<subseteq>
   6.559 +           insert (Crypt K X) (analz (insert X H))"
   6.560 +apply (rule subsetI)
   6.561 +apply (erule analz.induct, auto)
   6.562 +done
   6.563 +
   6.564 +lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   6.565 +apply auto
   6.566 +apply (erule analz.induct, auto)
   6.567 +done
   6.568 +
   6.569 +lemma analz_image_Pan [simp]: "analz (Pan`A) = Pan`A"
   6.570 +apply auto
   6.571 +apply (erule analz.induct, auto)
   6.572 +done
   6.573 +
   6.574 +
   6.575 +subsubsection{*Idempotence and transitivity*}
   6.576 +
   6.577 +lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   6.578 +by (erule analz.induct, blast+)
   6.579 +
   6.580 +lemma analz_idem [simp]: "analz (analz H) = analz H"
   6.581 +by blast
   6.582 +
   6.583 +lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   6.584 +by (drule analz_mono, blast)
   6.585 +
   6.586 +(*Cut; Lemma 2 of Lowe*)
   6.587 +lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   6.588 +by (erule analz_trans, blast)
   6.589 +
   6.590 +(*Cut can be proved easily by induction on
   6.591 +   "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   6.592 +*)
   6.593 +
   6.594 +(*This rewrite rule helps in the simplification of messages that involve
   6.595 +  the forwarding of unknown components (X).  Without it, removing occurrences
   6.596 +  of X can be very complicated. *)
   6.597 +lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   6.598 +by (blast intro: analz_cut analz_insertI)
   6.599 +
   6.600 +
   6.601 +text{*A congruence rule for "analz"*}
   6.602 +
   6.603 +lemma analz_subset_cong:
   6.604 +     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
   6.605 +               |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   6.606 +apply clarify
   6.607 +apply (erule analz.induct)
   6.608 +apply (best intro: analz_mono [THEN subsetD])+
   6.609 +done
   6.610 +
   6.611 +lemma analz_cong:
   6.612 +     "[| analz G = analz G'; analz H = analz H'
   6.613 +               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   6.614 +by (intro equalityI analz_subset_cong, simp_all)
   6.615 +
   6.616 +lemma analz_insert_cong:
   6.617 +     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   6.618 +by (force simp only: insert_def intro!: analz_cong)
   6.619 +
   6.620 +(*If there are no pairs or encryptions then analz does nothing*)
   6.621 +lemma analz_trivial:
   6.622 +     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   6.623 +apply safe
   6.624 +apply (erule analz.induct, blast+)
   6.625 +done
   6.626 +
   6.627 +(*These two are obsolete (with a single Spy) but cost little to prove...*)
   6.628 +lemma analz_UN_analz_lemma:
   6.629 +     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   6.630 +apply (erule analz.induct)
   6.631 +apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   6.632 +done
   6.633 +
   6.634 +lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   6.635 +by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   6.636 +
   6.637 +
   6.638 +subsection{*Inductive relation "synth"*}
   6.639 +
   6.640 +text{*Inductive definition of "synth" -- what can be built up from a set of
   6.641 +    messages.  A form of upward closure.  Pairs can be built, messages
   6.642 +    encrypted with known keys.  Agent names are public domain.
   6.643 +    Numbers can be guessed, but Nonces cannot be.*}
   6.644 +
   6.645 +consts  synth   :: "msg set => msg set"
   6.646 +inductive "synth H"
   6.647 +  intros
   6.648 +    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   6.649 +    Agent  [intro]:   "Agent agt \<in> synth H"
   6.650 +    Number [intro]:   "Number n  \<in> synth H"
   6.651 +    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   6.652 +    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   6.653 +    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   6.654 +
   6.655 +(*Monotonicity*)
   6.656 +lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   6.657 +apply auto
   6.658 +apply (erule synth.induct)
   6.659 +apply (auto dest: Fst Snd Body)
   6.660 +done
   6.661 +
   6.662 +(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
   6.663 +inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
   6.664 +inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
   6.665 +inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
   6.666 +inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   6.667 +inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   6.668 +inductive_cases Pan_synth   [elim!]: "Pan A \<in> synth H"
   6.669 +
   6.670 +
   6.671 +lemma synth_increasing: "H \<subseteq> synth(H)"
   6.672 +by blast
   6.673 +
   6.674 +subsubsection{*Unions*}
   6.675 +
   6.676 +(*Converse fails: we can synth more from the union than from the
   6.677 +  separate parts, building a compound message using elements of each.*)
   6.678 +lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   6.679 +by (intro Un_least synth_mono Un_upper1 Un_upper2)
   6.680 +
   6.681 +lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   6.682 +by (blast intro: synth_mono [THEN [2] rev_subsetD])
   6.683 +
   6.684 +subsubsection{*Idempotence and transitivity*}
   6.685 +
   6.686 +lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   6.687 +by (erule synth.induct, blast+)
   6.688 +
   6.689 +lemma synth_idem: "synth (synth H) = synth H"
   6.690 +by blast
   6.691 +
   6.692 +lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   6.693 +by (drule synth_mono, blast)
   6.694 +
   6.695 +(*Cut; Lemma 2 of Lowe*)
   6.696 +lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   6.697 +by (erule synth_trans, blast)
   6.698 +
   6.699 +lemma Agent_synth [simp]: "Agent A \<in> synth H"
   6.700 +by blast
   6.701 +
   6.702 +lemma Number_synth [simp]: "Number n \<in> synth H"
   6.703 +by blast
   6.704 +
   6.705 +lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   6.706 +by blast
   6.707 +
   6.708 +lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   6.709 +by blast
   6.710 +
   6.711 +lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   6.712 +by blast
   6.713 +
   6.714 +lemma Pan_synth_eq [simp]: "(Pan A \<in> synth H) = (Pan A \<in> H)"
   6.715 +by blast
   6.716 +
   6.717 +lemma keysFor_synth [simp]:
   6.718 +    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   6.719 +by (unfold keysFor_def, blast)
   6.720 +
   6.721 +
   6.722 +subsubsection{*Combinations of parts, analz and synth*}
   6.723 +
   6.724 +lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   6.725 +apply (rule equalityI)
   6.726 +apply (rule subsetI)
   6.727 +apply (erule parts.induct)
   6.728 +apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
   6.729 +                    parts.Fst parts.Snd parts.Body)+
   6.730 +done
   6.731 +
   6.732 +lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   6.733 +apply (intro equalityI analz_subset_cong)+
   6.734 +apply simp_all
   6.735 +done
   6.736 +
   6.737 +lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   6.738 +apply (rule equalityI)
   6.739 +apply (rule subsetI)
   6.740 +apply (erule analz.induct)
   6.741 +prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   6.742 +apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
   6.743 +done
   6.744 +
   6.745 +lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   6.746 +apply (cut_tac H = "{}" in analz_synth_Un)
   6.747 +apply (simp (no_asm_use))
   6.748 +done
   6.749 +
   6.750 +
   6.751 +subsubsection{*For reasoning about the Fake rule in traces*}
   6.752 +
   6.753 +lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   6.754 +by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   6.755 +
   6.756 +(*More specifically for Fake.  Very occasionally we could do with a version
   6.757 +  of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   6.758 +lemma Fake_parts_insert: "X \<in> synth (analz H) ==>
   6.759 +      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   6.760 +apply (drule parts_insert_subset_Un)
   6.761 +apply (simp (no_asm_use))
   6.762 +apply blast
   6.763 +done
   6.764 +
   6.765 +lemma Fake_parts_insert_in_Un:
   6.766 +     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   6.767 +      ==> Z \<in>  synth (analz H) \<union> parts H";
   6.768 +by (blast dest: Fake_parts_insert [THEN subsetD, dest])
   6.769 +
   6.770 +(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   6.771 +lemma Fake_analz_insert:
   6.772 +     "X\<in> synth (analz G) ==>
   6.773 +      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   6.774 +apply (rule subsetI)
   6.775 +apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   6.776 +prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
   6.777 +apply (simp (no_asm_use))
   6.778 +apply blast
   6.779 +done
   6.780 +
   6.781 +lemma analz_conj_parts [simp]:
   6.782 +     "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   6.783 +by (blast intro: analz_subset_parts [THEN subsetD])
   6.784 +
   6.785 +lemma analz_disj_parts [simp]:
   6.786 +     "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   6.787 +by (blast intro: analz_subset_parts [THEN subsetD])
   6.788 +
   6.789 +(*Without this equation, other rules for synth and analz would yield
   6.790 +  redundant cases*)
   6.791 +lemma MPair_synth_analz [iff]:
   6.792 +     "({|X,Y|} \<in> synth (analz H)) =
   6.793 +      (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   6.794 +by blast
   6.795 +
   6.796 +lemma Crypt_synth_analz:
   6.797 +     "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]
   6.798 +       ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   6.799 +by blast
   6.800 +
   6.801 +
   6.802 +lemma Hash_synth_analz [simp]:
   6.803 +     "X \<notin> synth (analz H)
   6.804 +      ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
   6.805 +by blast
   6.806 +
   6.807 +
   6.808 +(*We do NOT want Crypt... messages broken up in protocols!!*)
   6.809 +declare parts.Body [rule del]
   6.810 +
   6.811 +
   6.812 +text{*Rewrites to push in Key and Crypt messages, so that other messages can
   6.813 +    be pulled out using the @{text analz_insert} rules*}
   6.814 +ML
   6.815 +{*
   6.816 +fun insComm x y = inst "x" x (inst "y" y insert_commute);
   6.817 +
   6.818 +bind_thms ("pushKeys",
   6.819 +           map (insComm "Key ?K")
   6.820 +                   ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
   6.821 +		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
   6.822 +
   6.823 +bind_thms ("pushCrypts",
   6.824 +           map (insComm "Crypt ?X ?K")
   6.825 +                     ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
   6.826 +		      "Hash ?X'", "MPair ?X' ?Y"]);
   6.827 +*}
   6.828 +
   6.829 +text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   6.830 +  re-ordered.*}
   6.831 +lemmas pushes = pushKeys pushCrypts
   6.832 +
   6.833 +
   6.834 +subsection{*Tactics useful for many protocol proofs*}
   6.835 +ML
   6.836 +{*
   6.837 +val invKey = thm "invKey"
   6.838 +val keysFor_def = thm "keysFor_def"
   6.839 +val symKeys_def = thm "symKeys_def"
   6.840 +val parts_mono = thm "parts_mono";
   6.841 +val analz_mono = thm "analz_mono";
   6.842 +val Key_image_eq = thm "Key_image_eq";
   6.843 +val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
   6.844 +val keysFor_Un = thm "keysFor_Un";
   6.845 +val keysFor_mono = thm "keysFor_mono";
   6.846 +val keysFor_image_Key = thm "keysFor_image_Key";
   6.847 +val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
   6.848 +val MPair_parts = thm "MPair_parts";
   6.849 +val parts_increasing = thm "parts_increasing";
   6.850 +val parts_insertI = thm "parts_insertI";
   6.851 +val parts_empty = thm "parts_empty";
   6.852 +val parts_emptyE = thm "parts_emptyE";
   6.853 +val parts_singleton = thm "parts_singleton";
   6.854 +val parts_Un_subset1 = thm "parts_Un_subset1";
   6.855 +val parts_Un_subset2 = thm "parts_Un_subset2";
   6.856 +val parts_insert = thm "parts_insert";
   6.857 +val parts_insert2 = thm "parts_insert2";
   6.858 +val parts_UN_subset1 = thm "parts_UN_subset1";
   6.859 +val parts_UN_subset2 = thm "parts_UN_subset2";
   6.860 +val parts_UN = thm "parts_UN";
   6.861 +val parts_insert_subset = thm "parts_insert_subset";
   6.862 +val parts_partsD = thm "parts_partsD";
   6.863 +val parts_trans = thm "parts_trans";
   6.864 +val parts_cut = thm "parts_cut";
   6.865 +val parts_cut_eq = thm "parts_cut_eq";
   6.866 +val parts_insert_eq_I = thm "parts_insert_eq_I";
   6.867 +val parts_image_Key = thm "parts_image_Key";
   6.868 +val MPair_analz = thm "MPair_analz";
   6.869 +val analz_increasing = thm "analz_increasing";
   6.870 +val analz_subset_parts = thm "analz_subset_parts";
   6.871 +val not_parts_not_analz = thm "not_parts_not_analz";
   6.872 +val parts_analz = thm "parts_analz";
   6.873 +val analz_parts = thm "analz_parts";
   6.874 +val analz_insertI = thm "analz_insertI";
   6.875 +val analz_empty = thm "analz_empty";
   6.876 +val analz_Un = thm "analz_Un";
   6.877 +val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
   6.878 +val analz_image_Key = thm "analz_image_Key";
   6.879 +val analz_analzD = thm "analz_analzD";
   6.880 +val analz_trans = thm "analz_trans";
   6.881 +val analz_cut = thm "analz_cut";
   6.882 +val analz_insert_eq = thm "analz_insert_eq";
   6.883 +val analz_subset_cong = thm "analz_subset_cong";
   6.884 +val analz_cong = thm "analz_cong";
   6.885 +val analz_insert_cong = thm "analz_insert_cong";
   6.886 +val analz_trivial = thm "analz_trivial";
   6.887 +val analz_UN_analz = thm "analz_UN_analz";
   6.888 +val synth_mono = thm "synth_mono";
   6.889 +val synth_increasing = thm "synth_increasing";
   6.890 +val synth_Un = thm "synth_Un";
   6.891 +val synth_insert = thm "synth_insert";
   6.892 +val synth_synthD = thm "synth_synthD";
   6.893 +val synth_trans = thm "synth_trans";
   6.894 +val synth_cut = thm "synth_cut";
   6.895 +val Agent_synth = thm "Agent_synth";
   6.896 +val Number_synth = thm "Number_synth";
   6.897 +val Nonce_synth_eq = thm "Nonce_synth_eq";
   6.898 +val Key_synth_eq = thm "Key_synth_eq";
   6.899 +val Crypt_synth_eq = thm "Crypt_synth_eq";
   6.900 +val keysFor_synth = thm "keysFor_synth";
   6.901 +val parts_synth = thm "parts_synth";
   6.902 +val analz_analz_Un = thm "analz_analz_Un";
   6.903 +val analz_synth_Un = thm "analz_synth_Un";
   6.904 +val analz_synth = thm "analz_synth";
   6.905 +val parts_insert_subset_Un = thm "parts_insert_subset_Un";
   6.906 +val Fake_parts_insert = thm "Fake_parts_insert";
   6.907 +val Fake_analz_insert = thm "Fake_analz_insert";
   6.908 +val analz_conj_parts = thm "analz_conj_parts";
   6.909 +val analz_disj_parts = thm "analz_disj_parts";
   6.910 +val MPair_synth_analz = thm "MPair_synth_analz";
   6.911 +val Crypt_synth_analz = thm "Crypt_synth_analz";
   6.912 +val Hash_synth_analz = thm "Hash_synth_analz";
   6.913 +val pushes = thms "pushes";
   6.914 +
   6.915 +
   6.916 +(*Prove base case (subgoal i) and simplify others.  A typical base case
   6.917 +  concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   6.918 +  alone.*)
   6.919 +fun prove_simple_subgoals_tac i =
   6.920 +    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
   6.921 +    ALLGOALS Asm_simp_tac
   6.922 +
   6.923 +(*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   6.924 +  but this application is no longer necessary if analz_insert_eq is used.
   6.925 +  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   6.926 +  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   6.927 +
   6.928 +(*Apply rules to break down assumptions of the form
   6.929 +  Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
   6.930 +*)
   6.931 +val Fake_insert_tac =
   6.932 +    dresolve_tac [impOfSubs Fake_analz_insert,
   6.933 +                  impOfSubs Fake_parts_insert] THEN'
   6.934 +    eresolve_tac [asm_rl, thm"synth.Inj"];
   6.935 +
   6.936 +fun Fake_insert_simp_tac ss i =
   6.937 +    REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
   6.938 +
   6.939 +fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
   6.940 +    (Fake_insert_simp_tac ss 1
   6.941 +     THEN
   6.942 +     IF_UNSOLVED (Blast.depth_tac
   6.943 +		  (cs addIs [analz_insertI,
   6.944 +				   impOfSubs analz_subset_parts]) 4 1))
   6.945 +
   6.946 +(*The explicit claset and simpset arguments help it work with Isar*)
   6.947 +fun gen_spy_analz_tac (cs,ss) i =
   6.948 +  DETERM
   6.949 +   (SELECT_GOAL
   6.950 +     (EVERY
   6.951 +      [  (*push in occurrences of X...*)
   6.952 +       (REPEAT o CHANGED)
   6.953 +           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   6.954 +       (*...allowing further simplifications*)
   6.955 +       simp_tac ss 1,
   6.956 +       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   6.957 +       DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   6.958 +
   6.959 +fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
   6.960 +*}
   6.961 +
   6.962 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
   6.963 +  this means that some terms displayed as (f o g) will be rewritten, and others
   6.964 +  will not!*)
   6.965 +declare o_def [simp]
   6.966 +
   6.967 +
   6.968 +lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
   6.969 +by auto
   6.970 +
   6.971 +lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
   6.972 +by auto
   6.973 +
   6.974 +lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
   6.975 +by (simp add: synth_mono analz_mono)
   6.976 +
   6.977 +lemma Fake_analz_eq [simp]:
   6.978 +     "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
   6.979 +apply (drule Fake_analz_insert[of _ _ "H"])
   6.980 +apply (simp add: synth_increasing[THEN Un_absorb2])
   6.981 +apply (drule synth_mono)
   6.982 +apply (simp add: synth_idem)
   6.983 +apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
   6.984 +done
   6.985 +
   6.986 +text{*Two generalizations of @{text analz_insert_eq}*}
   6.987 +lemma gen_analz_insert_eq [rule_format]:
   6.988 +     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   6.989 +by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   6.990 +
   6.991 +lemma synth_analz_insert_eq [rule_format]:
   6.992 +     "X \<in> synth (analz H)
   6.993 +      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   6.994 +apply (erule synth.induct)
   6.995 +apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
   6.996 +done
   6.997 +
   6.998 +lemma Fake_parts_sing:
   6.999 +     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
  6.1000 +apply (rule subset_trans)
  6.1001 + apply (erule_tac [2] Fake_parts_insert)
  6.1002 +apply (simp add: parts_mono)
  6.1003 +done
  6.1004 +
  6.1005 +lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
  6.1006 +
  6.1007 +method_setup spy_analz = {*
  6.1008 +    Method.ctxt_args (fn ctxt =>
  6.1009 +        Method.METHOD (fn facts =>
  6.1010 +            gen_spy_analz_tac (Classical.get_local_claset ctxt,
  6.1011 +                               Simplifier.get_local_simpset ctxt) 1))*}
  6.1012 +    "for proving the Fake case when analz is involved"
  6.1013 +
  6.1014 +method_setup atomic_spy_analz = {*
  6.1015 +    Method.ctxt_args (fn ctxt =>
  6.1016 +        Method.METHOD (fn facts =>
  6.1017 +            atomic_spy_analz_tac (Classical.get_local_claset ctxt,
  6.1018 +                                  Simplifier.get_local_simpset ctxt) 1))*}
  6.1019 +    "for debugging spy_analz"
  6.1020 +
  6.1021 +method_setup Fake_insert_simp = {*
  6.1022 +    Method.ctxt_args (fn ctxt =>
  6.1023 +        Method.METHOD (fn facts =>
  6.1024 +            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1))*}
  6.1025 +    "for debugging spy_analz"
  6.1026 +
  6.1027 +
  6.1028 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Tue Sep 23 15:40:27 2003 +0200
     7.3 @@ -0,0 +1,586 @@
     7.4 +(*  Title:      HOL/Auth/SET/PublicSET
     7.5 +    ID:         $Id$
     7.6 +    Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     7.7 +*)
     7.8 +
     7.9 +header{*The Public-Key Theory, Modified for SET*}
    7.10 +
    7.11 +theory PublicSET = EventSET:
    7.12 +
    7.13 +subsection{*Symmetric and Asymmetric Keys*}
    7.14 +
    7.15 +axioms
    7.16 +  Key_supply_ax:
    7.17 +      "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs & K \<in> symKeys"
    7.18 +  --{*Unlike the corresponding property of nonces, this cannot be proved.
    7.19 +    We have infinitely many agents and there is nothing to stop their
    7.20 +    keys from exhausting all the natural numbers.  The axiom
    7.21 +    assumes that their keys are dispersed so as to leave room for infinitely
    7.22 +    many fresh session keys.  We could, alternatively, restrict agents to
    7.23 +    an unspecified finite number.*}
    7.24 +
    7.25 +
    7.26 +text{*definitions influenced by the wish to assign asymmetric keys 
    7.27 +  - since the beginning - only to RCA and CAs, namely we need a partial 
    7.28 +  function on type Agent*}
    7.29 +
    7.30 +
    7.31 +text{*The SET specs mention two signature keys for CAs - we only have one*}
    7.32 +
    7.33 +consts
    7.34 +  publicKey :: "[bool, agent] => key"
    7.35 +    --{*the boolean is TRUE if a signing key*}
    7.36 +
    7.37 +syntax
    7.38 +  pubEK :: "agent => key"
    7.39 +  pubSK :: "agent => key"
    7.40 +  priEK :: "agent => key"
    7.41 +  priSK :: "agent => key"
    7.42 +
    7.43 +translations
    7.44 +  "pubEK"  == "publicKey False"
    7.45 +  "pubSK"  == "publicKey True"
    7.46 +
    7.47 +  (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
    7.48 +  "priEK A"  == "invKey (pubEK A)"
    7.49 +  "priSK A"  == "invKey (pubSK A)"
    7.50 +
    7.51 +text{*By freeness of agents, no two agents have the same key. Since
    7.52 + @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
    7.53 +
    7.54 +specification (publicKey)
    7.55 +  injective_publicKey:
    7.56 +    "publicKey b A = publicKey c A' ==> b=c & A=A'"
    7.57 +   apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) 
    7.58 +   apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) 
    7.59 +   apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
    7.60 +(*or this, but presburger won't abstract out the function applications
    7.61 +   apply presburger+
    7.62 +*)
    7.63 +   done                       
    7.64 +
    7.65 +
    7.66 +axioms
    7.67 +  (*No private key equals any public key (essential to ensure that private
    7.68 +    keys are private!) *)
    7.69 +  privateKey_neq_publicKey [iff]:
    7.70 +      "invKey (publicKey b A) \<noteq> publicKey b' A'"
    7.71 +
    7.72 +declare privateKey_neq_publicKey [THEN not_sym, iff]
    7.73 +
    7.74 +  
    7.75 +subsection{*Initial Knowledge*}
    7.76 +
    7.77 +text{*This information is not necessary.  Each protocol distributes any needed
    7.78 +certificates, and anyway our proofs require a formalization of the Spy's 
    7.79 +knowledge only.  However, the initial knowledge is as follows:
    7.80 +   All agents know RCA's public keys;
    7.81 +   RCA and CAs know their own respective keys;
    7.82 +   RCA (has already certified and therefore) knows all CAs public keys; 
    7.83 +   Spy knows all keys of all bad agents.*}
    7.84 +primrec    
    7.85 +
    7.86 +  initState_CA:
    7.87 +    "initState (CA i)  =
    7.88 +       (if i=0 then Key ` ({priEK RCA, priSK RCA} Un
    7.89 +			    pubEK ` (range CA) Un pubSK ` (range CA))
    7.90 +	else {Key (priEK (CA i)), Key (priSK (CA i)),
    7.91 +	      Key (pubEK (CA i)), Key (pubSK (CA i)),
    7.92 +	      Key (pubEK RCA), Key (pubSK RCA)})"
    7.93 +
    7.94 +  initState_Cardholder:
    7.95 +    "initState (Cardholder i)  =    
    7.96 +       {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
    7.97 +	Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
    7.98 +	Key (pubEK RCA), Key (pubSK RCA)}"
    7.99 +
   7.100 +  initState_Merchant:
   7.101 +    "initState (Merchant i)  =    
   7.102 +       {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
   7.103 +	Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
   7.104 +	Key (pubEK RCA), Key (pubSK RCA)}"
   7.105 +
   7.106 +  initState_PG:
   7.107 +    "initState (PG i)  = 
   7.108 +       {Key (priEK (PG i)), Key (priSK (PG i)),
   7.109 +	Key (pubEK (PG i)), Key (pubSK (PG i)),
   7.110 +	Key (pubEK RCA), Key (pubSK RCA)}"
   7.111 +
   7.112 +  initState_Spy:
   7.113 +    "initState Spy = Key ` (invKey ` pubEK ` bad Un
   7.114 +			    invKey ` pubSK ` bad Un
   7.115 +			    range pubEK Un range pubSK)"
   7.116 +
   7.117 +
   7.118 +text{*Injective mapping from agents to PANs: an agent can have only one card*}
   7.119 +
   7.120 +consts  pan :: "agent => nat"
   7.121 +
   7.122 +specification (pan)
   7.123 +  inj_pan: "inj pan"
   7.124 +  --{*No two agents have the same PAN*}
   7.125 +   apply (rule exI [of _ "nat_of_agent"]) 
   7.126 +   apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) 
   7.127 +   done
   7.128 +
   7.129 +declare inj_pan [THEN inj_eq, iff]
   7.130 +
   7.131 +consts
   7.132 +  XOR :: "nat*nat => nat"  --{*no properties are assumed of exclusive-or*}
   7.133 +
   7.134 +
   7.135 +subsection{*Signature Primitives*}
   7.136 +
   7.137 +constdefs 
   7.138 +
   7.139 + (* Signature = Message + signed Digest *)
   7.140 +  sign :: "[key, msg]=>msg"
   7.141 +    "sign K X == {|X, Crypt K (Hash X) |}"
   7.142 +
   7.143 + (* Signature Only = signed Digest Only *)
   7.144 +  signOnly :: "[key, msg]=>msg"
   7.145 +    "signOnly K X == Crypt K (Hash X)"
   7.146 +
   7.147 + (* Signature for Certificates = Message + signed Message *)
   7.148 +  signCert :: "[key, msg]=>msg"
   7.149 +    "signCert K X == {|X, Crypt K X |}"
   7.150 +
   7.151 + (* Certification Authority's Certificate.
   7.152 +    Contains agent name, a key, a number specifying the key's target use,
   7.153 +              a key to sign the entire certificate.
   7.154 +
   7.155 +    Should prove if signK=priSK RCA and C=CA i,
   7.156 +                  then Ka=pubEK i or pubSK i depending on T  ??
   7.157 + *)
   7.158 +  cert :: "[agent, key, msg, key] => msg"
   7.159 +    "cert A Ka T signK == signCert signK {|Agent A, Key Ka, T|}"
   7.160 +
   7.161 +
   7.162 + (* Cardholder's Certificate.
   7.163 +    Contains a PAN, the certified key Ka, the PANSecret PS,
   7.164 +    a number specifying the target use for Ka, the signing key signK.
   7.165 + *)
   7.166 +  certC :: "[nat, key, nat, msg, key] => msg"
   7.167 +    "certC PAN Ka PS T signK ==
   7.168 +     signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
   7.169 +
   7.170 +  (*cert and certA have no repeated elements, so they could be translations,
   7.171 +    but that's tricky and makes proofs slower*)
   7.172 +
   7.173 +syntax
   7.174 +  "onlyEnc" :: msg      
   7.175 +  "onlySig" :: msg
   7.176 +  "authCode" :: msg
   7.177 +
   7.178 +translations
   7.179 +  "onlyEnc"   == "Number 0"
   7.180 +  "onlySig"  == "Number (Suc 0)"
   7.181 +  "authCode" == "Number (Suc (Suc 0))"
   7.182 +
   7.183 +subsection{*Encryption Primitives*}
   7.184 +
   7.185 +constdefs
   7.186 +
   7.187 +  EXcrypt :: "[key,key,msg,msg] => msg"
   7.188 +  --{*Extra Encryption*}
   7.189 +    (*K: the symmetric key   EK: the public encryption key*)
   7.190 +    "EXcrypt K EK M m ==
   7.191 +       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
   7.192 +
   7.193 +  EXHcrypt :: "[key,key,msg,msg] => msg"
   7.194 +  --{*Extra Encryption with Hashing*}
   7.195 +    (*K: the symmetric key   EK: the public encryption key*)
   7.196 +    "EXHcrypt K EK M m ==
   7.197 +       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
   7.198 +
   7.199 +  Enc :: "[key,key,key,msg] => msg"
   7.200 +  --{*Simple Encapsulation with SIGNATURE*}
   7.201 +    (*SK: the sender's signing key
   7.202 +      K: the symmetric key
   7.203 +      EK: the public encryption key*)
   7.204 +    "Enc SK K EK M ==
   7.205 +       {|Crypt K (sign SK M), Crypt EK (Key K)|}"
   7.206 +
   7.207 +  EncB :: "[key,key,key,msg,msg] => msg"
   7.208 +  --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
   7.209 +    "EncB SK K EK M b == 
   7.210 +       {|Enc SK K EK {|M, Hash b|}, b|}"
   7.211 +
   7.212 +
   7.213 +subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
   7.214 +
   7.215 +lemma publicKey_eq_iff [iff]:
   7.216 +     "(publicKey b A = publicKey b' A') = (b=b' & A=A')"
   7.217 +by (blast dest: injective_publicKey)
   7.218 +
   7.219 +lemma privateKey_eq_iff [iff]:
   7.220 +     "(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' & A=A')"
   7.221 +by auto
   7.222 +
   7.223 +lemma not_symKeys_publicKey [iff]: "publicKey b A \<notin> symKeys"
   7.224 +by (simp add: symKeys_def)
   7.225 +
   7.226 +lemma not_symKeys_privateKey [iff]: "invKey (publicKey b A) \<notin> symKeys"
   7.227 +by (simp add: symKeys_def)
   7.228 +
   7.229 +lemma symKeys_invKey_eq [simp]: "K \<in> symKeys ==> invKey K = K"
   7.230 +by (simp add: symKeys_def)
   7.231 +
   7.232 +lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
   7.233 +by (unfold symKeys_def, auto)
   7.234 +
   7.235 +text{*Can be slow (or even loop) as a simprule*}
   7.236 +lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
   7.237 +by blast
   7.238 +
   7.239 +text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
   7.240 +in practice.*}
   7.241 +lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
   7.242 +by blast
   7.243 +
   7.244 +lemma symKey_neq_publicKey: "K \<in> symKeys ==> K \<noteq> publicKey b A"
   7.245 +by blast
   7.246 +
   7.247 +lemma privateKey_neq_symKey: "K \<in> symKeys ==> invKey (publicKey b A) \<noteq> K"
   7.248 +by blast
   7.249 +
   7.250 +lemma symKey_neq_privateKey: "K \<in> symKeys ==> K \<noteq> invKey (publicKey b A)"
   7.251 +by blast
   7.252 +
   7.253 +lemma analz_symKeys_Decrypt:
   7.254 +     "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
   7.255 +      ==> X \<in> analz H"
   7.256 +by auto
   7.257 +
   7.258 +
   7.259 +subsection{*"Image" Equations That Hold for Injective Functions *}
   7.260 +
   7.261 +lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
   7.262 +by auto
   7.263 +
   7.264 +text{*holds because invKey is injective*}
   7.265 +lemma publicKey_image_eq [iff]:
   7.266 +     "(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
   7.267 +by auto
   7.268 +
   7.269 +lemma privateKey_image_eq [iff]:
   7.270 +     "(invKey (publicKey b A) \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
   7.271 +by auto
   7.272 +
   7.273 +lemma privateKey_notin_image_publicKey [iff]:
   7.274 +     "invKey (publicKey b A) \<notin> publicKey c ` AS"
   7.275 +by auto
   7.276 +
   7.277 +lemma publicKey_notin_image_privateKey [iff]:
   7.278 +     "publicKey b A \<notin> invKey ` publicKey c ` AS"
   7.279 +by auto
   7.280 +
   7.281 +lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   7.282 +apply (simp add: keysFor_def)
   7.283 +apply (induct_tac "C")
   7.284 +apply (auto intro: range_eqI)
   7.285 +done
   7.286 +
   7.287 +text{*for proving @{text new_keys_not_used}*}
   7.288 +lemma keysFor_parts_insert:
   7.289 +     "[| K \<in> keysFor (parts (insert X H));  X \<in> synth (analz H) |]  
   7.290 +      ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
   7.291 +apply (force dest!: 
   7.292 +         parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   7.293 +         analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] 
   7.294 +            intro: analz_into_parts)
   7.295 +done
   7.296 +
   7.297 +lemma Crypt_imp_keysFor [intro]:
   7.298 +     "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
   7.299 +by (drule Crypt_imp_invKey_keysFor, simp)
   7.300 +
   7.301 +text{*Agents see their own private keys!*}
   7.302 +lemma privateKey_in_initStateCA [iff]:
   7.303 +     "Key (invKey (publicKey b A)) \<in> initState A"
   7.304 +by (case_tac "A", auto)
   7.305 +
   7.306 +text{*Agents see their own public keys!*}
   7.307 +lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
   7.308 +by (case_tac "A", auto)
   7.309 +
   7.310 +text{*RCA sees CAs' public keys! *}
   7.311 +lemma pubK_CA_in_initState_RCA [iff]:
   7.312 +     "Key (publicKey b (CA i)) \<in> initState RCA"
   7.313 +by auto
   7.314 +
   7.315 +
   7.316 +text{*Spy knows all public keys*}
   7.317 +lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
   7.318 +apply (induct_tac "evs")
   7.319 +apply (simp_all add: imageI knows_Cons split add: event.split)
   7.320 +done
   7.321 +
   7.322 +declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
   7.323 +                            (*needed????*)
   7.324 +
   7.325 +text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
   7.326 +lemma knows_Spy_bad_privateKey [intro!]:
   7.327 +     "A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
   7.328 +apply (rule initState_subset_knows [THEN subsetD], simp)
   7.329 +done
   7.330 +
   7.331 +
   7.332 +subsection{*Fresh Nonces for Possibility Theorems*}
   7.333 +
   7.334 +lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
   7.335 +by (induct_tac "B", auto)
   7.336 +
   7.337 +lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
   7.338 +by (simp add: used_Nil)
   7.339 +
   7.340 +text{*In any trace, there is an upper bound N on the greatest nonce in use.*}
   7.341 +lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
   7.342 +apply (induct_tac "evs")
   7.343 +apply (rule_tac x = 0 in exI)
   7.344 +apply (simp_all add: used_Cons split add: event.split, safe)
   7.345 +apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
   7.346 +done
   7.347 +
   7.348 +lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
   7.349 +by (rule Nonce_supply_lemma [THEN exE], blast)
   7.350 +
   7.351 +lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
   7.352 +apply (rule Nonce_supply_lemma [THEN exE])
   7.353 +apply (rule someI, fast)
   7.354 +done
   7.355 +
   7.356 +
   7.357 +subsection{*Fresh Numbers for Possibility Theorems*}
   7.358 +
   7.359 +lemma Number_notin_initState [iff]: "Number N \<notin> parts (initState B)"
   7.360 +by (induct_tac "B", auto)
   7.361 +
   7.362 +lemma Number_notin_used_empty [simp]: "Number N \<notin> used []"
   7.363 +by (simp add: used_Nil)
   7.364 +
   7.365 +text{*In any trace, there is an upper bound N on the greatest number in use.*}
   7.366 +lemma Number_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Number n \<notin> used evs"
   7.367 +apply (induct_tac "evs")
   7.368 +apply (rule_tac x = 0 in exI)
   7.369 +apply (simp_all add: used_Cons split add: event.split, safe)
   7.370 +apply (rule msg_Number_supply [THEN exE], blast elim!: add_leE)+
   7.371 +done
   7.372 +
   7.373 +lemma Number_supply1: "\<exists>N. Number N \<notin> used evs"
   7.374 +by (rule Number_supply_lemma [THEN exE], blast)
   7.375 +
   7.376 +lemma Number_supply: "Number (@ N. Number N \<notin> used evs) \<notin> used evs"
   7.377 +apply (rule Number_supply_lemma [THEN exE])
   7.378 +apply (rule someI, fast)
   7.379 +done
   7.380 +
   7.381 +
   7.382 +subsection{*Fresh Keys for Possibility Theorems*}
   7.383 +
   7.384 +lemma Key_supply1: "\<exists>K. Key K \<notin> used evs & K \<in> symKeys"
   7.385 +by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
   7.386 +
   7.387 +lemma Key_supply:
   7.388 +     "(@K. K \<in> symKeys & Key K \<notin> used evs) \<in> symKeys &  
   7.389 +      Key (@K. K \<in> symKeys & Key K \<notin> used evs) \<notin> used evs"
   7.390 +apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
   7.391 +apply (rule someI, blast)
   7.392 +done
   7.393 +
   7.394 +
   7.395 +subsection{*Specialized Methods for Possibility Theorems*}
   7.396 +
   7.397 +ML
   7.398 +{*
   7.399 +val Nonce_supply1 = thm "Nonce_supply1";
   7.400 +val Nonce_supply = thm "Nonce_supply";
   7.401 +val Key_supply = thm "Key_supply";
   7.402 +val Number_supply = thm "Number_supply";
   7.403 +
   7.404 +val used_Says = thm "used_Says";
   7.405 +val used_Notes = thm "used_Notes";
   7.406 +
   7.407 +(*Tactic for possibility theorems (Isar interface)*)
   7.408 +fun gen_possibility_tac ss state = state |>
   7.409 +    REPEAT (*omit used_Says so that Nonces start from different traces!*)
   7.410 +    (ALLGOALS (simp_tac (ss delsimps [used_Says,used_Notes]))
   7.411 +     THEN
   7.412 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
   7.413 +                   resolve_tac [refl, conjI, Nonce_supply, Number_supply,
   7.414 +                                Key_supply RS conjunct1,
   7.415 +                                Key_supply RS conjunct2]))
   7.416 +
   7.417 +(*Tactic for possibility theorems (ML script version)*)
   7.418 +fun possibility_tac state = gen_possibility_tac (simpset()) state
   7.419 +
   7.420 +(*For harder protocols (such as SET_CR!), where we have to set up some
   7.421 +  nonces and keys initially*)
   7.422 +fun basic_possibility_tac st = st |>
   7.423 +    REPEAT 
   7.424 +    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
   7.425 +     THEN
   7.426 +     REPEAT_FIRST (resolve_tac [refl, conjI]))
   7.427 +*}
   7.428 +
   7.429 +method_setup possibility = {*
   7.430 +    Method.ctxt_args (fn ctxt =>
   7.431 +        Method.METHOD (fn facts =>
   7.432 +            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
   7.433 +    "for proving possibility theorems"
   7.434 +
   7.435 +
   7.436 +
   7.437 +subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
   7.438 +
   7.439 +lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
   7.440 +by blast
   7.441 +
   7.442 +lemma insert_Key_image:
   7.443 +     "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
   7.444 +by blast
   7.445 +
   7.446 +text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
   7.447 +lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
   7.448 +by auto
   7.449 +
   7.450 +lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
   7.451 +by (blast intro!: initState_into_used)
   7.452 +
   7.453 +text{*Reverse the normal simplification of "image" to build up (not break down)
   7.454 +  the set of keys.  Based on @{text analz_image_freshK_ss}, but simpler.*}
   7.455 +lemmas analz_image_keys_simps =
   7.456 +       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
   7.457 +       image_insert [THEN sym] image_Un [THEN sym] 
   7.458 +       rangeI symKeys_neq_imp_neq
   7.459 +       insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
   7.460 +
   7.461 +
   7.462 +(*General lemmas proved by Larry*)
   7.463 +
   7.464 +subsection{*Controlled Unfolding of Abbreviations*}
   7.465 +
   7.466 +text{*A set is expanded only if a relation is applied to it*}
   7.467 +lemma def_abbrev_simp_relation:
   7.468 +     "A == B ==> (A \<in> X) = (B \<in> X) &  
   7.469 +                 (u = A) = (u = B) &  
   7.470 +                 (A = u) = (B = u)"
   7.471 +by auto
   7.472 +
   7.473 +text{*A set is expanded only if one of the given functions is applied to it*}
   7.474 +lemma def_abbrev_simp_function:
   7.475 +     "A == B  
   7.476 +      ==> parts (insert A X) = parts (insert B X) &  
   7.477 +          analz (insert A X) = analz (insert B X) &  
   7.478 +          keysFor (insert A X) = keysFor (insert B X)"
   7.479 +by auto
   7.480 +
   7.481 +subsubsection{*Special Simplification Rules for @{term signCert}*}
   7.482 +
   7.483 +text{*Avoids duplicating X and its components!*}
   7.484 +lemma parts_insert_signCert:
   7.485 +     "parts (insert (signCert K X) H) =  
   7.486 +      insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"
   7.487 +by (simp add: signCert_def insert_commute [of X])
   7.488 +
   7.489 +text{*Avoids a case split! [X is always available]*}
   7.490 +lemma analz_insert_signCert:
   7.491 +     "analz (insert (signCert K X) H) =  
   7.492 +      insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"
   7.493 +by (simp add: signCert_def insert_commute [of X])
   7.494 +
   7.495 +lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
   7.496 +by (simp add: signCert_def)
   7.497 +
   7.498 +text{*Controlled rewrite rules for @{term signCert}, just the definitions
   7.499 +  of the others. Encryption primitives are just expanded, despite their huge
   7.500 +  redundancy!*}
   7.501 +lemmas abbrev_simps [simp] =
   7.502 +    parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
   7.503 +    sign_def	 [THEN def_abbrev_simp_relation]
   7.504 +    sign_def	 [THEN def_abbrev_simp_function]
   7.505 +    signCert_def [THEN def_abbrev_simp_relation]
   7.506 +    signCert_def [THEN def_abbrev_simp_function]
   7.507 +    certC_def	 [THEN def_abbrev_simp_relation]
   7.508 +    certC_def	 [THEN def_abbrev_simp_function]
   7.509 +    cert_def	 [THEN def_abbrev_simp_relation]
   7.510 +    cert_def	 [THEN def_abbrev_simp_function]
   7.511 +    EXcrypt_def	 [THEN def_abbrev_simp_relation]
   7.512 +    EXcrypt_def	 [THEN def_abbrev_simp_function]
   7.513 +    EXHcrypt_def [THEN def_abbrev_simp_relation]
   7.514 +    EXHcrypt_def [THEN def_abbrev_simp_function]
   7.515 +    Enc_def	 [THEN def_abbrev_simp_relation]
   7.516 +    Enc_def	 [THEN def_abbrev_simp_function]
   7.517 +    EncB_def	 [THEN def_abbrev_simp_relation]
   7.518 +    EncB_def	 [THEN def_abbrev_simp_function]
   7.519 +
   7.520 +
   7.521 +subsubsection{*Elimination Rules for Controlled Rewriting *}
   7.522 +
   7.523 +lemma Enc_partsE: 
   7.524 +     "!!R. [|Enc SK K EK M \<in> parts H;  
   7.525 +             [|Crypt K (sign SK M) \<in> parts H;  
   7.526 +               Crypt EK (Key K) \<in> parts H|] ==> R|]  
   7.527 +           ==> R"
   7.528 +
   7.529 +by (unfold Enc_def, blast)
   7.530 +
   7.531 +lemma EncB_partsE: 
   7.532 +     "!!R. [|EncB SK K EK M b \<in> parts H;  
   7.533 +             [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;  
   7.534 +               Crypt EK (Key K) \<in> parts H;  
   7.535 +               b \<in> parts H|] ==> R|]  
   7.536 +           ==> R"
   7.537 +by (unfold EncB_def Enc_def, blast)
   7.538 +
   7.539 +lemma EXcrypt_partsE: 
   7.540 +     "!!R. [|EXcrypt K EK M m \<in> parts H;  
   7.541 +             [|Crypt K {|M, Hash m|} \<in> parts H;  
   7.542 +               Crypt EK {|Key K, m|} \<in> parts H|] ==> R|]  
   7.543 +           ==> R"
   7.544 +by (unfold EXcrypt_def, blast)
   7.545 +
   7.546 +
   7.547 +subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
   7.548 +
   7.549 +lemma analz_knows_absorb:
   7.550 +     "Key K \<in> analz (knows Spy evs)  
   7.551 +      ==> analz (Key ` (insert K H) \<union> knows Spy evs) =  
   7.552 +          analz (Key ` H \<union> knows Spy evs)"
   7.553 +by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
   7.554 +
   7.555 +lemma analz_knows_absorb2:
   7.556 +     "Key K \<in> analz (knows Spy evs)  
   7.557 +      ==> analz (Key ` (insert X (insert K H)) \<union> knows Spy evs) =  
   7.558 +          analz (Key ` (insert X H) \<union> knows Spy evs)"
   7.559 +apply (subst insert_commute)
   7.560 +apply (erule analz_knows_absorb)
   7.561 +done
   7.562 +
   7.563 +lemma analz_insert_subset_eq:
   7.564 +     "[|X \<in> analz (knows Spy evs);  knows Spy evs \<subseteq> H|]  
   7.565 +      ==> analz (insert X H) = analz H"
   7.566 +apply (rule analz_insert_eq)
   7.567 +apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   7.568 +done
   7.569 +
   7.570 +lemmas analz_insert_simps = 
   7.571 +         analz_insert_subset_eq Un_upper2
   7.572 +	 subset_insertI [THEN [2] subset_trans] 
   7.573 +
   7.574 +
   7.575 +subsection{*Freshness Lemmas*}
   7.576 +
   7.577 +lemma in_parts_Says_imp_used:
   7.578 +     "[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
   7.579 +by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
   7.580 +
   7.581 +text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
   7.582 +lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
   7.583 +by auto
   7.584 +
   7.585 +lemma fresh_notin_analz_knows_Spy:
   7.586 +     "Key K \<notin> used evs ==> Key K \<notin> analz (knows Spy evs)"
   7.587 +by (auto dest: analz_into_parts)
   7.588 +
   7.589 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Tue Sep 23 15:40:27 2003 +0200
     8.3 @@ -0,0 +1,1140 @@
     8.4 +(*  Title:      HOL/Auth/SET/Purchase
     8.5 +    ID:         $Id$
     8.6 +    Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     8.7 +*)
     8.8 +
     8.9 +header{*Purchase Phase of SET*}
    8.10 +
    8.11 +theory Purchase = PublicSET:
    8.12 +
    8.13 +text{*
    8.14 +Note: nonces seem to consist of 20 bytes.  That includes both freshness
    8.15 +challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
    8.16 +
    8.17 +This version omits @{text LID_C} but retains @{text LID_M}. At first glance
    8.18 +(Programmer's Guide page 267) it seems that both numbers are just introduced
    8.19 +for the respective convenience of the Cardholder's and Merchant's
    8.20 +system. However, omitting both of them would create a problem of
    8.21 +identification: how can the Merchant's system know what transaction is it
    8.22 +supposed to process?
    8.23 +
    8.24 +Further reading (Programmer's guide page 309) suggest that there is an outside
    8.25 +bootstrapping message (SET initiation message) which is used by the Merchant
    8.26 +and the Cardholder to agree on the actual transaction. This bootstrapping
    8.27 +message is described in the SET External Interface Guide and ought to generate
    8.28 +@{text LID_M}. According SET Extern Interface Guide, this number might be a
    8.29 +cookie, an invoice number etc. The Programmer's Guide on page 310, states that
    8.30 +in absence of @{text LID_M} the protocol must somehow ("outside SET") identify
    8.31 +the transaction from OrderDesc, which is assumed to be a searchable text only
    8.32 +field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed
    8.33 +out-of-bad on the value of @{text LID_M} (for instance a cookie in a web
    8.34 +transaction etc.). This out-of-band agreement is expressed with a preliminary
    8.35 +start action in which the merchant and the Cardholder agree on the appropriate
    8.36 +values. Agreed values are stored with a suitable notes action.
    8.37 +
    8.38 +"XID is a transaction ID that is usually generated by the Merchant system,
    8.39 +unless there is no PInitRes, in which case it is generated by the Cardholder
    8.40 +system. It is a randomly generated 20 byte variable that is globally unique
    8.41 +(statistically). Merchant and Cardholder systems shall use appropriate random
    8.42 +number generators to ensure the global uniqueness of XID."
    8.43 +--Programmer's Guide, page 267.
    8.44 +
    8.45 +PI (Payment Instruction) is the most central and sensitive data structure in
    8.46 +SET. It is used to pass the data required to authorize a payment card payment
    8.47 +from the Cardholder to the Payment Gateway, which will use the data to
    8.48 +initiate a payment card transaction through the traditional payment card
    8.49 +financial network. The data is encrypted by the Cardholder and sent via the
    8.50 +Merchant, such that the data is hidden from the Merchant unless the Acquirer
    8.51 +passes the data back to the Merchant.
    8.52 +--Programmer's Guide, page 271.*}
    8.53 +
    8.54 +consts
    8.55 +
    8.56 +    CardSecret :: "nat => nat"
    8.57 +     (*Maps Cardholders to CardSecrets.
    8.58 +       A CardSecret of 0 means no cerificate, must use unsigned format.*)
    8.59 +
    8.60 +    PANSecret :: "nat => nat"
    8.61 +     (*Maps Cardholders to PANSecrets.*)
    8.62 +
    8.63 +    set_pur  :: "event list set"
    8.64 +
    8.65 +inductive set_pur
    8.66 + intros
    8.67 +
    8.68 +  Nil:   --{*Initial trace is empty*}
    8.69 +	 "[] \<in> set_pur"
    8.70 +
    8.71 +  Fake:  --{*The spy MAY say anything he CAN say.*}
    8.72 +	 "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]
    8.73 +	  ==> Says Spy B X  # evsf \<in> set_pur"
    8.74 +
    8.75 +
    8.76 +  Reception: --{*If A sends a message X to B, then B might receive it*}
    8.77 +	     "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]
    8.78 +	      ==> Gets B X  # evsr \<in> set_pur"
    8.79 +
    8.80 +  Start: 
    8.81 +      --{*Added start event which is out-of-band for SET: the Cardholder and
    8.82 +	  the merchant agree on the amounts and uses @{text LID_M} as an
    8.83 +          identifier.
    8.84 +	  This is suggested by the External Interface Guide. The Programmer's
    8.85 +	  Guide, in absence of @{text LID_M}, states that the merchant uniquely
    8.86 +	  identifies the order out of some data contained in OrderDesc.*}
    8.87 +   "[|evsStart \<in> set_pur;
    8.88 +      Number LID_M \<notin> used evsStart;
    8.89 +      C = Cardholder k; M = Merchant i; P = PG j;
    8.90 +      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    8.91 +      LID_M \<notin> range CardSecret;
    8.92 +      LID_M \<notin> range PANSecret |]
    8.93 +     ==> Notes C {|Number LID_M, Transaction|}
    8.94 +       # Notes M {|Number LID_M, Agent P, Transaction|}
    8.95 +       # evsStart \<in> set_pur"
    8.96 +
    8.97 +  PInitReq:
    8.98 +     --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
    8.99 +   "[|evsPIReq \<in> set_pur;
   8.100 +      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.101 +      Nonce Chall_C \<notin> used evsPIReq;
   8.102 +      Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;
   8.103 +      Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
   8.104 +    ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
   8.105 +
   8.106 +  PInitRes:
   8.107 +     --{*Merchant replies with his own label XID and the encryption
   8.108 +	 key certificate of his chosen Payment Gateway. Page 74 of Formal
   8.109 +         Protocol Desc. We use @{text LID_M} to identify Cardholder*}
   8.110 +   "[|evsPIRes \<in> set_pur;
   8.111 +      Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;
   8.112 +      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.113 +      Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;
   8.114 +      Nonce Chall_M \<notin> used evsPIRes;
   8.115 +      Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;
   8.116 +      Number XID \<notin> used evsPIRes;
   8.117 +      XID \<notin> range CardSecret; XID \<notin> range PANSecret|]
   8.118 +    ==> Says M C (sign (priSK M)
   8.119 +		       {|Number LID_M, Number XID,
   8.120 +			 Nonce Chall_C, Nonce Chall_M,
   8.121 +			 cert P (pubEK P) onlyEnc (priSK RCA)|})
   8.122 +          # evsPIRes \<in> set_pur"
   8.123 +
   8.124 +  PReqUns:
   8.125 +      --{*UNSIGNED Purchase request (CardSecret = 0).
   8.126 +	Page 79 of Formal Protocol Desc.
   8.127 +	Merchant never sees the amount in clear. This holds of the real
   8.128 +	protocol, where XID identifies the transaction. We omit
   8.129 +	Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
   8.130 +	the CardSecret is 0 and because AuthReq treated the unsigned case
   8.131 +	very differently from the signed one anyway.*}
   8.132 +   "[|evsPReqU \<in> set_pur;
   8.133 +      C = Cardholder k; CardSecret k = 0;
   8.134 +      Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
   8.135 +      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.136 +      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   8.137 +      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};
   8.138 +      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
   8.139 +      Gets C (sign (priSK M)
   8.140 +		   {|Number LID_M, Number XID,
   8.141 +		     Nonce Chall_C, Nonce Chall_M,
   8.142 +		     cert P EKj onlyEnc (priSK RCA)|})
   8.143 +	\<in> set evsPReqU;
   8.144 +      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;
   8.145 +      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]
   8.146 +    ==> Says C M
   8.147 +	     {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
   8.148 +	       OIData, Hash{|PIHead, Pan (pan C)|} |}
   8.149 +	  # Notes C {|Key KC1, Agent M|}
   8.150 +	  # evsPReqU \<in> set_pur"
   8.151 +
   8.152 +  PReqS:
   8.153 +      --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
   8.154 +          We could specify the equation
   8.155 +	  @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
   8.156 +	  Formal Desc. gives PIHead the same format in the unsigned case.
   8.157 +	  However, there's little point, as P treats the signed and 
   8.158 +          unsigned cases differently.*}
   8.159 +   "[|evsPReqS \<in> set_pur;
   8.160 +      C = Cardholder k;
   8.161 +      CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
   8.162 +      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.163 +      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   8.164 +      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};
   8.165 +      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
   8.166 +		  Hash{|Number XID, Nonce (CardSecret k)|}|};
   8.167 +      PANData = {|Pan (pan C), Nonce (PANSecret k)|};
   8.168 +      PIData = {|PIHead, PANData|};
   8.169 +      PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},
   8.170 +		       EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};
   8.171 +      OIDualSigned = {|OIData, Hash PIData|};
   8.172 +      Gets C (sign (priSK M)
   8.173 +		   {|Number LID_M, Number XID,
   8.174 +		     Nonce Chall_C, Nonce Chall_M,
   8.175 +		     cert P EKj onlyEnc (priSK RCA)|})
   8.176 +	\<in> set evsPReqS;
   8.177 +      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;
   8.178 +      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]
   8.179 +    ==> Says C M {|PIDualSigned, OIDualSigned|}
   8.180 +	  # Notes C {|Key KC2, Agent M|}
   8.181 +	  # evsPReqS \<in> set_pur"
   8.182 +
   8.183 +  --{*Authorization Request.  Page 92 of Formal Protocol Desc.
   8.184 +    Sent in response to Purchase Request.*}
   8.185 +  AuthReq:
   8.186 +   "[| evsAReq \<in> set_pur;
   8.187 +       Key KM \<notin> used evsAReq;  KM \<in> symKeys;
   8.188 +       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.189 +       HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   8.190 +       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,
   8.191 +		  Nonce Chall_M|};
   8.192 +       CardSecret k \<noteq> 0 -->
   8.193 +	 P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
   8.194 +       Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;
   8.195 +       Says M C (sign (priSK M) {|Number LID_M, Number XID,
   8.196 +				  Nonce Chall_C, Nonce Chall_M,
   8.197 +				  cert P EKj onlyEnc (priSK RCA)|})
   8.198 +	 \<in> set evsAReq;
   8.199 +	Notes M {|Number LID_M, Agent P, Transaction|}
   8.200 +	   \<in> set evsAReq |]
   8.201 +    ==> Says M P
   8.202 +	     (EncB (priSK M) KM (pubEK P)
   8.203 +	       {|Number LID_M, Number XID, Hash OIData, HOD|}	P_I)
   8.204 +	  # evsAReq \<in> set_pur"
   8.205 +
   8.206 +  --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
   8.207 +    Page 99 of Formal Protocol Desc.
   8.208 +    PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and
   8.209 +    HOIData occur independently in @{text P_I} and in M's message.
   8.210 +    The authCode in AuthRes represents the baggage of EncB, which in the
   8.211 +    full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
   8.212 +    optional items for split shipments, recurring payments, etc.*}
   8.213 +
   8.214 +  AuthResUns:
   8.215 +    --{*Authorization Response, UNSIGNED*}
   8.216 +   "[| evsAResU \<in> set_pur;
   8.217 +       C = Cardholder k; M = Merchant i;
   8.218 +       Key KP \<notin> used evsAResU;  KP \<in> symKeys;
   8.219 +       CardSecret k = 0;  KC1 \<in> symKeys;  KM \<in> symKeys;
   8.220 +       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
   8.221 +       P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));
   8.222 +       Gets P (EncB (priSK M) KM (pubEK P)
   8.223 +	       {|Number LID_M, Number XID, HOIData, HOD|} P_I)
   8.224 +	   \<in> set evsAResU |]
   8.225 +   ==> Says P M
   8.226 +	    (EncB (priSK P) KP (pubEK M)
   8.227 +	      {|Number LID_M, Number XID, Number PurchAmt|}
   8.228 +	      authCode)
   8.229 +       # evsAResU \<in> set_pur"
   8.230 +
   8.231 +  AuthResS:
   8.232 +    --{*Authorization Response, SIGNED*}
   8.233 +   "[| evsAResS \<in> set_pur;
   8.234 +       C = Cardholder k;
   8.235 +       Key KP \<notin> used evsAResS;  KP \<in> symKeys;
   8.236 +       CardSecret k \<noteq> 0;  KC2 \<in> symKeys;  KM \<in> symKeys;
   8.237 +       P_I = {|sign (priSK C) {|Hash PIData, HOIData|},
   8.238 +	       EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};
   8.239 +       PANData = {|Pan (pan C), Nonce (PANSecret k)|};
   8.240 +       PIData = {|PIHead, PANData|};
   8.241 +       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
   8.242 +		  Hash{|Number XID, Nonce (CardSecret k)|}|};
   8.243 +       Gets P (EncB (priSK M) KM (pubEK P)
   8.244 +		{|Number LID_M, Number XID, HOIData, HOD|}
   8.245 +	       P_I)
   8.246 +	   \<in> set evsAResS |]
   8.247 +   ==> Says P M
   8.248 +	    (EncB (priSK P) KP (pubEK M)
   8.249 +	      {|Number LID_M, Number XID, Number PurchAmt|}
   8.250 +	      authCode)
   8.251 +       # evsAResS \<in> set_pur"
   8.252 +
   8.253 +  PRes:
   8.254 +    --{*Purchase response.*}
   8.255 +   "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
   8.256 +       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   8.257 +       Gets M (EncB (priSK P) KP (pubEK M)
   8.258 +	      {|Number LID_M, Number XID, Number PurchAmt|}
   8.259 +	      authCode)
   8.260 +	  \<in> set evsPRes;
   8.261 +       Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
   8.262 +       Says M P
   8.263 +	    (EncB (priSK M) KM (pubEK P)
   8.264 +	      {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
   8.265 +	 \<in> set evsPRes;
   8.266 +       Notes M {|Number LID_M, Agent P, Transaction|}
   8.267 +	  \<in> set evsPRes
   8.268 +      |]
   8.269 +   ==> Says M C
   8.270 +	 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
   8.271 +			   Hash (Number PurchAmt)|})
   8.272 +	 # evsPRes \<in> set_pur"
   8.273 +
   8.274 +
   8.275 +specification (CardSecret PANSecret)
   8.276 +  inj_CardSecret:  "inj CardSecret"
   8.277 +  inj_PANSecret:   "inj PANSecret"
   8.278 +  CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
   8.279 +    --{*No CardSecret equals any PANSecret*}
   8.280 +  apply (rule_tac x="curry nat2_to_nat 0" in exI)
   8.281 +  apply (rule_tac x="curry nat2_to_nat 1" in exI)
   8.282 +  apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
   8.283 +  done
   8.284 +
   8.285 +declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   8.286 +declare parts.Body [dest]
   8.287 +declare analz_into_parts [dest]
   8.288 +declare Fake_parts_insert_in_Un [dest]
   8.289 +
   8.290 +declare CardSecret_neq_PANSecret [iff] 
   8.291 +        CardSecret_neq_PANSecret [THEN not_sym, iff]
   8.292 +declare inj_CardSecret [THEN inj_eq, iff] 
   8.293 +        inj_PANSecret [THEN inj_eq, iff]
   8.294 +
   8.295 +
   8.296 +subsection{*Possibility Properties*}
   8.297 +
   8.298 +lemma Says_to_Gets:
   8.299 +     "Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"
   8.300 +by (rule set_pur.Reception, auto)
   8.301 +
   8.302 +(* Possibility for UNSIGNED purchases*)
   8.303 +lemma possibility_Uns:
   8.304 +     "[| CardSecret k = 0;
   8.305 +        \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
   8.306 +        \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
   8.307 +        \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
   8.308 +        \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
   8.309 +     |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
   8.310 +             \<exists>evs \<in> set_pur.
   8.311 +            Says (Merchant i) (Cardholder k)
   8.312 +                 (sign (priSK (Merchant i))
   8.313 +          {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
   8.314 +                  \<in> set evs"
   8.315 +apply (intro exI bexI)
   8.316 +apply (rule_tac [2]
   8.317 +        set_pur.Nil [THEN set_pur.Start, 
   8.318 +                     THEN set_pur.PInitReq, THEN Says_to_Gets, 
   8.319 +                     THEN set_pur.PInitRes, THEN Says_to_Gets,
   8.320 +                     THEN set_pur.PReqUns, THEN Says_to_Gets, 
   8.321 +                     THEN set_pur.AuthReq, THEN Says_to_Gets, 
   8.322 +                     THEN set_pur.AuthResUns, THEN Says_to_Gets, 
   8.323 +                     THEN set_pur.PRes])
   8.324 +apply (possibility, erule spec)+
   8.325 +done
   8.326 +
   8.327 +lemma possibility_S:
   8.328 +     "[| CardSecret k \<noteq> 0;
   8.329 +        \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
   8.330 +        \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
   8.331 +        \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
   8.332 +        \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
   8.333 +     |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
   8.334 +             \<exists>evs \<in> set_pur.
   8.335 +            Says (Merchant i) (Cardholder k)
   8.336 +                 (sign (priSK (Merchant i))
   8.337 +          {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
   8.338 +                  \<in> set evs"
   8.339 +apply (intro exI bexI)
   8.340 +apply (rule_tac [2]
   8.341 +        set_pur.Nil [THEN set_pur.Start, 
   8.342 +                     THEN set_pur.PInitReq, THEN Says_to_Gets, 
   8.343 +                     THEN set_pur.PInitRes, THEN Says_to_Gets,
   8.344 +                     THEN set_pur.PReqS, THEN Says_to_Gets, 
   8.345 +                     THEN set_pur.AuthReq, THEN Says_to_Gets, 
   8.346 +                     THEN set_pur.AuthResS, THEN Says_to_Gets, 
   8.347 +                     THEN set_pur.PRes])
   8.348 +apply possibility    --{*39 seconds on a 1.8GHz machine*}
   8.349 +apply ((erule spec)+, auto)
   8.350 +done
   8.351 +
   8.352 +(*General facts about message reception*)
   8.353 +lemma Gets_imp_Says:
   8.354 +     "[| Gets B X \<in> set evs; evs \<in> set_pur |]
   8.355 +   ==> \<exists>A. Says A B X \<in> set evs"
   8.356 +apply (erule rev_mp)
   8.357 +apply (erule set_pur.induct, auto)
   8.358 +done
   8.359 +
   8.360 +lemma Gets_imp_knows_Spy:
   8.361 +     "[| Gets B X \<in> set evs; evs \<in> set_pur |]  ==> X \<in> knows Spy evs"
   8.362 +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   8.363 +
   8.364 +declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   8.365 +
   8.366 +text{*Forwarding lemmas, to aid simplification*}
   8.367 +
   8.368 +lemma AuthReq_msg_in_parts_spies:
   8.369 +     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
   8.370 +        evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"
   8.371 +by auto
   8.372 +
   8.373 +lemma AuthReq_msg_in_analz_spies:
   8.374 +     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
   8.375 +        evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
   8.376 +by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
   8.377 +
   8.378 +
   8.379 +subsection{*Proofs on Asymmetric Keys*}
   8.380 +
   8.381 +text{*Private Keys are Secret*}
   8.382 +
   8.383 +text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   8.384 +lemma Spy_see_private_Key [simp]:
   8.385 +     "evs \<in> set_pur
   8.386 +      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   8.387 +apply (erule set_pur.induct)
   8.388 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.389 +apply auto
   8.390 +done
   8.391 +declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   8.392 +
   8.393 +lemma Spy_analz_private_Key [simp]:
   8.394 +     "evs \<in> set_pur ==>
   8.395 +     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   8.396 +by auto
   8.397 +declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   8.398 +
   8.399 +text{*rewriting rule for priEK's*}
   8.400 +lemma parts_image_priEK:
   8.401 +     "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
   8.402 +        evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"
   8.403 +by auto
   8.404 +
   8.405 +text{*trivial proof because (priEK C) never appears even in (parts evs)*}
   8.406 +lemma analz_image_priEK:
   8.407 +     "evs \<in> set_pur ==>
   8.408 +          (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
   8.409 +          (priEK C \<in> KK | C \<in> bad)"
   8.410 +by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   8.411 +
   8.412 +subsection{*Public Keys in Certificates are Correct*}
   8.413 +
   8.414 +lemma Crypt_valid_pubEK [dest!]:
   8.415 +     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
   8.416 +           \<in> parts (knows Spy evs);
   8.417 +         evs \<in> set_pur |] ==> EKi = pubEK C"
   8.418 +apply (erule rev_mp)
   8.419 +apply (erule set_pur.induct, auto)
   8.420 +done
   8.421 +
   8.422 +lemma Crypt_valid_pubSK [dest!]:
   8.423 +     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
   8.424 +           \<in> parts (knows Spy evs);
   8.425 +         evs \<in> set_pur |] ==> SKi = pubSK C"
   8.426 +apply (erule rev_mp)
   8.427 +apply (erule set_pur.induct, auto)
   8.428 +done
   8.429 +
   8.430 +lemma certificate_valid_pubEK:
   8.431 +    "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   8.432 +        evs \<in> set_pur |]
   8.433 +     ==> EKi = pubEK C"
   8.434 +by (unfold cert_def signCert_def, auto)
   8.435 +
   8.436 +lemma certificate_valid_pubSK:
   8.437 +    "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   8.438 +        evs \<in> set_pur |] ==> SKi = pubSK C"
   8.439 +by (unfold cert_def signCert_def, auto)
   8.440 +
   8.441 +lemma Says_certificate_valid [simp]:
   8.442 +     "[| Says A B (sign SK {|lid, xid, cc, cm,
   8.443 +                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
   8.444 +         evs \<in> set_pur |]
   8.445 +      ==> EK = pubEK C"
   8.446 +by (unfold sign_def, auto)
   8.447 +
   8.448 +lemma Gets_certificate_valid [simp]:
   8.449 +     "[| Gets A (sign SK {|lid, xid, cc, cm,
   8.450 +                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
   8.451 +         evs \<in> set_pur |]
   8.452 +      ==> EK = pubEK C"
   8.453 +by (frule Gets_imp_Says, auto)
   8.454 +
   8.455 +ML
   8.456 +{*
   8.457 +val Gets_certificate_valid = thm "Gets_certificate_valid";
   8.458 +
   8.459 +fun valid_certificate_tac i =
   8.460 +    EVERY [ftac Gets_certificate_valid i,
   8.461 +           assume_tac i, REPEAT (hyp_subst_tac i)];
   8.462 +*}
   8.463 +
   8.464 +
   8.465 +subsection{*Proofs on Symmetric Keys*}
   8.466 +
   8.467 +text{*Nobody can have used non-existent keys!*}
   8.468 +lemma new_keys_not_used [rule_format,simp]:
   8.469 +     "evs \<in> set_pur
   8.470 +      ==> Key K \<notin> used evs --> K \<in> symKeys -->
   8.471 +          K \<notin> keysFor (parts (knows Spy evs))"
   8.472 +apply (erule set_pur.induct)
   8.473 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.474 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.475 +apply auto
   8.476 +apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
   8.477 +done
   8.478 +
   8.479 +lemma new_keys_not_analzd:
   8.480 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   8.481 +      ==> K \<notin> keysFor (analz (knows Spy evs))"
   8.482 +by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used)
   8.483 +
   8.484 +lemma Crypt_parts_imp_used:
   8.485 +     "[|Crypt K X \<in> parts (knows Spy evs);
   8.486 +        K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
   8.487 +apply (rule ccontr)
   8.488 +apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   8.489 +done
   8.490 +
   8.491 +lemma Crypt_analz_imp_used:
   8.492 +     "[|Crypt K X \<in> analz (knows Spy evs);
   8.493 +        K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
   8.494 +by (blast intro: Crypt_parts_imp_used)
   8.495 +
   8.496 +text{*New versions: as above, but generalized to have the KK argument*}
   8.497 +
   8.498 +lemma gen_new_keys_not_used:
   8.499 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   8.500 +      ==> Key K \<notin> used evs --> K \<in> symKeys -->
   8.501 +          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   8.502 +by auto
   8.503 +
   8.504 +lemma gen_new_keys_not_analzd:
   8.505 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   8.506 +      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   8.507 +by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used)
   8.508 +
   8.509 +lemma analz_Key_image_insert_eq:
   8.510 +     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   8.511 +      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   8.512 +          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   8.513 +by (simp add: gen_new_keys_not_analzd)
   8.514 +
   8.515 +
   8.516 +subsection{*Secrecy of Symmetric Keys*}
   8.517 +
   8.518 +lemma Key_analz_image_Key_lemma:
   8.519 +     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
   8.520 +      ==>
   8.521 +      P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
   8.522 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   8.523 +
   8.524 +
   8.525 +lemma symKey_compromise:
   8.526 +     "evs \<in> set_pur ==>
   8.527 +      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow>
   8.528 +        (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
   8.529 +               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
   8.530 +               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
   8.531 +apply (erule set_pur.induct)
   8.532 +apply (rule_tac [!] allI)+
   8.533 +apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
   8.534 +apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   8.535 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.536 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.537 +apply (simp_all
   8.538 +         del: image_insert image_Un imp_disjL
   8.539 +         add: analz_image_keys_simps disj_simps
   8.540 +              analz_Key_image_insert_eq notin_image_iff
   8.541 +              analz_insert_simps analz_image_priEK)
   8.542 +  --{*35 seconds on a 1.8GHz machine*}
   8.543 +apply spy_analz --{*Fake*}
   8.544 +apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}
   8.545 +done
   8.546 +
   8.547 +
   8.548 +
   8.549 +subsection{*Secrecy of Nonces*}
   8.550 +
   8.551 +text{*As usual: we express the property as a logical equivalence*}
   8.552 +lemma Nonce_analz_image_Key_lemma:
   8.553 +     "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
   8.554 +      ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
   8.555 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   8.556 +
   8.557 +text{*The @{text "(no_asm)"} attribute is essential, since it retains
   8.558 +  the quantifier and allows the simprule's condition to itself be simplified.*}
   8.559 +lemma Nonce_compromise [rule_format (no_asm)]:
   8.560 +     "evs \<in> set_pur ==>
   8.561 +      (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C))   -->
   8.562 +              (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
   8.563 +              (Nonce N \<in> analz (knows Spy evs)))"
   8.564 +apply (erule set_pur.induct)
   8.565 +apply (rule_tac [!] allI)+
   8.566 +apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
   8.567 +apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   8.568 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.569 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.570 +apply (simp_all
   8.571 +         del: image_insert image_Un imp_disjL
   8.572 +         add: analz_image_keys_simps disj_simps symKey_compromise
   8.573 +              analz_Key_image_insert_eq notin_image_iff
   8.574 +              analz_insert_simps analz_image_priEK)
   8.575 +  --{*35 seconds on a 1.8GHz machine*}
   8.576 +apply spy_analz --{*Fake*}
   8.577 +apply (blast elim!: ballE) --{*PReqS*}
   8.578 +done
   8.579 +
   8.580 +lemma PANSecret_notin_spies:
   8.581 +     "evs \<in> set_pur
   8.582 +   ==> Nonce (PANSecret k) \<in> analz (knows Spy evs) -->
   8.583 +       (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
   8.584 +          Says (Cardholder k) M
   8.585 +               {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
   8.586 +                 V|}  \<in>  set evs)"
   8.587 +apply (erule set_pur.induct)
   8.588 +apply (frule_tac [9] AuthReq_msg_in_analz_spies)
   8.589 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.590 +apply (simp_all
   8.591 +         del: image_insert image_Un imp_disjL
   8.592 +         add: analz_image_keys_simps disj_simps
   8.593 +              symKey_compromise pushes sign_def Nonce_compromise
   8.594 +              analz_Key_image_insert_eq notin_image_iff
   8.595 +              analz_insert_simps analz_image_priEK)
   8.596 +  --{*13 seconds on a 1.8GHz machine*}
   8.597 +apply spy_analz
   8.598 +apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   8.599 +apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
   8.600 +                   Gets_imp_knows_Spy [THEN analz.Inj])
   8.601 +apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*}
   8.602 +apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
   8.603 +                   Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*}
   8.604 +done
   8.605 +
   8.606 +text{*This theorem is a bit silly, in that many CardSecrets are 0!
   8.607 +  But then we don't care.  NOT USED*}
   8.608 +lemma CardSecret_notin_spies:
   8.609 +     "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"
   8.610 +by (erule set_pur.induct, auto)
   8.611 +
   8.612 +subsection{*Confidentiality of PAN*}
   8.613 +
   8.614 +lemma analz_image_pan_lemma:
   8.615 +     "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
   8.616 +      (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
   8.617 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   8.618 +
   8.619 +text{*The @{text "(no_asm)"} attribute is essential, since it retains
   8.620 +  the quantifier and allows the simprule's condition to itself be simplified.*}
   8.621 +lemma analz_image_pan [rule_format (no_asm)]:
   8.622 +     "evs \<in> set_pur ==>
   8.623 +       \<forall>KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
   8.624 +            (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
   8.625 +            (Pan P \<in> analz (knows Spy evs))"
   8.626 +apply (erule set_pur.induct)
   8.627 +apply (rule_tac [!] allI impI)+
   8.628 +apply (rule_tac [!] analz_image_pan_lemma)+
   8.629 +apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   8.630 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.631 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.632 +apply (simp_all
   8.633 +         del: image_insert image_Un imp_disjL
   8.634 +         add: analz_image_keys_simps
   8.635 +              symKey_compromise pushes sign_def
   8.636 +              analz_Key_image_insert_eq notin_image_iff
   8.637 +              analz_insert_simps analz_image_priEK)
   8.638 +  --{*32 seconds on a 1.8GHz machine*}
   8.639 +apply spy_analz --{*Fake*}
   8.640 +apply auto
   8.641 +done
   8.642 +
   8.643 +lemma analz_insert_pan:
   8.644 +     "[| evs \<in> set_pur;  K \<notin> range(\<lambda>C. priEK C) |] ==>
   8.645 +          (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
   8.646 +          (Pan P \<in> analz (knows Spy evs))"
   8.647 +by (simp del: image_insert image_Un
   8.648 +         add: analz_image_keys_simps analz_image_pan)
   8.649 +
   8.650 +text{*Confidentiality of the PAN, unsigned case.*}
   8.651 +lemma pan_confidentiality_unsigned:
   8.652 +     "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
   8.653 +         CardSecret k = 0;  evs \<in> set_pur|]
   8.654 +    ==> \<exists>P M KC1 K X Y.
   8.655 +     Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
   8.656 +          \<in> set evs  &
   8.657 +     P \<in> bad"
   8.658 +apply (erule rev_mp)
   8.659 +apply (erule set_pur.induct)
   8.660 +apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   8.661 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.662 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.663 +apply (simp_all
   8.664 +         del: image_insert image_Un imp_disjL
   8.665 +         add: analz_image_keys_simps analz_insert_pan analz_image_pan
   8.666 +              notin_image_iff
   8.667 +              analz_insert_simps analz_image_priEK)
   8.668 +  --{*15 seconds on a 1.8GHz machine*}
   8.669 +apply spy_analz --{*Fake*}
   8.670 +apply blast --{*PReqUns: unsigned*}
   8.671 +apply force --{*PReqS: signed*}
   8.672 +done
   8.673 +
   8.674 +text{*Confidentiality of the PAN, signed case.*}
   8.675 +lemma pan_confidentiality_signed:
   8.676 +     "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
   8.677 +         CardSecret k \<noteq> 0;  evs \<in> set_pur|]
   8.678 +    ==> \<exists>B M KC2 K ps X Y Z.
   8.679 +     Says C M {|{|X, EXcrypt KC2 (pubEK B) Y {|Pan (pan C), ps|}|}, Z|}
   8.680 +          \<in> set evs  &
   8.681 +     B \<in> bad"
   8.682 +apply (erule rev_mp)
   8.683 +apply (erule set_pur.induct)
   8.684 +apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   8.685 +apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
   8.686 +apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
   8.687 +apply (simp_all
   8.688 +         del: image_insert image_Un imp_disjL
   8.689 +         add: analz_image_keys_simps analz_insert_pan analz_image_pan
   8.690 +              notin_image_iff
   8.691 +              analz_insert_simps analz_image_priEK)
   8.692 +  --{*17 seconds on a 1.8GHz machine*}
   8.693 +apply spy_analz --{*Fake*}
   8.694 +apply force --{*PReqUns: unsigned*}
   8.695 +apply blast --{*PReqS: signed*}
   8.696 +done
   8.697 +
   8.698 +text{*General goal: that C, M and PG agree on those details of the transaction
   8.699 +     that they are allowed to know about.  PG knows about price and account
   8.700 +     details.  M knows about the order description and price.  C knows both.*}
   8.701 +
   8.702 +
   8.703 +subsection{*Proofs Common to Signed and Unsigned Versions*}
   8.704 +
   8.705 +lemma M_Notes_PG:
   8.706 +     "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;
   8.707 +        evs \<in> set_pur|] ==> \<exists>j. P = PG j"
   8.708 +apply (erule rev_mp)
   8.709 +apply (erule set_pur.induct, simp_all)
   8.710 +done
   8.711 +
   8.712 +text{*If we trust M, then @{term LID_M} determines his choice of P
   8.713 +      (Payment Gateway)*}
   8.714 +lemma goodM_gives_correct_PG:
   8.715 +     "[| MsgPInitRes = 
   8.716 +            {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
   8.717 +         Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
   8.718 +         evs \<in> set_pur; M \<notin> bad |]
   8.719 +      ==> \<exists>j trans.
   8.720 +            P = PG j &
   8.721 +            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"
   8.722 +apply clarify
   8.723 +apply (erule rev_mp)
   8.724 +apply (erule set_pur.induct)
   8.725 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.726 +apply simp_all
   8.727 +apply (blast intro: M_Notes_PG)+
   8.728 +done
   8.729 +
   8.730 +lemma C_gets_correct_PG:
   8.731 +     "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,
   8.732 +                              cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;
   8.733 +         evs \<in> set_pur;  M \<notin> bad|]
   8.734 +      ==> \<exists>j trans.
   8.735 +            P = PG j &
   8.736 +            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   8.737 +            EKj = pubEK P"
   8.738 +by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)
   8.739 +
   8.740 +text{*When C receives PInitRes, he learns M's choice of P*}
   8.741 +lemma C_verifies_PInitRes:
   8.742 + "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
   8.743 +	   cert P EKj onlyEnc (priSK RCA)|};
   8.744 +     Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
   8.745 +     evs \<in> set_pur;  M \<notin> bad|]
   8.746 +  ==> \<exists>j trans.
   8.747 +         Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   8.748 +         P = PG j &
   8.749 +         EKj = pubEK P"
   8.750 +apply clarify
   8.751 +apply (erule rev_mp)
   8.752 +apply (erule set_pur.induct)
   8.753 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.754 +apply simp_all
   8.755 +apply (blast intro: M_Notes_PG)+
   8.756 +done
   8.757 +
   8.758 +text{*Corollary of previous one*}
   8.759 +lemma Says_C_PInitRes:
   8.760 +     "[|Says A C (sign (priSK M)
   8.761 +                      {|Number LID_M, Number XID,
   8.762 +                        Nonce Chall_C, Nonce Chall_M,
   8.763 +                        cert P EKj onlyEnc (priSK RCA)|})
   8.764 +           \<in> set evs;  M \<notin> bad;  evs \<in> set_pur|]
   8.765 +      ==> \<exists>j trans.
   8.766 +           Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   8.767 +           P = PG j &
   8.768 +           EKj = pubEK (PG j)"
   8.769 +apply (frule Says_certificate_valid)
   8.770 +apply (auto simp add: sign_def)
   8.771 +apply (blast dest: refl [THEN goodM_gives_correct_PG])
   8.772 +apply (blast dest: refl [THEN C_verifies_PInitRes])
   8.773 +done
   8.774 +
   8.775 +text{*When P receives an AuthReq, he knows that the signed part originated 
   8.776 +      with M. PIRes also has a signed message from M....*}
   8.777 +lemma P_verifies_AuthReq:
   8.778 +     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
   8.779 +         Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})
   8.780 +           \<in> parts (knows Spy evs);
   8.781 +         evs \<in> set_pur;  M \<notin> bad|]
   8.782 +      ==> \<exists>j trans KM OIData HPIData.
   8.783 +            Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
   8.784 +            Gets M {|P_I, OIData, HPIData|} \<in> set evs &
   8.785 +            Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
   8.786 +              \<in> set evs"
   8.787 +apply clarify
   8.788 +apply (erule rev_mp)
   8.789 +apply (erule set_pur.induct, simp_all)
   8.790 +apply (frule_tac [4] M_Notes_PG, auto)
   8.791 +done
   8.792 +
   8.793 +text{*When M receives AuthRes, he knows that P signed it, including
   8.794 +  the identifying tages and the purchase amount, which he can verify.
   8.795 +  (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
   8.796 +   send the same message to M.)*}
   8.797 +lemma M_verifies_AuthRes:
   8.798 +  "[| MsgAuthRes = {|Number LID_M, Number XID, Number PurchAmt|};
   8.799 +      Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
   8.800 +      evs \<in> set_pur;  PG j \<notin> bad|]
   8.801 +   ==> \<exists>i KM HOIData HOD P_I.
   8.802 +	Gets (PG j)
   8.803 +	   (EncB (priSK (Merchant i)) KM (pubEK (PG j))
   8.804 +		    {|Number LID_M, Number XID, HOIData, HOD|}
   8.805 +		    P_I) \<in> set evs &
   8.806 +	Says (PG j) (Merchant i)
   8.807 +	     (Crypt (pubEK (Merchant i)) (sign (priSK (PG j)) MsgAuthRes))
   8.808 +          \<in> set evs"
   8.809 +apply clarify
   8.810 +apply (erule rev_mp)
   8.811 +apply (erule set_pur.induct)
   8.812 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.813 +apply simp_all
   8.814 +apply blast+
   8.815 +done
   8.816 +
   8.817 +
   8.818 +subsection{*Proofs for Unsigned Purchases*}
   8.819 +
   8.820 +text{*What we can derive from the ASSUMPTION that C issued a purchase request.
   8.821 +   In the unsigned case, we must trust "C": there's no authentication.*}
   8.822 +lemma C_determines_EKj:
   8.823 +     "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
   8.824 +                    OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;
   8.825 +         PIHead = {|Number LID_M, Trans_details|};
   8.826 +         evs \<in> set_pur;  C = Cardholder k;  M \<notin> bad|]
   8.827 +  ==> \<exists>trans j.
   8.828 +               Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
   8.829 +               EKj = pubEK (PG j)"
   8.830 +apply clarify
   8.831 +apply (erule rev_mp)
   8.832 +apply (erule set_pur.induct, simp_all)
   8.833 +apply (tactic{*valid_certificate_tac 2*}) --{*PReqUns*}
   8.834 +apply auto
   8.835 +apply (blast dest: Gets_imp_Says Says_C_PInitRes)
   8.836 +done
   8.837 +
   8.838 +
   8.839 +text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}
   8.840 +lemma unique_LID_M:
   8.841 +     "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;
   8.842 +        Notes C {|Number LID_M, Agent M, Agent C, Number OD,
   8.843 +             Number PA|} \<in> set evs;
   8.844 +        evs \<in> set_pur|]
   8.845 +      ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
   8.846 +apply (erule rev_mp)
   8.847 +apply (erule rev_mp)
   8.848 +apply (erule set_pur.induct, simp_all)
   8.849 +apply (force dest!: Notes_imp_parts_subset_used)
   8.850 +done
   8.851 +
   8.852 +text{*Unicity of @{term LID_M}, for two Merchant Notes events*}
   8.853 +lemma unique_LID_M2:
   8.854 +     "[|Notes M {|Number LID_M, Trans|} \<in> set evs;
   8.855 +        Notes M {|Number LID_M, Trans'|} \<in> set evs;
   8.856 +        evs \<in> set_pur|] ==> Trans' = Trans"
   8.857 +apply (erule rev_mp)
   8.858 +apply (erule rev_mp)
   8.859 +apply (erule set_pur.induct, simp_all)
   8.860 +apply (force dest!: Notes_imp_parts_subset_used)
   8.861 +done
   8.862 +
   8.863 +text{*Lemma needed below: for the case that
   8.864 +  if PRes is present, then @{term LID_M} has been used.*}
   8.865 +lemma signed_imp_used:
   8.866 +     "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);
   8.867 +         M \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
   8.868 +apply (erule rev_mp)
   8.869 +apply (erule set_pur.induct)
   8.870 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.871 +apply simp_all
   8.872 +apply safe
   8.873 +apply blast+
   8.874 +done
   8.875 +
   8.876 +text{*Similar, with nested Hash*}
   8.877 +lemma signed_Hash_imp_used:
   8.878 +     "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
   8.879 +         C \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
   8.880 +apply (erule rev_mp)
   8.881 +apply (erule set_pur.induct)
   8.882 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.883 +apply simp_all
   8.884 +apply safe
   8.885 +apply blast+
   8.886 +done
   8.887 +
   8.888 +text{*Lemma needed below: for the case that
   8.889 +  if PRes is present, then @{text LID_M} has been used.*}
   8.890 +lemma PRes_imp_LID_used:
   8.891 +     "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);
   8.892 +         M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"
   8.893 +by (drule signed_imp_used, auto)
   8.894 +
   8.895 +text{*When C receives PRes, he knows that M and P agreed to the purchase details.
   8.896 +  He also knows that P is the same PG as before*}
   8.897 +lemma C_verifies_PRes_lemma:
   8.898 +     "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);
   8.899 +         Notes C {|Number LID_M, Trans |} \<in> set evs;
   8.900 +         Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
   8.901 +         MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
   8.902 +                Hash (Number PurchAmt)|};
   8.903 +         evs \<in> set_pur;  M \<notin> bad|]
   8.904 +  ==> \<exists>j KP.
   8.905 +        Notes M {|Number LID_M, Agent (PG j), Trans |}
   8.906 +          \<in> set evs &
   8.907 +        Gets M (EncB (priSK (PG j)) KP (pubEK M)
   8.908 +                {|Number LID_M, Number XID, Number PurchAmt|}
   8.909 +                authCode)
   8.910 +          \<in> set evs &
   8.911 +        Says M C (sign (priSK M) MsgPRes) \<in> set evs"
   8.912 +apply clarify
   8.913 +apply (erule rev_mp)
   8.914 +apply (erule rev_mp)
   8.915 +apply (erule set_pur.induct)
   8.916 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.917 +apply simp_all
   8.918 +apply blast
   8.919 +apply blast
   8.920 +apply (blast dest: PRes_imp_LID_used)
   8.921 +apply (frule M_Notes_PG, auto)
   8.922 +apply (blast dest: unique_LID_M)
   8.923 +done
   8.924 +
   8.925 +lemma C_verifies_PRes:
   8.926 +     "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
   8.927 +                     Hash (Number PurchAmt)|};
   8.928 +         Gets C (sign (priSK M) MsgPRes) \<in> set evs;
   8.929 +         Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
   8.930 +                   Number PurchAmt|} \<in> set evs;
   8.931 +         evs \<in> set_pur;  M \<notin> bad|]
   8.932 +  ==> \<exists>P KP trans.
   8.933 +        Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
   8.934 +        Gets M (EncB (priSK P) KP (pubEK M)
   8.935 +                {|Number LID_M, Number XID, Number PurchAmt|}
   8.936 +                authCode)
   8.937 +          \<in> set evs &
   8.938 +        Says M C (sign (priSK M) MsgPRes) \<in> set evs"
   8.939 +apply (rule C_verifies_PRes_lemma [THEN exE])
   8.940 +apply (auto simp add: sign_def)
   8.941 +done
   8.942 +
   8.943 +subsection{*Proofs for Signed Purchases*}
   8.944 +
   8.945 +text{*Some Useful Lemmas: the cardholder knows what he is doing*}
   8.946 +
   8.947 +lemma Crypt_imp_Says_Cardholder:
   8.948 +     "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
   8.949 +           \<in> parts (knows Spy evs);
   8.950 +         PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
   8.951 +         Key K \<notin> analz (knows Spy evs);
   8.952 +         evs \<in> set_pur|]
   8.953 +  ==> \<exists>M shash EK HPIData.
   8.954 +       Says (Cardholder k) M {|{|shash,
   8.955 +          Crypt K
   8.956 +            {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
   8.957 +           Crypt EK {|Key K, PANData|}|},
   8.958 +          OIData, HPIData|} \<in> set evs"
   8.959 +apply (erule rev_mp)
   8.960 +apply (erule rev_mp)
   8.961 +apply (erule rev_mp)
   8.962 +apply (erule set_pur.induct, analz_mono_contra)
   8.963 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   8.964 +apply simp_all
   8.965 +apply auto
   8.966 +done
   8.967 +
   8.968 +lemma Says_PReqS_imp_trans_details_C:
   8.969 +     "[| MsgPReqS = {|{|shash,
   8.970 +                 Crypt K
   8.971 +                  {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
   8.972 +            cryptek|}, data|};
   8.973 +         Says (Cardholder k) M MsgPReqS \<in> set evs;
   8.974 +         evs \<in> set_pur |]
   8.975 +   ==> \<exists>trans.
   8.976 +           Notes (Cardholder k) 
   8.977 +                 {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
   8.978 +            \<in> set evs"
   8.979 +apply (erule rev_mp)
   8.980 +apply (erule rev_mp)
   8.981 +apply (erule set_pur.induct)
   8.982 +apply (simp_all (no_asm_simp))
   8.983 +apply auto
   8.984 +done
   8.985 +
   8.986 +text{*Can't happen: only Merchants create this type of Note*}
   8.987 +lemma Notes_Cardholder_self_False:
   8.988 +     "[|Notes (Cardholder k)
   8.989 +          {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;
   8.990 +        evs \<in> set_pur|] ==> False"
   8.991 +apply (erule rev_mp)
   8.992 +apply (erule set_pur.induct, auto)
   8.993 +done
   8.994 +
   8.995 +text{*When M sees a dual signature, he knows that it originated with C.
   8.996 +  Using XID he knows it was intended for him.
   8.997 +  This guarantee isn't useful to P, who never gets OIData.*}
   8.998 +lemma M_verifies_Signed_PReq:
   8.999 +     "[| MsgDualSign = {|HPIData, Hash OIData|};
  8.1000 +         OIData = {|Number LID_M, etc|};
  8.1001 +         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  8.1002 +         Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
  8.1003 +         M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
  8.1004 +      ==> \<exists>PIData PICrypt.
  8.1005 +            HPIData = Hash PIData &
  8.1006 +            Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
  8.1007 +              \<in> set evs"
  8.1008 +apply clarify
  8.1009 +apply (erule rev_mp)
  8.1010 +apply (erule rev_mp)
  8.1011 +apply (erule set_pur.induct)
  8.1012 +apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
  8.1013 +apply simp_all
  8.1014 +apply blast
  8.1015 +apply (force dest!: signed_Hash_imp_used)
  8.1016 +apply (clarify) --{*speeds next step*}
  8.1017 +apply (blast dest: unique_LID_M)
  8.1018 +apply (blast dest!: Notes_Cardholder_self_False)
  8.1019 +done
  8.1020 +
  8.1021 +text{*When P sees a dual signature, he knows that it originated with C.
  8.1022 +  and was intended for M. This guarantee isn't useful to M, who never gets
  8.1023 +  PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
  8.1024 +  assuming @{term "M \<notin> bad"}.*}
  8.1025 +lemma P_verifies_Signed_PReq:
  8.1026 +     "[| MsgDualSign = {|Hash PIData, HOIData|};
  8.1027 +         PIData = {|PIHead, PANData|};
  8.1028 +         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  8.1029 +                    TransStain|};
  8.1030 +         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  8.1031 +         evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
  8.1032 +    ==> \<exists>OIData OrderDesc K j trans.
  8.1033 +          HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
  8.1034 +          HOIData = Hash OIData &
  8.1035 +          Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
  8.1036 +          Says C M {|{|sign (priSK C) MsgDualSign,
  8.1037 +                     EXcrypt K (pubEK (PG j))
  8.1038 +                                {|PIHead, Hash OIData|} PANData|},
  8.1039 +                     OIData, Hash PIData|}
  8.1040 +            \<in> set evs"
  8.1041 +apply clarify
  8.1042 +apply (erule rev_mp)
  8.1043 +apply (erule set_pur.induct, simp_all)
  8.1044 +apply (auto dest!: C_gets_correct_PG)
  8.1045 +done
  8.1046 +
  8.1047 +lemma C_determines_EKj_signed:
  8.1048 +     "[| Says C M {|{|sign (priSK C) text,
  8.1049 +                      EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;
  8.1050 +         PIHead = {|Number LID_M, Number XID, W|};
  8.1051 +         C = Cardholder k;  evs \<in> set_pur;  M \<notin> bad|]
  8.1052 +  ==> \<exists> trans j.
  8.1053 +         Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
  8.1054 +         EKj = pubEK (PG j)"
  8.1055 +apply clarify
  8.1056 +apply (erule rev_mp)
  8.1057 +apply (erule set_pur.induct, simp_all, auto)
  8.1058 +apply (blast dest: C_gets_correct_PG)
  8.1059 +done
  8.1060 +
  8.1061 +lemma M_Says_AuthReq:
  8.1062 +     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
  8.1063 +         sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);
  8.1064 +         evs \<in> set_pur;  M \<notin> bad|]
  8.1065 +   ==> \<exists>j trans KM.
  8.1066 +           Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
  8.1067 +             Says M (PG j)
  8.1068 +               (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
  8.1069 +              \<in> set evs"
  8.1070 +apply (rule refl [THEN P_verifies_AuthReq, THEN exE])
  8.1071 +apply (auto simp add: sign_def)
  8.1072 +done
  8.1073 +
  8.1074 +text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information.
  8.1075 +  Even here we cannot be certain about what C sent to M, since a bad
  8.1076 +  PG could have replaced the two key fields.  (NOT USED)*}
  8.1077 +lemma Signed_PReq_imp_Says_Cardholder:
  8.1078 +     "[| MsgDualSign = {|Hash PIData, Hash OIData|};
  8.1079 +         OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};
  8.1080 +         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  8.1081 +                    TransStain|};
  8.1082 +         PIData = {|PIHead, PANData|};
  8.1083 +         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  8.1084 +         M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
  8.1085 +      ==> \<exists>KC EKj.
  8.1086 +            Says C M {|{|sign (priSK C) MsgDualSign,
  8.1087 +                       EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
  8.1088 +                       OIData, Hash PIData|}
  8.1089 +              \<in> set evs"
  8.1090 +apply clarify
  8.1091 +apply (erule rev_mp)
  8.1092 +apply (erule rev_mp)
  8.1093 +apply (erule set_pur.induct, simp_all, auto)
  8.1094 +done
  8.1095 +
  8.1096 +text{*When P receives an AuthReq and a dual signature, he knows that C and M
  8.1097 +  agree on the essential details.  PurchAmt however is never sent by M to
  8.1098 +  P; instead C and M both send 
  8.1099 +     @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}
  8.1100 +  and P compares the two copies of HOD.
  8.1101 +
  8.1102 +  Agreement can't be proved for some things, including the symmetric keys
  8.1103 +  used in the digital envelopes.  On the other hand, M knows the true identity
  8.1104 +  of PG (namely j'), and sends AReq there; he can't, however, check that
  8.1105 +  the EXcrypt involves the correct PG's key.
  8.1106 +*}
  8.1107 +lemma P_sees_CM_agreement:
  8.1108 +     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
  8.1109 +         KC \<in> symKeys;
  8.1110 +         Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
  8.1111 +           \<in> set evs;
  8.1112 +         C = Cardholder k;
  8.1113 +         PI_sign = sign (priSK C) {|Hash PIData, HOIData|};
  8.1114 +         P_I = {|PI_sign,
  8.1115 +                 EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};
  8.1116 +         PANData = {|Pan (pan C), Nonce (PANSecret k)|};
  8.1117 +         PIData = {|PIHead, PANData|};
  8.1118 +         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  8.1119 +                    TransStain|};
  8.1120 +         evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
  8.1121 +  ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.
  8.1122 +           HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
  8.1123 +           HOIData = Hash OIData &
  8.1124 +           Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &
  8.1125 +           Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &
  8.1126 +           Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
  8.1127 +                           AuthReqData P_I'')  \<in>  set evs &
  8.1128 +           P_I' = {|PI_sign,
  8.1129 +             EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &
  8.1130 +           P_I'' = {|PI_sign,
  8.1131 +             EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"
  8.1132 +apply clarify
  8.1133 +apply (rule exE)
  8.1134 +apply (rule P_verifies_Signed_PReq [OF refl refl refl])
  8.1135 +apply (simp (no_asm_use) add: sign_def EncB_def, blast)
  8.1136 +apply (assumption+, clarify, simp)
  8.1137 +apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
  8.1138 +apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2)
  8.1139 +done
  8.1140 +
  8.1141 +end
  8.1142 +
  8.1143 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/SET-Protocol/ROOT.ML	Tue Sep 23 15:40:27 2003 +0200
     9.3 @@ -0,0 +1,16 @@
     9.4 +(*  Title:      HOL/SET-Protocol/ROOT
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   2003  University of Cambridge
     9.8 +
     9.9 +Root file for the SET protocol proofs.
    9.10 +*)
    9.11 +
    9.12 +goals_limit := 1;
    9.13 +set timing;
    9.14 +
    9.15 +no_document use_thy "NatPair";
    9.16 +time_use_thy "Cardholder_Registration";
    9.17 +time_use_thy "Merchant_Registration";
    9.18 +time_use_thy "Purchase";
    9.19 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/SET-Protocol/document/root.tex	Tue Sep 23 15:40:27 2003 +0200
    10.3 @@ -0,0 +1,27 @@
    10.4 +\documentclass[10pt,a4paper,twoside]{article}
    10.5 +\usepackage{graphicx}
    10.6 +\usepackage{latexsym,theorem}
    10.7 +\usepackage{isabelle,isabellesym}
    10.8 +\usepackage{pdfsetup}\urlstyle{rm}
    10.9 +
   10.10 +\begin{document}
   10.11 +
   10.12 +\pagestyle{headings}
   10.13 +\pagenumbering{arabic}
   10.14 +
   10.15 +\title{Verification of The SET Protocol}
   10.16 +\author{Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson et al.}
   10.17 +\maketitle
   10.18 +
   10.19 +\tableofcontents
   10.20 +
   10.21 +\begin{center}
   10.22 +  \includegraphics[scale=0.5]{session_graph}  
   10.23 +\end{center}
   10.24 +
   10.25 +\newpage
   10.26 +
   10.27 +\parindent 0pt\parskip 0.5ex
   10.28 +
   10.29 +\input{session}
   10.30 +\end{document}