--- a/NEWS Mon Sep 22 16:19:46 2003 +0200
+++ b/NEWS Tue Sep 23 15:40:27 2003 +0200
@@ -38,6 +38,8 @@
* 'specification' command added, allowing for definition by
specification.
+* SET-Protocol: formalization and verification of the SET protocol suite;
+
New in Isabelle2003 (May 2003)
--------------------------------
--- a/src/HOL/IsaMakefile Mon Sep 22 16:19:46 2003 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 23 15:40:27 2003 +0200
@@ -35,6 +35,7 @@
HOL-NanoJava \
HOL-NumberTheory \
HOL-Prolog \
+ HOL-SET-Protocol \
HOL-Subst \
TLA-Buffer \
TLA-Inc \
@@ -386,8 +387,7 @@
UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
- UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \
- UNITY/Simple/Network.thy\
+ UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
@@ -615,6 +615,22 @@
@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
+## HOL-SET-Protocol
+
+HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
+
+$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
+ SET-Protocol/MessageSET.thy\
+ SET-Protocol/EventSET.thy\
+ SET-Protocol/PublicSET.thy\
+ SET-Protocol/Cardholder_Registration.thy\
+ SET-Protocol/Merchant_Registration.thy\
+ SET-Protocol/Purchase.thy\
+ SET-Protocol/document/root.tex
+ @$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
+
+
+
## TLA
TLA: HOL $(OUT)/TLA
@@ -679,6 +695,6 @@
$(LOG)/HOL-Lattice \
$(LOG)/HOL-Complex.gz \
$(LOG)/HOL-Complex-ex.gz \
- $(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/TLA-Inc.gz \
- $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
+ $(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
+ $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,1084 @@
+(* Title: HOL/Auth/SET/Cardholder_Registration
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
+ Piero Tramontano
+*)
+
+header{*The SET Cardholder Registration Protocol*}
+
+theory Cardholder_Registration = PublicSET:
+
+text{*Note: nonces seem to consist of 20 bytes. That includes both freshness
+challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
+*}
+
+text{*Simplifications involving @{text analz_image_keys_simps} appear to
+have become much slower. The cause is unclear. However, there is a big blow-up
+and the rewriting is very sensitive to the set of rewrite rules given.*}
+
+subsection{*Predicate Formalizing the Encryption Association between Keys *}
+
+consts
+ KeyCryptKey :: "[key, key, event list] => bool"
+
+primrec
+
+KeyCryptKey_Nil:
+ "KeyCryptKey DK K [] = False"
+
+KeyCryptKey_Cons:
+ --{*Says is the only important case.
+ 1st case: CR5, where KC3 encrypts KC2.
+ 2nd case: any use of priEK C.
+ Revision 1.12 has a more complicated version with separate treatment of
+ the dependency of KC1, KC2 and KC3 on priEK (CA i.) Not needed since
+ priEK C is never sent (and so can't be lost except at the start). *}
+ "KeyCryptKey DK K (ev # evs) =
+ (KeyCryptKey DK K evs |
+ (case ev of
+ Says A B Z =>
+ ((\<exists>N X Y. A \<noteq> Spy &
+ DK \<in> symKeys &
+ Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
+ (\<exists>C. DK = priEK C))
+ | Gets A' X => False
+ | Notes A' X => False))"
+
+
+subsection{*Predicate formalizing the association between keys and nonces *}
+
+consts
+ KeyCryptNonce :: "[key, key, event list] => bool"
+
+primrec
+
+KeyCryptNonce_Nil:
+ "KeyCryptNonce EK K [] = False"
+
+KeyCryptNonce_Cons:
+ --{*Says is the only important case.
+ 1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
+ 2nd case: CR5, where KC3 encrypts NC3;
+ 3rd case: CR6, where KC2 encrypts NC3;
+ 4th case: CR6, where KC2 encrypts NonceCCA;
+ 5th case: any use of @{term "priEK C"} (including CardSecret).
+ NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
+ But we can't prove @{text Nonce_compromise} unless the relation covers ALL
+ nonces that the protocol keeps secret.
+ *}
+ "KeyCryptNonce DK N (ev # evs) =
+ (KeyCryptNonce DK N evs |
+ (case ev of
+ Says A B Z =>
+ A \<noteq> Spy &
+ ((\<exists>X Y. DK \<in> symKeys &
+ Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
+ (\<exists>X Y. DK \<in> symKeys &
+ Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
+ (\<exists>K i X Y.
+ K \<in> symKeys &
+ Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
+ (DK=K | KeyCryptKey DK K evs)) |
+ (\<exists>K C NC3 Y.
+ K \<in> symKeys &
+ Z = Crypt K
+ {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
+ Y|} &
+ (DK=K | KeyCryptKey DK K evs)) |
+ (\<exists>C. DK = priEK C))
+ | Gets A' X => False
+ | Notes A' X => False))"
+
+
+subsection{*Formal protocol definition *}
+
+consts set_cr :: "event list set"
+inductive set_cr
+ intros
+
+ Nil: --{*Initial trace is empty*}
+ "[] \<in> set_cr"
+
+ Fake: --{*The spy MAY say anything he CAN say.*}
+ "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> set_cr"
+
+ Reception: --{*If A sends a message X to B, then B might receive it*}
+ "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> set_cr"
+
+ SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
+ "[| evs1 \<in> set_cr; C = Cardholder k; Nonce NC1 \<notin> used evs1 |]
+ ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
+
+ SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
+ "[| evs2 \<in> set_cr;
+ Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
+ ==> Says (CA i) C
+ {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
+ cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ # evs2 \<in> set_cr"
+
+ SET_CR3:
+ --{*RegFormReq: C sends his PAN and a new nonce to CA.
+ C verifies that
+ - nonce received is the same as that sent;
+ - certificates are signed by RCA;
+ - certificates are an encryption certificate (flag is onlyEnc) and a
+ signature certificate (flag is onlySig);
+ - certificates pertain to the CA that C contacted (this is done by
+ checking the signature).
+ C generates a fresh symmetric key KC1.
+ The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
+ is not clear. *}
+"[| evs3 \<in> set_cr; C = Cardholder k;
+ Nonce NC2 \<notin> used evs3;
+ Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
+ Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
+ cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)|}
+ \<in> set evs3;
+ Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
+ ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
+ # Notes C {|Key KC1, Agent (CA i)|}
+ # evs3 \<in> set_cr"
+
+ SET_CR4:
+ --{*RegFormRes:
+ CA responds sending NC2 back with a new nonce NCA, after checking that
+ - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
+ - the entire message is encrypted with the same key found inside the
+ envelope (here, KC1) *}
+"[| evs4 \<in> set_cr;
+ Nonce NCA \<notin> used evs4; KC1 \<in> symKeys;
+ Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
+ \<in> set evs4 |]
+ ==> Says (CA i) C
+ {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
+ cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ # evs4 \<in> set_cr"
+
+ SET_CR5:
+ --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
+ and its half of the secret value to CA.
+ We now assume that C has a fixed key pair, and he submits (pubSK C).
+ The protocol does not require this key to be fresh.
+ The encryption below is actually EncX.*}
+"[| evs5 \<in> set_cr; C = Cardholder k;
+ Nonce NC3 \<notin> used evs5; Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
+ Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
+ Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
+ Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
+ cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA) |}
+ \<in> set evs5;
+ Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
+ \<in> set evs5 |]
+==> Says C (CA i)
+ {|Crypt KC3
+ {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
+ Crypt (priSK C)
+ (Hash {|Agent C, Nonce NC3, Key KC2,
+ Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
+ Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
+ # Notes C {|Key KC2, Agent (CA i)|}
+ # Notes C {|Key KC3, Agent (CA i)|}
+ # evs5 \<in> set_cr"
+
+
+ --{* CertRes: CA responds sending NC3 back with its half of the secret value,
+ its signature certificate and the new cardholder signature
+ certificate. CA checks to have never certified the key proposed by C.
+ NOTE: In Merchant Registration, the corresponding rule (4)
+ uses the "sign" primitive. The encryption below is actually @{term EncK},
+ which is just @{term "Crypt K (sign SK X)"}.
+*}
+
+SET_CR6:
+"[| evs6 \<in> set_cr;
+ Nonce NonceCCA \<notin> used evs6;
+ KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys;
+ Notes (CA i) (Key cardSK) \<notin> set evs6;
+ Gets (CA i)
+ {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
+ Crypt (invKey cardSK)
+ (Hash {|Agent C, Nonce NC3, Key KC2,
+ Key cardSK, Pan (pan C), Nonce CardSecret|})|},
+ Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
+ \<in> set evs6 |]
+==> Says (CA i) C
+ (Crypt KC2
+ {|sign (priSK (CA i))
+ {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+ certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ # Notes (CA i) (Key cardSK)
+ # evs6 \<in> set_cr"
+
+
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+text{*A "possibility property": there are traces that reach the end.
+ An unconstrained proof with many subgoals.*}
+
+lemma Says_to_Gets:
+ "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
+by (rule set_cr.Reception, auto)
+
+text{*The many nonces and keys generated, some simultaneously, force us to
+ introduce them explicitly as shown below.*}
+lemma possibility_CR6:
+ "[|NC1 < (NC2::nat); NC2 < NC3; NC3 < NCA ;
+ NCA < NonceCCA; NonceCCA < CardSecret;
+ KC1 < (KC2::key); KC2 < KC3;
+ KC1 \<in> symKeys; Key KC1 \<notin> used [];
+ KC2 \<in> symKeys; Key KC2 \<notin> used [];
+ KC3 \<in> symKeys; Key KC3 \<notin> used [];
+ C = Cardholder k|]
+ ==> \<exists>evs \<in> set_cr.
+ Says (CA i) C
+ (Crypt KC2
+ {|sign (priSK (CA i))
+ {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+ certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
+ onlySig (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] ?NC1.8 = NC1 and ?NC1.10 = NC1
+ and ?NC2.4 = NC2 and ?NC2.6 = NC2
+ and ?NC3.0 = NC3 and ?NC3.2 = NC3
+ and NCA2 = NCA and NCA4 = NCA
+ and CardSecret = CardSecret and CardSecret2 = CardSecret
+ and ?KC1.4 = KC1 and ?KC1.6 = KC1
+ and ?KC2.0 = KC2 and ?KC2.2 = KC2
+ and ?KC3.0 = KC3 and ?KC3.2 = KC3
+ in
+ set_cr.Nil [THEN set_cr.SET_CR1, THEN Says_to_Gets,
+ THEN set_cr.SET_CR2, THEN Says_to_Gets,
+ THEN set_cr.SET_CR3, THEN Says_to_Gets,
+ THEN set_cr.SET_CR4, THEN Says_to_Gets,
+ THEN set_cr.SET_CR5, THEN Says_to_Gets,
+ THEN set_cr.SET_CR6])
+apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
+apply auto
+done
+
+
+text{*General facts about message reception*}
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
+
+
+subsection{*Proofs on keys *}
+
+text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
+
+lemma Spy_see_private_Key [simp]:
+ "evs \<in> set_cr
+ ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
+by (erule set_cr.induct, auto)
+
+lemma Spy_analz_private_Key [simp]:
+ "evs \<in> set_cr ==>
+ (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
+by auto
+
+declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
+declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
+
+
+subsection{*Begin Piero's Theorems on Certificates*}
+text{*Trivial in the current model, where certificates by RCA are secure *}
+
+lemma Crypt_valid_pubEK:
+ "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_cr |] ==> EKi = pubEK C"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+lemma certificate_valid_pubEK:
+ "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_cr |]
+ ==> EKi = pubEK C"
+apply (unfold cert_def signCert_def)
+apply (blast dest!: Crypt_valid_pubEK)
+done
+
+lemma Crypt_valid_pubSK:
+ "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_cr |] ==> SKi = pubSK C"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+lemma certificate_valid_pubSK:
+ "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_cr |] ==> SKi = pubSK C"
+apply (unfold cert_def signCert_def)
+apply (blast dest!: Crypt_valid_pubSK)
+done
+
+lemma Gets_certificate_valid:
+ "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
+ cert C SKi onlySig (priSK RCA)|} \<in> set evs;
+ evs \<in> set_cr |]
+ ==> EKi = pubEK C & SKi = pubSK C"
+by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
+
+text{*Nobody can have used non-existent keys!*}
+lemma new_keys_not_used:
+ "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
+ ==> K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (frule_tac [8] Gets_certificate_valid)
+apply (frule_tac [6] Gets_certificate_valid, simp_all)
+txt{*Fake*}
+apply (force dest!: usedI keysFor_parts_insert)
+txt{*Others*}
+apply blast
+apply auto
+done
+
+
+subsection{*New versions: as above, but generalized to have the KK argument *}
+
+lemma gen_new_keys_not_used:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
+ ==> Key K \<notin> used evs --> K \<in> symKeys -->
+ K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
+by (auto simp add: new_keys_not_used)
+
+lemma gen_new_keys_not_analzd:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
+ ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
+by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
+ dest: gen_new_keys_not_used)
+
+lemma analz_Key_image_insert_eq:
+ "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
+ ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
+ insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
+by (simp add: gen_new_keys_not_analzd)
+
+lemma Crypt_parts_imp_used:
+ "[|Crypt K X \<in> parts (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
+apply (rule ccontr)
+apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
+done
+
+lemma Crypt_analz_imp_used:
+ "[|Crypt K X \<in> analz (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
+by (blast intro: Crypt_parts_imp_used)
+
+
+subsection{*Messages signed by CA*}
+
+text{*Message @{text SET_CR2}: C can check CA's signature if he has received
+ CA's certificate.*}
+lemma CA_Says_2_lemma:
+ "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
+ \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+text{*Ever used?*}
+lemma CA_Says_2:
+ "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
+ \<in> parts (knows Spy evs);
+ cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
+ \<in> set evs"
+by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
+
+
+text{*Message @{text SET_CR4}: C can check CA's signature if he has received
+ CA's certificate.*}
+lemma CA_Says_4_lemma:
+ "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
+ \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
+ {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+text{*NEVER USED*}
+lemma CA_Says_4:
+ "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
+ \<in> parts (knows Spy evs);
+ cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
+ {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
+by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
+
+
+text{*Message @{text SET_CR6}: C can check CA's signature if he has
+ received CA's certificate.*}
+lemma CA_Says_6_lemma:
+ "[| Crypt (priSK (CA i))
+ (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
+ \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
+ {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+text{*NEVER USED*}
+lemma CA_Says_6:
+ "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
+ \<in> parts (knows Spy evs);
+ cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_cr; (CA i) \<notin> bad |]
+ ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
+ {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
+by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
+
+
+
+subsection{*Useful lemmas *}
+
+text{*Rewriting rule for private encryption keys. Analogous rewriting rules
+for other keys aren't needed.*}
+
+lemma parts_image_priEK:
+ "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
+ evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
+by auto
+
+text{*trivial proof because (priEK C) never appears even in (parts evs)*}
+lemma analz_image_priEK:
+ "evs \<in> set_cr ==>
+ (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
+ (priEK C \<in> KK | C \<in> bad)"
+by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
+
+
+subsection{*Secrecy of Session Keys *}
+
+subsubsection{*Lemmas about the predicate KeyCryptKey *}
+
+text{*A fresh DK cannot be associated with any other
+ (with respect to a given trace). *}
+lemma DK_fresh_not_KeyCryptKey:
+ "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (simp_all (no_asm_simp))
+apply (blast dest: Crypt_analz_imp_used)+
+done
+
+text{*A fresh K cannot be associated with any other. The assumption that
+ DK isn't a private encryption key may be an artifact of the particular
+ definition of KeyCryptKey.*}
+lemma K_fresh_not_KeyCryptKey:
+ "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
+apply (induct evs)
+apply (auto simp add: parts_insert2 split add: event.split)
+done
+
+
+text{*This holds because if (priEK (CA i)) appears in any traffic then it must
+ be known to the Spy, by @{term Spy_see_private_Key}*}
+lemma cardSK_neq_priEK:
+ "[|Key cardSK \<notin> analz (knows Spy evs);
+ Key cardSK : parts (knows Spy evs);
+ evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
+by blast
+
+lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
+ "[|cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr|] ==>
+ Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
+by (erule set_cr.induct, analz_mono_contra, auto)
+
+text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
+lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
+apply (induct_tac "evs")
+apply (auto simp add: parts_insert2 split add: event.split)
+done
+
+text{*Lemma for message 6: either cardSK is compromised (when we don't care)
+ or else cardSK hasn't been used to encrypt K. Previously we treated
+ message 5 in the same way, but the current model assumes that rule
+ @{text SET_CR5} is executed only by honest agents.*}
+lemma msg6_KeyCryptKey_disj:
+ "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
+ \<in> set evs;
+ cardSK \<notin> symKeys; evs \<in> set_cr|]
+ ==> Key cardSK \<in> analz (knows Spy evs) |
+ (\<forall>K. ~ KeyCryptKey cardSK K evs)"
+by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
+
+text{*As usual: we express the property as a logical equivalence*}
+lemma Key_analz_image_Key_lemma:
+ "P --> (Key K \<in> analz (Key`KK Un H)) --> (K \<in> KK | Key K \<in> analz H)
+ ==>
+ P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+ML
+{*
+val Gets_certificate_valid = thm "Gets_certificate_valid";
+
+fun valid_certificate_tac i =
+ EVERY [ftac Gets_certificate_valid i,
+ assume_tac i,
+ etac conjE i, REPEAT (hyp_subst_tac i)];
+*}
+
+text{*The @{text "(no_asm)"} attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.*}
+lemma symKey_compromise [rule_format (no_asm)]:
+ "evs \<in> set_cr ==>
+ (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) -->
+ (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
+ (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
+apply (erule set_cr.induct)
+apply (rule_tac [!] allI) +
+apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_knows_absorb
+ analz_Key_image_insert_eq notin_image_iff
+ K_fresh_not_KeyCryptKey
+ DK_fresh_not_KeyCryptKey ball_conj_distrib
+ analz_image_priEK disj_simps)
+ --{*46 seconds on a 1.8GHz machine*}
+apply spy_analz
+txt{*3*}
+apply blast
+txt{*5*}
+apply blast
+done
+
+text{*The remaining quantifiers seem to be essential.
+ NO NEED to assume the cardholder's OK: bad cardholders don't do anything
+ wrong!!*}
+lemma symKey_secrecy [rule_format]:
+ "[|CA i \<notin> bad; K \<in> symKeys; evs \<in> set_cr|]
+ ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
+ Key K \<in> parts{X} -->
+ Cardholder c \<notin> bad -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule set_cr.induct)
+apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
+apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
+apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
+apply (simp_all del: image_insert image_Un imp_disjL
+ add: symKey_compromise fresh_notin_analz_knows_Spy
+ analz_image_keys_simps analz_knows_absorb
+ analz_Key_image_insert_eq notin_image_iff
+ K_fresh_not_KeyCryptKey
+ DK_fresh_not_KeyCryptKey
+ analz_image_priEK)
+ --{*13 seconds on a 1.8GHz machine*}
+txt{*Fake*}
+apply spy_analz
+apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
+done
+
+
+subsection{*Primary Goals of Cardholder Registration *}
+
+text{*The cardholder's certificate really was created by the CA, provided the
+ CA is uncompromised *}
+
+text{*Lemma concerning the actual signed message digest*}
+lemma cert_valid_lemma:
+ "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
+ \<in> parts (knows Spy evs);
+ CA i \<notin> bad; evs \<in> set_cr|]
+ ==> \<exists>KC2 X Y. Says (CA i) C
+ (Crypt KC2
+ {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (simp_all (no_asm_simp))
+apply auto
+done
+
+text{*Pre-packaged version for cardholder. We don't try to confirm the values
+ of KC2, X and Y, since they are not important.*}
+lemma certificate_valid_cardSK:
+ "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
+ cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
+ CA i \<notin> bad; evs \<in> set_cr|]
+ ==> \<exists>KC2 X Y. Says (CA i) C
+ (Crypt KC2
+ {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
+ \<in> set evs"
+by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
+ certificate_valid_pubSK cert_valid_lemma)
+
+
+lemma Hash_imp_parts [rule_format]:
+ "evs \<in> set_cr
+ ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
+ Nonce N \<in> parts (knows Spy evs)"
+apply (erule set_cr.induct, force)
+apply (simp_all (no_asm_simp))
+apply (blast intro: parts_mono [THEN [2] rev_subsetD])
+done
+
+lemma Hash_imp_parts2 [rule_format]:
+ "evs \<in> set_cr
+ ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
+ Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
+apply (erule set_cr.induct, force)
+apply (simp_all (no_asm_simp))
+apply (blast intro: parts_mono [THEN [2] rev_subsetD])
+done
+
+
+subsection{*Secrecy of Nonces*}
+
+subsubsection{*Lemmas about the predicate KeyCryptNonce *}
+
+text{*A fresh DK cannot be associated with any other
+ (with respect to a given trace). *}
+lemma DK_fresh_not_KeyCryptNonce:
+ "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
+ ==> ~ KeyCryptNonce DK K evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (simp_all (no_asm_simp))
+apply blast
+apply blast
+apply (auto simp add: DK_fresh_not_KeyCryptKey)
+done
+
+text{*A fresh N cannot be associated with any other
+ (with respect to a given trace). *}
+lemma N_fresh_not_KeyCryptNonce:
+ "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
+apply (induct_tac "evs")
+apply (case_tac [2] "a")
+apply (auto simp add: parts_insert2)
+done
+
+lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
+ "[|cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr|] ==>
+ Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
+apply (erule set_cr.induct, analz_mono_contra, simp_all)
+txt{*6*}
+apply (blast dest: not_KeyCryptKey_cardSK)
+done
+
+subsubsection{*Lemmas for message 5 and 6:
+ either cardSK is compromised (when we don't care)
+ or else cardSK hasn't been used to encrypt K. *}
+
+text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
+lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
+apply (induct_tac "evs")
+apply (auto simp add: parts_insert2 split add: event.split)
+done
+
+text{*Lemma for message 6: either cardSK is compromised (when we don't care)
+ or else cardSK hasn't been used to encrypt K.*}
+lemma msg6_KeyCryptNonce_disj:
+ "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
+ \<in> set evs;
+ cardSK \<notin> symKeys; evs \<in> set_cr|]
+ ==> Key cardSK \<in> analz (knows Spy evs) |
+ ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
+ (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
+by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
+ intro: cardSK_neq_priEK)
+
+
+text{*As usual: we express the property as a logical equivalence*}
+lemma Nonce_analz_image_Key_lemma:
+ "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
+ ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+text{*The @{text "(no_asm)"} attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.*}
+lemma Nonce_compromise [rule_format (no_asm)]:
+ "evs \<in> set_cr ==>
+ (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs) -->
+ (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
+ (Nonce N \<in> analz (knows Spy evs)))"
+apply (erule set_cr.induct)
+apply (rule_tac [!] allI)+
+apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
+apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
+apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
+apply (frule_tac [11] msg6_KeyCryptNonce_disj)
+apply (erule_tac [13] disjE)
+apply (simp_all del: image_insert image_Un
+ add: symKey_compromise
+ analz_image_keys_simps analz_knows_absorb
+ analz_Key_image_insert_eq notin_image_iff
+ N_fresh_not_KeyCryptNonce
+ DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
+ ball_conj_distrib analz_image_priEK)
+ --{*71 seconds on a 1.8GHz machine*}
+txt{*Fake*}
+apply spy_analz
+txt{*3*}
+apply blast
+txt{*5*}
+apply blast
+txt{*6*}
+txt{*cardSK compromised?*}
+apply (force del: allE ballE impCE simp add: symKey_compromise)
+txt{*Simplify again--necessary because the previous simplification introduces
+ some logical connectives*}
+by (force del: allE ballE impCE
+ simp del: image_insert image_Un imp_disjL
+ simp add: analz_image_keys_simps symKey_compromise)
+
+
+subsection{*Secrecy of CardSecret: the Cardholder's secret*}
+
+lemma NC2_not_CardSecret:
+ "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
+ \<in> parts (knows Spy evs);
+ Key K \<notin> analz (knows Spy evs);
+ Nonce N \<notin> analz (knows Spy evs);
+ evs \<in> set_cr|]
+ ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct, analz_mono_contra, simp_all)
+apply (blast dest: Hash_imp_parts)+
+done
+
+lemma KC2_secure_lemma [rule_format]:
+ "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
+ U \<in> parts (knows Spy evs);
+ evs \<in> set_cr|]
+ ==> Nonce N \<notin> analz (knows Spy evs) -->
+ (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs &
+ Cardholder k \<notin> bad & CA i \<notin> bad)"
+apply (erule_tac P = "U \<in> ?H" in rev_mp)
+apply (erule set_cr.induct)
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (simp_all del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_knows_absorb
+ analz_knows_absorb2 notin_image_iff)
+ --{*19 seconds on a 1.8GHz machine*}
+apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
+apply (blast intro!: analz_insertI)+
+done
+
+lemma KC2_secrecy:
+ "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
+ Nonce N \<notin> analz (knows Spy evs); KC2 \<in> symKeys;
+ evs \<in> set_cr|]
+ ==> Key KC2 \<notin> analz (knows Spy evs)"
+by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
+
+
+text{*Inductive version*}
+lemma CardSecret_secrecy_lemma [rule_format]:
+ "[|CA i \<notin> bad; evs \<in> set_cr|]
+ ==> Key K \<notin> analz (knows Spy evs) -->
+ Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
+ \<in> parts (knows Spy evs) -->
+ Nonce CardSecret \<notin> analz (knows Spy evs)"
+apply (erule set_cr.induct, analz_mono_contra)
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_knows_absorb
+ analz_Key_image_insert_eq notin_image_iff
+ EXHcrypt_def Crypt_notin_image_Key
+ N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
+ ball_conj_distrib Nonce_compromise symKey_compromise
+ analz_image_priEK)
+ --{*12 seconds on a 1.8GHz machine*}
+txt{*Fake*}
+apply spy_analz
+apply (simp_all (no_asm_simp))
+txt{*1*}
+apply blast
+txt{*2*}
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
+txt{*3*}
+apply blast
+txt{*4*}
+apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)
+txt{*5*}
+apply blast
+txt{*6*}
+apply (blast dest: KC2_secrecy)
+apply (blast dest: KC2_secrecy)
+done
+
+
+text{*Packaged version for cardholder*}
+lemma CardSecret_secrecy:
+ "[|Cardholder k \<notin> bad; CA i \<notin> bad;
+ Says (Cardholder k) (CA i)
+ {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
+ Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+ KC3 \<in> symKeys; evs \<in> set_cr|]
+ ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
+apply (frule Gets_certificate_valid, assumption)
+apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
+apply (blast dest: CardSecret_secrecy_lemma)
+apply (rule symKey_secrecy)
+apply (auto simp add: parts_insert2)
+done
+
+
+subsection{*Secrecy of NonceCCA [the CA's secret] *}
+
+lemma NC2_not_NonceCCA:
+ "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
+ \<in> parts (knows Spy evs);
+ Nonce N \<notin> analz (knows Spy evs);
+ evs \<in> set_cr|]
+ ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct, analz_mono_contra, simp_all)
+apply (blast dest: Hash_imp_parts2)+
+done
+
+
+text{*Inductive version*}
+lemma NonceCCA_secrecy_lemma [rule_format]:
+ "[|CA i \<notin> bad; evs \<in> set_cr|]
+ ==> Key K \<notin> analz (knows Spy evs) -->
+ Crypt K
+ {|sign (priSK (CA i))
+ {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
+ X, Y|}
+ \<in> parts (knows Spy evs) -->
+ Nonce NonceCCA \<notin> analz (knows Spy evs)"
+apply (erule set_cr.induct, analz_mono_contra)
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_knows_absorb sign_def
+ analz_Key_image_insert_eq notin_image_iff
+ EXHcrypt_def Crypt_notin_image_Key
+ N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
+ ball_conj_distrib Nonce_compromise symKey_compromise
+ analz_image_priEK)
+ --{*15 seconds on a 1.8GHz machine*}
+txt{*Fake*}
+apply spy_analz
+txt{*1*}
+apply blast
+txt{*2*}
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
+txt{*3*}
+apply blast
+txt{*4*}
+apply (blast dest: NC2_not_NonceCCA)
+txt{*5*}
+apply blast
+txt{*6*}
+apply (blast dest: KC2_secrecy)
+apply (blast dest: KC2_secrecy)
+done
+
+
+text{*Packaged version for cardholder*}
+lemma NonceCCA_secrecy:
+ "[|Cardholder k \<notin> bad; CA i \<notin> bad;
+ Gets (Cardholder k)
+ (Crypt KC2
+ {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
+ X, Y|}) \<in> set evs;
+ Says (Cardholder k) (CA i)
+ {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
+ Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+ KC2 \<in> symKeys; evs \<in> set_cr|]
+ ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
+apply (frule Gets_certificate_valid, assumption)
+apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
+apply (blast dest: NonceCCA_secrecy_lemma)
+apply (rule symKey_secrecy)
+apply (auto simp add: parts_insert2)
+done
+
+text{*We don't bother to prove guarantees for the CA. He doesn't care about
+ the PANSecret: it isn't his credit card!*}
+
+
+subsection{*Rewriting Rule for PANs*}
+
+text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
+ or if it is then (because it appears in traffic) that CA is bad,
+ and so the Spy knows that key already. Either way, we can simplify
+ the expression @{term "analz (insert (Key cardSK) X)"}.*}
+lemma msg6_cardSK_disj:
+ "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
+ \<in> set evs; evs \<in> set_cr |]
+ ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
+by auto
+
+lemma analz_image_pan_lemma:
+ "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H) ==>
+ (Pan P \<in> analz (Key`nE Un H)) = (Pan P \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+lemma analz_image_pan [rule_format]:
+ "evs \<in> set_cr ==>
+ \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
+ (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
+ (Pan P \<in> analz (knows Spy evs))"
+apply (erule set_cr.induct)
+apply (rule_tac [!] allI impI)+
+apply (rule_tac [!] analz_image_pan_lemma)
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
+apply (simp_all
+ del: image_insert image_Un
+ add: analz_image_keys_simps disjoint_image_iff
+ notin_image_iff analz_image_priEK)
+ --{*33 seconds on a 1.8GHz machine*}
+apply spy_analz
+txt{*6*}
+apply (simp add: insert_absorb)
+done
+
+lemma analz_insert_pan:
+ "[| evs \<in> set_cr; K \<notin> invKey ` pubEK ` range CA |] ==>
+ (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
+ (Pan P \<in> analz (knows Spy evs))"
+by (simp del: image_insert image_Un
+ add: analz_image_keys_simps analz_image_pan)
+
+
+text{*Confidentiality of the PAN\@. Maybe we could combine the statements of
+ this theorem with @{term analz_image_pan}, requiring a single induction but
+ a much more difficult proof.*}
+lemma pan_confidentiality:
+ "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
+ ==> \<exists>i X K HN.
+ Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
+ \<in> set evs
+ & (CA i) \<in> bad"
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
+apply (simp_all
+ del: image_insert image_Un
+ add: analz_image_keys_simps analz_insert_pan analz_image_pan
+ notin_image_iff analz_image_priEK)
+ --{*18 seconds on a 1.8GHz machine*}
+txt{*fake*}
+apply spy_analz
+txt{*3*}
+apply blast
+txt{*5*}
+apply blast
+txt{*6*}
+apply (simp (no_asm_simp) add: insert_absorb)
+done
+
+
+subsection{*Unicity*}
+
+lemma CR6_Says_imp_Notes:
+ "[|Says (CA i) C (Crypt KC2
+ {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
+ certC (pan C) cardSK X onlySig (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}) \<in> set evs;
+ evs \<in> set_cr |]
+ ==> Notes (CA i) (Key cardSK) \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (simp_all (no_asm_simp))
+done
+
+text{*Unicity of cardSK: it uniquely identifies the other components.
+ This holds because a CA accepts a cardSK at most once.*}
+lemma cardholder_key_unicity:
+ "[|Says (CA i) C (Crypt KC2
+ {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
+ certC (pan C) cardSK X onlySig (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ \<in> set evs;
+ Says (CA i) C' (Crypt KC2'
+ {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
+ certC (pan C') cardSK X' onlySig (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ \<in> set evs;
+ evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct)
+apply (simp_all (no_asm_simp))
+apply (blast dest!: CR6_Says_imp_Notes)
+done
+
+
+text{*UNUSED unicity result*}
+lemma unique_KC1:
+ "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
+ \<in> set evs;
+ Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
+ \<in> set evs;
+ C \<notin> bad; evs \<in> set_cr|] ==> B'=B & Y'=Y"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+text{*UNUSED unicity result*}
+lemma unique_KC2:
+ "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
+ Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
+ C \<notin> bad; evs \<in> set_cr|] ==> B'=B & X'=X"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_cr.induct, auto)
+done
+
+text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
+ it could be a previously compromised cardSK [e.g. involving a bad CA]*}
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/EventSET.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,271 @@
+(* Title: HOL/Auth/SET/EventSET
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+*)
+
+header{*Theory of Events for SET*}
+
+theory EventSET = MessageSET:
+
+text{*The Root Certification Authority*}
+syntax RCA :: agent
+translations "RCA" == "CA 0"
+
+
+text{*Message events*}
+datatype
+ event = Says agent agent msg
+ | Gets agent msg
+ | Notes agent msg
+
+
+text{*compromised agents: keys known, Notes visible*}
+consts bad :: "agent set"
+
+text{*Spy has access to his own key for spoof messages, but RCA is secure*}
+specification (bad)
+ Spy_in_bad [iff]: "Spy \<in> bad"
+ RCA_not_bad [iff]: "RCA \<notin> bad"
+ by (rule exI [of _ "{Spy}"], simp)
+
+
+subsection{*Agents' Knowledge*}
+
+consts (*Initial states of agents -- parameter of the construction*)
+ initState :: "agent => msg set"
+ knows :: "[agent, event list] => msg set"
+
+(* Message reception does not extend spy's knowledge because of
+ reception invariant enforced by Reception rule in protocol definition*)
+primrec
+
+knows_Nil:
+ "knows A [] = initState A"
+knows_Cons:
+ "knows A (ev # evs) =
+ (if A = Spy then
+ (case ev of
+ Says A' B X => insert X (knows Spy evs)
+ | Gets A' X => knows Spy evs
+ | Notes A' X =>
+ if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
+ else
+ (case ev of
+ Says A' B X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Gets A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Notes A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs))"
+
+
+subsection{*Used Messages*}
+
+consts
+ (*Set of items that might be visible to somebody:
+ complement of the set of fresh items*)
+ used :: "event list => msg set"
+
+(* As above, message reception does extend used items *)
+primrec
+ used_Nil: "used [] = (UN B. parts (initState B))"
+ used_Cons: "used (ev # evs) =
+ (case ev of
+ Says A B X => parts {X} Un (used evs)
+ | Gets A X => used evs
+ | Notes A X => parts {X} Un (used evs))"
+
+
+
+(* Inserted by default but later removed. This declaration lets the file
+be re-loaded. Addsimps [knows_Cons, used_Nil, *)
+
+(** Simplifying parts (insert X (knows Spy evs))
+ = parts {X} Un parts (knows Spy evs) -- since general case loops*)
+
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+
+lemma knows_Spy_Says [simp]:
+ "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
+by auto
+
+text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
+ on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
+lemma knows_Spy_Notes [simp]:
+ "knows Spy (Notes A X # evs) =
+ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
+apply auto
+done
+
+lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
+by auto
+
+lemma initState_subset_knows: "initState A <= knows A evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+lemma knows_Spy_subset_knows_Spy_Says:
+ "knows Spy evs <= knows Spy (Says A B X # evs)"
+by auto
+
+lemma knows_Spy_subset_knows_Spy_Notes:
+ "knows Spy evs <= knows Spy (Notes A X # evs)"
+by auto
+
+lemma knows_Spy_subset_knows_Spy_Gets:
+ "knows Spy evs <= knows Spy (Gets A X # evs)"
+by auto
+
+(*Spy sees what is sent on the traffic*)
+lemma Says_imp_knows_Spy [rule_format]:
+ "Says A B X \<in> set evs --> X \<in> knows Spy evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+(*Use with addSEs to derive contradictions from old Says events containing
+ items known to be fresh*)
+lemmas knows_Spy_partsEs =
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
+ parts.Body [THEN revcut_rl, standard]
+
+
+subsection{*Lemmas About Agents' Knowledge*}
+
+lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
+by auto
+
+lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
+by auto
+
+lemma knows_Gets:
+ "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
+by auto
+
+lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A B X # evs)"
+by auto
+
+lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A X # evs)"
+by auto
+
+lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A X # evs)"
+by auto
+
+(*Agents know what they say*)
+lemma Says_imp_knows [rule_format]:
+ "Says A B X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+(*Agents know what they note*)
+lemma Notes_imp_knows [rule_format]:
+ "Notes A X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+(*Agents know what they receive*)
+lemma Gets_imp_knows_agents [rule_format]:
+ "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+
+(*What agents DIFFERENT FROM Spy know
+ was either said, or noted, or got, or known initially*)
+lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
+ "[| X \<in> knows A evs; A \<noteq> Spy |] ==>
+ \<exists>B. Says A B X \<in> set evs |
+ Gets A X \<in> set evs |
+ Notes A X \<in> set evs |
+ X \<in> initState A"
+apply (erule rev_mp)
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+(*What the Spy knows -- for the time being --
+ was either said or noted, or known initially*)
+lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
+ "[| X \<in> knows Spy evs |] ==>
+ \<exists>A B. Says A B X \<in> set evs |
+ Notes A X \<in> set evs |
+ X \<in> initState Spy"
+apply (erule rev_mp)
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+
+subsection{*The Function @{term used}*}
+
+lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
+apply (induct_tac "evs")
+apply (auto simp add: parts_insert_knows_A split: event.split)
+done
+
+lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
+
+lemma initState_subset_used: "parts (initState B) <= used evs"
+apply (induct_tac "evs")
+apply (auto split: event.split)
+done
+
+lemmas initState_into_used = initState_subset_used [THEN subsetD]
+
+lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} Un used evs"
+by auto
+
+lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} Un used evs"
+by auto
+
+lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
+by auto
+
+lemma used_nil_subset: "used [] <= used evs"
+apply auto
+apply (rule initState_into_used, auto)
+done
+
+
+lemma Notes_imp_parts_subset_used [rule_format]:
+ "Notes A X \<in> set evs --> parts {X} <= used evs"
+apply (induct_tac "evs")
+apply (induct_tac [2] "a", auto)
+done
+
+text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
+declare knows_Cons [simp del]
+ used_Nil [simp del] used_Cons [simp del]
+
+
+text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
+ New events added by induction to "evs" are discarded. Provided
+ this information isn't needed, the proof will be much shorter, since
+ it will omit complicated reasoning about @{term analz}.*}
+
+lemmas analz_mono_contra =
+ knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
+ knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
+ knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
+ML
+{*
+val analz_mono_contra_tac =
+ let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+ in
+ rtac analz_impI THEN'
+ REPEAT1 o
+ (dresolve_tac (thms"analz_mono_contra"))
+ THEN' mp_tac
+ end
+*}
+
+method_setup analz_mono_contra = {*
+ Method.no_args
+ (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
+ "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,435 @@
+(* Title: HOL/Auth/SET/Merchant_Registration
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+*)
+
+header{*The SET Merchant Registration Protocol*}
+
+theory Merchant_Registration = PublicSET:
+
+text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
+ needed: no session key encrypts another. Instead we
+ prove the "key compromise" theorems for sets KK that contain no private
+ encryption keys (@{term "priEK C"}). *}
+
+
+consts set_mr :: "event list set"
+inductive set_mr
+ intros
+
+ Nil: --{*Initial trace is empty*}
+ "[] \<in> set_mr"
+
+
+ Fake: --{*The spy MAY say anything he CAN say.*}
+ "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> set_mr"
+
+
+ Reception: --{*If A sends a message X to B, then B might receive it*}
+ "[| evsr \<in> set_mr; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> set_mr"
+
+
+ SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
+ "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
+ ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
+
+
+ SET_MR2: --{*RegFormRes: CA replies with the registration form and the
+ certificates for her keys*}
+ "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
+ Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
+ ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
+ cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
+ # evs2 \<in> set_mr"
+
+ SET_MR3:
+ --{*CertReq: M submits the key pair to be certified. The Notes
+ event allows KM1 to be lost if M is compromised. Piero remarks
+ that the agent mentioned inside the signature is not verified to
+ correspond to M. As in CR, each Merchant has fixed key pairs. M
+ is only optionally required to send NCA back, so M doesn't do so
+ in the model*}
+ "[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3;
+ Key KM1 \<notin> used evs3; KM1 \<in> symKeys;
+ Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
+ cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA) |}
+ \<in> set evs3;
+ Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
+ ==> Says M (CA i)
+ {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
+ Key (pubSK M), Key (pubEK M)|}),
+ Crypt EKi (Key KM1)|}
+ # Notes M {|Key KM1, Agent (CA i)|}
+ # evs3 \<in> set_mr"
+
+ SET_MR4:
+ --{*CertRes: CA issues the certificates for merSK and merEK,
+ while checking never to have certified the m even
+ separately. NOTE: In Cardholder Registration the
+ corresponding rule (6) doesn't use the "sign" primitive. "The
+ CertRes shall be signed but not encrypted if the EE is a Merchant
+ or Payment Gateway."-- Programmer's Guide, page 191.*}
+ "[| evs4 \<in> set_mr; M = Merchant k;
+ merSK \<notin> symKeys; merEK \<notin> symKeys;
+ Notes (CA i) (Key merSK) \<notin> set evs4;
+ Notes (CA i) (Key merEK) \<notin> set evs4;
+ Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
+ {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
+ Crypt (pubEK (CA i)) (Key KM1) |}
+ \<in> set evs4 |]
+ ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
+ cert M merSK onlySig (priSK (CA i)),
+ cert M merEK onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ # Notes (CA i) (Key merSK)
+ # Notes (CA i) (Key merEK)
+ # evs4 \<in> set_mr"
+
+
+text{*Note possibility proofs are missing.*}
+
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+text{*General facts about message reception*}
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_mr.induct, auto)
+done
+
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+
+declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
+
+subsubsection{*Proofs on keys *}
+
+text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
+lemma Spy_see_private_Key [simp]:
+ "evs \<in> set_mr
+ ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
+apply (erule set_mr.induct)
+apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj])
+done
+
+lemma Spy_analz_private_Key [simp]:
+ "evs \<in> set_mr ==>
+ (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
+by auto
+
+declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
+declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
+
+(*This is to state that the signed keys received in step 4
+ are into parts - rather than installing sign_def each time.
+ Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK
+Goal "[|Gets C \<lbrace>Crypt KM1
+ (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace>
+ \<in> set evs; evs \<in> set_mr |]
+ ==> Key merSK \<in> parts (knows Spy evs) \<and>
+ Key merEK \<in> parts (knows Spy evs)"
+by (fast_tac (claset() addss (simpset())) 1);
+qed "signed_keys_in_parts";
+???*)
+
+text{*Proofs on certificates -
+ they hold, as in CR, because RCA's keys are secure*}
+
+lemma Crypt_valid_pubEK:
+ "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
+apply (erule rev_mp)
+apply (erule set_mr.induct, auto)
+done
+
+lemma certificate_valid_pubEK:
+ "[| cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_mr |]
+ ==> EKi = pubEK (CA i)"
+apply (unfold cert_def signCert_def)
+apply (blast dest!: Crypt_valid_pubEK)
+done
+
+lemma Crypt_valid_pubSK:
+ "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
+apply (erule rev_mp)
+apply (erule set_mr.induct, auto)
+done
+
+lemma certificate_valid_pubSK:
+ "[| cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
+apply (unfold cert_def signCert_def)
+apply (blast dest!: Crypt_valid_pubSK)
+done
+
+lemma Gets_certificate_valid:
+ "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+ evs \<in> set_mr |]
+ ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
+by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
+
+
+text{*Nobody can have used non-existent keys!*}
+lemma new_keys_not_used [rule_format,simp]:
+ "evs \<in> set_mr
+ ==> Key K \<notin> used evs --> K \<in> symKeys -->
+ K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule set_mr.induct, simp_all)
+txt{*Fake*}
+apply (force dest!: usedI keysFor_parts_insert)
+txt{*Message 2*}
+apply force
+txt{*Message 3*}
+apply (blast dest: Gets_certificate_valid)
+txt{*Message 4*}
+apply force
+done
+
+
+subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*}
+
+lemma gen_new_keys_not_used [rule_format]:
+ "evs \<in> set_mr
+ ==> Key K \<notin> used evs --> K \<in> symKeys -->
+ K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
+by auto
+
+lemma gen_new_keys_not_analzd:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
+ ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
+by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
+ dest: gen_new_keys_not_used)
+
+lemma analz_Key_image_insert_eq:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
+ ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
+ insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
+by (simp add: gen_new_keys_not_analzd)
+
+
+lemma Crypt_parts_imp_used:
+ "[|Crypt K X \<in> parts (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
+apply (rule ccontr)
+apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
+done
+
+lemma Crypt_analz_imp_used:
+ "[|Crypt K X \<in> analz (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
+by (blast intro: Crypt_parts_imp_used)
+
+text{*Rewriting rule for private encryption keys. Analogous rewriting rules
+for other keys aren't needed.*}
+
+lemma parts_image_priEK:
+ "[|Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs));
+ evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad"
+by auto
+
+text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*}
+lemma analz_image_priEK:
+ "evs \<in> set_mr ==>
+ (Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) =
+ (priEK (CA i) \<in> KK | CA i \<in> bad)"
+by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
+
+
+subsection{*Secrecy of Session Keys*}
+
+text{*This holds because if (priEK (CA i)) appears in any traffic then it must
+ be known to the Spy, by @{text Spy_see_private_Key}*}
+lemma merK_neq_priEK:
+ "[|Key merK \<notin> analz (knows Spy evs);
+ Key merK \<in> parts (knows Spy evs);
+ evs \<in> set_mr|] ==> merK \<noteq> priEK C"
+by blast
+
+text{*Lemma for message 4: either merK is compromised (when we don't care)
+ or else merK hasn't been used to encrypt K.*}
+lemma msg4_priEK_disj:
+ "[|Gets B {|Crypt KM1
+ (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
+ Y|} \<in> set evs;
+ evs \<in> set_mr|]
+ ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
+ & (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
+apply (unfold sign_def)
+apply (blast dest: merK_neq_priEK)
+done
+
+
+lemma Key_analz_image_Key_lemma:
+ "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
+ ==>
+ P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+lemma symKey_compromise:
+ "evs \<in> set_mr ==>
+ (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
+ (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
+ (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
+apply (erule set_mr.induct)
+apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
+apply (drule_tac [7] msg4_priEK_disj)
+apply (frule_tac [6] Gets_certificate_valid)
+apply (safe del: impI)
+apply (simp_all del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps abbrev_simps analz_knows_absorb
+ analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
+ Spy_analz_private_Key analz_image_priEK)
+ --{*23 seconds on a 1.8GHz machine*}
+txt{*Fake*}
+apply spy_analz
+txt{*Message 3*}
+apply auto
+done
+
+lemma symKey_secrecy [rule_format]:
+ "[|CA i \<notin> bad; K \<in> symKeys; evs \<in> set_mr|]
+ ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs -->
+ Key K \<in> parts{X} -->
+ Merchant m \<notin> bad -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule set_mr.induct)
+apply (drule_tac [7] msg4_priEK_disj)
+apply (frule_tac [6] Gets_certificate_valid)
+apply (safe del: impI)
+apply (simp_all del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps abbrev_simps analz_knows_absorb
+ analz_knows_absorb2 analz_Key_image_insert_eq
+ symKey_compromise notin_image_iff Spy_analz_private_Key
+ analz_image_priEK)
+txt{*Fake*}
+apply spy_analz
+txt{*Message 1*}
+apply force
+txt{*Message 3*}
+apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
+done
+
+subsection{*Unicity *}
+
+lemma msg4_Says_imp_Notes:
+ "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ cert M merSK onlySig (priSK (CA i)),
+ cert M merEK onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
+ evs \<in> set_mr |]
+ ==> Notes (CA i) (Key merSK) \<in> set evs
+ & Notes (CA i) (Key merEK) \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_mr.induct)
+apply (simp_all (no_asm_simp))
+done
+
+text{*Unicity of merSK wrt a given CA:
+ merSK uniquely identifies the other components, including merEK*}
+lemma merSK_unicity:
+ "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ cert M merSK onlySig (priSK (CA i)),
+ cert M merEK onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
+ Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
+ cert M' merSK onlySig (priSK (CA i)),
+ cert M' merEK' onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
+ evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_mr.induct)
+apply (simp_all (no_asm_simp))
+apply (blast dest!: msg4_Says_imp_Notes)
+done
+
+text{*Unicity of merEK wrt a given CA:
+ merEK uniquely identifies the other components, including merSK*}
+lemma merEK_unicity:
+ "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ cert M merSK onlySig (priSK (CA i)),
+ cert M merEK onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
+ Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
+ cert M' merSK' onlySig (priSK (CA i)),
+ cert M' merEK onlyEnc (priSK (CA i)),
+ cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
+ evs \<in> set_mr |]
+ ==> M=M' & NM2=NM2' & merSK=merSK'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_mr.induct)
+apply (simp_all (no_asm_simp))
+apply (blast dest!: msg4_Says_imp_Notes)
+done
+
+
+text{* -No interest on secrecy of nonces: they appear to be used
+ only for freshness.
+ -No interest on secrecy of merSK or merEK, as in CR.
+ -There's no equivalent of the PAN*}
+
+
+subsection{*Primary Goals of Merchant Registration *}
+
+subsubsection{*The merchant's certificates really were created by the CA,
+provided the CA is uncompromised *}
+
+text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses
+ certificates of the same form.*}
+lemma certificate_merSK_valid_lemma [intro]:
+ "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
+ \<in> parts (knows Spy evs);
+ CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|]
+ ==> \<exists>X Y Z. Says (CA i) M
+ {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_mr.induct)
+apply (simp_all (no_asm_simp))
+apply auto
+done
+
+lemma certificate_merSK_valid:
+ "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
+ CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|]
+ ==> \<exists>X Y Z. Says (CA i) M
+ {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
+by auto
+
+lemma certificate_merEK_valid_lemma [intro]:
+ "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
+ \<in> parts (knows Spy evs);
+ CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|]
+ ==> \<exists>X Y Z. Says (CA i) M
+ {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_mr.induct)
+apply (simp_all (no_asm_simp))
+apply auto
+done
+
+lemma certificate_merEK_valid:
+ "[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs);
+ CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|]
+ ==> \<exists>X Y Z. Says (CA i) M
+ {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
+by auto
+
+text{*The two certificates - for merSK and for merEK - cannot be proved to
+ have originated together*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/MessageSET.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,1025 @@
+(* Title: HOL/Auth/SET/MessageSET
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+*)
+
+header{*The Message Theory, Modified for SET*}
+
+theory MessageSET = NatPair:
+
+subsection{*General Lemmas*}
+
+text{*Needed occasionally with @{text spy_analz_tac}, e.g. in
+ @{text analz_insert_Key_newK}*}
+
+lemma Un_absorb3 [simp] : "A \<union> (B \<union> A) = B \<union> A"
+by blast
+
+text{*Collapses redundant cases in the huge protocol proofs*}
+lemmas disj_simps = disj_comms disj_left_absorb disj_assoc
+
+text{*Effective with assumptions like @{term "K \<notin> range pubK"} and
+ @{term "K \<notin> invKey`range pubK"}*}
+lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
+by blast
+
+text{*Effective with the assumption @{term "KK \<subseteq> - (range(invKey o pubK))"} *}
+lemma disjoint_image_iff: "(A <= - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)"
+by blast
+
+
+
+types
+ key = nat
+
+consts
+ all_symmetric :: bool --{*true if all keys are symmetric*}
+ invKey :: "key=>key" --{*inverse of a symmetric key*}
+
+specification (invKey)
+ invKey [simp]: "invKey (invKey K) = K"
+ invKey_symmetric: "all_symmetric --> invKey = id"
+ by (rule exI [of _ id], auto)
+
+
+text{*The inverse of a symmetric key is itself; that of a public key
+ is the private key and vice versa*}
+
+constdefs
+ symKeys :: "key set"
+ "symKeys == {K. invKey K = K}"
+
+text{*Agents. We allow any number of certification authorities, cardholders
+ merchants, and payment gateways.*}
+datatype
+ agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
+
+text{*Messages*}
+datatype
+ msg = Agent agent --{*Agent names*}
+ | Number nat --{*Ordinary integers, timestamps, ...*}
+ | Nonce nat --{*Unguessable nonces*}
+ | Pan nat --{*Unguessable Primary Account Numbers (??)*}
+ | Key key --{*Crypto keys*}
+ | Hash msg --{*Hashing*}
+ | MPair msg msg --{*Compound messages*}
+ | Crypt key msg --{*Encryption, public- or shared-key*}
+
+
+(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
+syntax
+ "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+
+syntax (xsymbols)
+ "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+
+translations
+ "{|x, y, z|}" == "{|x, {|y, z|}|}"
+ "{|x, y|}" == "MPair x y"
+
+
+constdefs
+ nat_of_agent :: "agent => nat"
+ "nat_of_agent == agent_case (curry nat2_to_nat 0)
+ (curry nat2_to_nat 1)
+ (curry nat2_to_nat 2)
+ (curry nat2_to_nat 3)
+ (nat2_to_nat (4,0))"
+ --{*maps each agent to a unique natural number, for specifications*}
+
+text{*The function is indeed injective*}
+lemma inj_nat_of_agent: "inj nat_of_agent"
+by (simp add: nat_of_agent_def inj_on_def curry_def
+ nat2_to_nat_inj [THEN inj_eq] split: agent.split)
+
+
+constdefs
+ (*Keys useful to decrypt elements of a message set*)
+ keysFor :: "msg set => key set"
+ "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
+
+subsubsection{*Inductive definition of all "parts" of a message.*}
+
+consts parts :: "msg set => msg set"
+inductive "parts H"
+ intros
+ Inj [intro]: "X \<in> H ==> X \<in> parts H"
+ Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
+ Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
+ Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+
+
+(*Monotonicity*)
+lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
+apply auto
+apply (erule parts.induct)
+apply (auto dest: Fst Snd Body)
+done
+
+
+subsubsection{*Inverse of keys*}
+
+(*Equations hold because constructors are injective; cannot prove for all f*)
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
+by auto
+
+lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
+by auto
+
+lemma Cardholder_image_eq [simp]: "(Cardholder x \<in> Cardholder`A) = (x \<in> A)"
+by auto
+
+lemma CA_image_eq [simp]: "(CA x \<in> CA`A) = (x \<in> A)"
+by auto
+
+lemma Pan_image_eq [simp]: "(Pan x \<in> Pan`A) = (x \<in> A)"
+by auto
+
+lemma Pan_Key_image_eq [simp]: "(Pan x \<notin> Key`A)"
+by auto
+
+lemma Nonce_Pan_image_eq [simp]: "(Nonce x \<notin> Pan`A)"
+by auto
+
+lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
+apply safe
+apply (drule_tac f = invKey in arg_cong, simp)
+done
+
+
+subsection{*keysFor operator*}
+
+lemma keysFor_empty [simp]: "keysFor {} = {}"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
+by (unfold keysFor_def, blast)
+
+(*Monotonicity*)
+lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Pan [simp]: "keysFor (insert (Pan A) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Crypt [simp]:
+ "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
+by (unfold keysFor_def, auto)
+
+lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
+by (unfold keysFor_def, blast)
+
+
+subsection{*Inductive relation "parts"*}
+
+lemma MPair_parts:
+ "[| {|X,Y|} \<in> parts H;
+ [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
+by (blast dest: parts.Fst parts.Snd)
+
+declare MPair_parts [elim!] parts.Body [dest!]
+text{*NB These two rules are UNSAFE in the formal sense, as they discard the
+ compound message. They work well on THIS FILE.
+ @{text MPair_parts} is left as SAFE because it speeds up proofs.
+ The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
+
+lemma parts_increasing: "H \<subseteq> parts(H)"
+by blast
+
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+
+lemma parts_empty [simp]: "parts{} = {}"
+apply safe
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
+by simp
+
+(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
+lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
+by (erule parts.induct, blast+)
+
+
+subsubsection{*Unions*}
+
+lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
+by (intro Un_least parts_mono Un_upper1 Un_upper2)
+
+lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
+by (intro equalityI parts_Un_subset1 parts_Un_subset2)
+
+lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
+apply (subst insert_is_Un [of _ H])
+apply (simp only: parts_Un)
+done
+
+(*TWO inserts to avoid looping. This rewrite is better than nothing.
+ Not suitable for Addsimps: its behaviour can be strange.*)
+lemma parts_insert2:
+ "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
+apply (simp add: Un_assoc)
+apply (simp add: parts_insert [symmetric])
+done
+
+lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
+by (intro UN_least parts_mono UN_upper)
+
+lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
+by (intro equalityI parts_UN_subset1 parts_UN_subset2)
+
+(*Added to simplify arguments to parts, analz and synth.
+ NOTE: the UN versions are no longer used!*)
+
+
+text{*This allows @{text blast} to simplify occurrences of
+ @{term "parts(G\<union>H)"} in the assumption.*}
+declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!]
+
+
+lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
+by (blast intro: parts_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Idempotence and transitivity*}
+
+lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
+by (erule parts.induct, blast+)
+
+lemma parts_idem [simp]: "parts (parts H) = parts H"
+by blast
+
+lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
+by (drule parts_mono, blast)
+
+(*Cut*)
+lemma parts_cut:
+ "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
+by (erule parts_trans, auto)
+
+lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
+by (force dest!: parts_cut intro: parts_insertI)
+
+
+subsubsection{*Rewrite rules for pulling out atomic messages*}
+
+lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
+
+
+lemma parts_insert_Agent [simp]:
+ "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Nonce [simp]:
+ "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Number [simp]:
+ "parts (insert (Number N) H) = insert (Number N) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Key [simp]:
+ "parts (insert (Key K) H) = insert (Key K) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Pan [simp]:
+ "parts (insert (Pan A) H) = insert (Pan A) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Hash [simp]:
+ "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Crypt [simp]:
+ "parts (insert (Crypt K X) H) =
+ insert (Crypt K X) (parts (insert X H))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (erule parts.induct)
+apply (blast intro: parts.Body)+
+done
+
+lemma parts_insert_MPair [simp]:
+ "parts (insert {|X,Y|} H) =
+ insert {|X,Y|} (parts (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (erule parts.induct)
+apply (blast intro: parts.Fst parts.Snd)+
+done
+
+lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
+apply auto
+apply (erule parts.induct, auto)
+done
+
+lemma parts_image_Pan [simp]: "parts (Pan`A) = Pan`A"
+apply auto
+apply (erule parts.induct, auto)
+done
+
+
+(*In any message, there is an upper bound N on its greatest nonce.*)
+lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
+apply (induct_tac "msg")
+apply (simp_all (no_asm_simp) add: exI parts_insert2)
+(*MPair case: blast_tac works out the necessary sum itself!*)
+prefer 2 apply (blast elim!: add_leE)
+(*Nonce case*)
+apply (rule_tac x = "N + Suc nat" in exI)
+apply (auto elim!: add_leE)
+done
+
+(* Ditto, for numbers.*)
+lemma msg_Number_supply: "\<exists>N. \<forall>n. N<=n --> Number n \<notin> parts {msg}"
+apply (induct_tac "msg")
+apply (simp_all (no_asm_simp) add: exI parts_insert2)
+prefer 2 apply (blast elim!: add_leE)
+apply (rule_tac x = "N + Suc nat" in exI, auto)
+done
+
+subsection{*Inductive relation "analz"*}
+
+text{*Inductive definition of "analz" -- what can be broken down from a set of
+ messages, including keys. A form of downward closure. Pairs can
+ be taken apart; messages decrypted with known keys.*}
+
+consts analz :: "msg set => msg set"
+inductive "analz H"
+ intros
+ Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
+ Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+ Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ Decrypt [dest]:
+ "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+
+
+(*Monotonicity; Lemma 1 of Lowe's paper*)
+lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
+apply auto
+apply (erule analz.induct)
+apply (auto dest: Fst Snd)
+done
+
+text{*Making it safe speeds up proofs*}
+lemma MPair_analz [elim!]:
+ "[| {|X,Y|} \<in> analz H;
+ [| X \<in> analz H; Y \<in> analz H |] ==> P
+ |] ==> P"
+by (blast dest: analz.Fst analz.Snd)
+
+lemma analz_increasing: "H \<subseteq> analz(H)"
+by blast
+
+lemma analz_subset_parts: "analz H \<subseteq> parts H"
+apply (rule subsetI)
+apply (erule analz.induct, blast+)
+done
+
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+
+
+lemma parts_analz [simp]: "parts (analz H) = parts H"
+apply (rule equalityI)
+apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
+apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
+done
+
+lemma analz_parts [simp]: "analz (parts H) = parts H"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+
+subsubsection{*General equational properties*}
+
+lemma analz_empty [simp]: "analz{} = {}"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+(*Converse fails: we can analz more from the union than from the
+ separate parts, as a key in one might decrypt a message in the other*)
+lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
+by (intro Un_least analz_mono Un_upper1 Un_upper2)
+
+lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Rewrite rules for pulling out atomic messages*}
+
+lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
+
+lemma analz_insert_Agent [simp]:
+ "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Nonce [simp]:
+ "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Number [simp]:
+ "analz (insert (Number N) H) = insert (Number N) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Hash [simp]:
+ "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+(*Can only pull out Keys if they are not needed to decrypt the rest*)
+lemma analz_insert_Key [simp]:
+ "K \<notin> keysFor (analz H) ==>
+ analz (insert (Key K) H) = insert (Key K) (analz H)"
+apply (unfold keysFor_def)
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_MPair [simp]:
+ "analz (insert {|X,Y|} H) =
+ insert {|X,Y|} (analz (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+apply (erule analz.induct)
+apply (blast intro: analz.Fst analz.Snd)+
+done
+
+(*Can pull out enCrypted message if the Key is not known*)
+lemma analz_insert_Crypt:
+ "Key (invKey K) \<notin> analz H
+ ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Pan [simp]:
+ "analz (insert (Pan A) H) = insert (Pan A) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma lemma1: "Key (invKey K) \<in> analz H ==>
+ analz (insert (Crypt K X) H) \<subseteq>
+ insert (Crypt K X) (analz (insert X H))"
+apply (rule subsetI)
+apply (erule_tac xa = x in analz.induct, auto)
+done
+
+lemma lemma2: "Key (invKey K) \<in> analz H ==>
+ insert (Crypt K X) (analz (insert X H)) \<subseteq>
+ analz (insert (Crypt K X) H)"
+apply auto
+apply (erule_tac xa = x in analz.induct, auto)
+apply (blast intro: analz_insertI analz.Decrypt)
+done
+
+lemma analz_insert_Decrypt:
+ "Key (invKey K) \<in> analz H ==>
+ analz (insert (Crypt K X) H) =
+ insert (Crypt K X) (analz (insert X H))"
+by (intro equalityI lemma1 lemma2)
+
+(*Case analysis: either the message is secure, or it is not!
+ Effective, but can cause subgoals to blow up!
+ Use with split_if; apparently split_tac does not cope with patterns
+ such as "analz (insert (Crypt K X) H)" *)
+lemma analz_Crypt_if [simp]:
+ "analz (insert (Crypt K X) H) =
+ (if (Key (invKey K) \<in> analz H)
+ then insert (Crypt K X) (analz (insert X H))
+ else insert (Crypt K X) (analz H))"
+by (simp add: analz_insert_Crypt analz_insert_Decrypt)
+
+
+(*This rule supposes "for the sake of argument" that we have the key.*)
+lemma analz_insert_Crypt_subset:
+ "analz (insert (Crypt K X) H) \<subseteq>
+ insert (Crypt K X) (analz (insert X H))"
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+lemma analz_image_Pan [simp]: "analz (Pan`A) = Pan`A"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+
+subsubsection{*Idempotence and transitivity*}
+
+lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
+by (erule analz.induct, blast+)
+
+lemma analz_idem [simp]: "analz (analz H) = analz H"
+by blast
+
+lemma analz_trans: "[| X\<in> analz G; G \<subseteq> analz H |] ==> X\<in> analz H"
+by (drule analz_mono, blast)
+
+(*Cut; Lemma 2 of Lowe*)
+lemma analz_cut: "[| Y\<in> analz (insert X H); X\<in> analz H |] ==> Y\<in> analz H"
+by (erule analz_trans, blast)
+
+(*Cut can be proved easily by induction on
+ "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
+*)
+
+(*This rewrite rule helps in the simplification of messages that involve
+ the forwarding of unknown components (X). Without it, removing occurrences
+ of X can be very complicated. *)
+lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
+by (blast intro: analz_cut analz_insertI)
+
+
+text{*A congruence rule for "analz"*}
+
+lemma analz_subset_cong:
+ "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
+ |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
+apply clarify
+apply (erule analz.induct)
+apply (best intro: analz_mono [THEN subsetD])+
+done
+
+lemma analz_cong:
+ "[| analz G = analz G'; analz H = analz H'
+ |] ==> analz (G \<union> H) = analz (G' \<union> H')"
+by (intro equalityI analz_subset_cong, simp_all)
+
+lemma analz_insert_cong:
+ "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
+by (force simp only: insert_def intro!: analz_cong)
+
+(*If there are no pairs or encryptions then analz does nothing*)
+lemma analz_trivial:
+ "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+(*These two are obsolete (with a single Spy) but cost little to prove...*)
+lemma analz_UN_analz_lemma:
+ "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+apply (erule analz.induct)
+apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
+done
+
+lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
+by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
+
+
+subsection{*Inductive relation "synth"*}
+
+text{*Inductive definition of "synth" -- what can be built up from a set of
+ messages. A form of upward closure. Pairs can be built, messages
+ encrypted with known keys. Agent names are public domain.
+ Numbers can be guessed, but Nonces cannot be.*}
+
+consts synth :: "msg set => msg set"
+inductive "synth H"
+ intros
+ Inj [intro]: "X \<in> H ==> X \<in> synth H"
+ Agent [intro]: "Agent agt \<in> synth H"
+ Number [intro]: "Number n \<in> synth H"
+ Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
+ MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+
+(*Monotonicity*)
+lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
+apply auto
+apply (erule synth.induct)
+apply (auto dest: Fst Snd Body)
+done
+
+(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*)
+inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
+inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
+inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
+inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
+inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
+inductive_cases Pan_synth [elim!]: "Pan A \<in> synth H"
+
+
+lemma synth_increasing: "H \<subseteq> synth(H)"
+by blast
+
+subsubsection{*Unions*}
+
+(*Converse fails: we can synth more from the union than from the
+ separate parts, building a compound message using elements of each.*)
+lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
+by (intro Un_least synth_mono Un_upper1 Un_upper2)
+
+lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
+by (blast intro: synth_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Idempotence and transitivity*}
+
+lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
+by (erule synth.induct, blast+)
+
+lemma synth_idem: "synth (synth H) = synth H"
+by blast
+
+lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
+by (drule synth_mono, blast)
+
+(*Cut; Lemma 2 of Lowe*)
+lemma synth_cut: "[| Y\<in> synth (insert X H); X\<in> synth H |] ==> Y\<in> synth H"
+by (erule synth_trans, blast)
+
+lemma Agent_synth [simp]: "Agent A \<in> synth H"
+by blast
+
+lemma Number_synth [simp]: "Number n \<in> synth H"
+by blast
+
+lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
+by blast
+
+lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
+by blast
+
+lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+by blast
+
+lemma Pan_synth_eq [simp]: "(Pan A \<in> synth H) = (Pan A \<in> H)"
+by blast
+
+lemma keysFor_synth [simp]:
+ "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
+by (unfold keysFor_def, blast)
+
+
+subsubsection{*Combinations of parts, analz and synth*}
+
+lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct)
+apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
+ parts.Fst parts.Snd parts.Body)+
+done
+
+lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
+apply (intro equalityI analz_subset_cong)+
+apply simp_all
+done
+
+lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct)
+prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
+apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
+done
+
+lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
+apply (cut_tac H = "{}" in analz_synth_Un)
+apply (simp (no_asm_use))
+done
+
+
+subsubsection{*For reasoning about the Fake rule in traces*}
+
+lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
+by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
+
+(*More specifically for Fake. Very occasionally we could do with a version
+ of the form parts{X} \<subseteq> synth (analz H) \<union> parts H *)
+lemma Fake_parts_insert: "X \<in> synth (analz H) ==>
+ parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
+apply (drule parts_insert_subset_Un)
+apply (simp (no_asm_use))
+apply blast
+done
+
+lemma Fake_parts_insert_in_Un:
+ "[|Z \<in> parts (insert X H); X: synth (analz H)|]
+ ==> Z \<in> synth (analz H) \<union> parts H";
+by (blast dest: Fake_parts_insert [THEN subsetD, dest])
+
+(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
+lemma Fake_analz_insert:
+ "X\<in> synth (analz G) ==>
+ analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
+apply (rule subsetI)
+apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
+prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
+apply (simp (no_asm_use))
+apply blast
+done
+
+lemma analz_conj_parts [simp]:
+ "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
+by (blast intro: analz_subset_parts [THEN subsetD])
+
+lemma analz_disj_parts [simp]:
+ "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
+by (blast intro: analz_subset_parts [THEN subsetD])
+
+(*Without this equation, other rules for synth and analz would yield
+ redundant cases*)
+lemma MPair_synth_analz [iff]:
+ "({|X,Y|} \<in> synth (analz H)) =
+ (X \<in> synth (analz H) & Y \<in> synth (analz H))"
+by blast
+
+lemma Crypt_synth_analz:
+ "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |]
+ ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
+by blast
+
+
+lemma Hash_synth_analz [simp]:
+ "X \<notin> synth (analz H)
+ ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+by blast
+
+
+(*We do NOT want Crypt... messages broken up in protocols!!*)
+declare parts.Body [rule del]
+
+
+text{*Rewrites to push in Key and Crypt messages, so that other messages can
+ be pulled out using the @{text analz_insert} rules*}
+ML
+{*
+fun insComm x y = inst "x" x (inst "y" y insert_commute);
+
+bind_thms ("pushKeys",
+ map (insComm "Key ?K")
+ ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
+ "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
+
+bind_thms ("pushCrypts",
+ map (insComm "Crypt ?X ?K")
+ ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
+ "Hash ?X'", "MPair ?X' ?Y"]);
+*}
+
+text{*Cannot be added with @{text "[simp]"} -- messages should not always be
+ re-ordered.*}
+lemmas pushes = pushKeys pushCrypts
+
+
+subsection{*Tactics useful for many protocol proofs*}
+ML
+{*
+val invKey = thm "invKey"
+val keysFor_def = thm "keysFor_def"
+val symKeys_def = thm "symKeys_def"
+val parts_mono = thm "parts_mono";
+val analz_mono = thm "analz_mono";
+val Key_image_eq = thm "Key_image_eq";
+val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
+val keysFor_Un = thm "keysFor_Un";
+val keysFor_mono = thm "keysFor_mono";
+val keysFor_image_Key = thm "keysFor_image_Key";
+val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
+val MPair_parts = thm "MPair_parts";
+val parts_increasing = thm "parts_increasing";
+val parts_insertI = thm "parts_insertI";
+val parts_empty = thm "parts_empty";
+val parts_emptyE = thm "parts_emptyE";
+val parts_singleton = thm "parts_singleton";
+val parts_Un_subset1 = thm "parts_Un_subset1";
+val parts_Un_subset2 = thm "parts_Un_subset2";
+val parts_insert = thm "parts_insert";
+val parts_insert2 = thm "parts_insert2";
+val parts_UN_subset1 = thm "parts_UN_subset1";
+val parts_UN_subset2 = thm "parts_UN_subset2";
+val parts_UN = thm "parts_UN";
+val parts_insert_subset = thm "parts_insert_subset";
+val parts_partsD = thm "parts_partsD";
+val parts_trans = thm "parts_trans";
+val parts_cut = thm "parts_cut";
+val parts_cut_eq = thm "parts_cut_eq";
+val parts_insert_eq_I = thm "parts_insert_eq_I";
+val parts_image_Key = thm "parts_image_Key";
+val MPair_analz = thm "MPair_analz";
+val analz_increasing = thm "analz_increasing";
+val analz_subset_parts = thm "analz_subset_parts";
+val not_parts_not_analz = thm "not_parts_not_analz";
+val parts_analz = thm "parts_analz";
+val analz_parts = thm "analz_parts";
+val analz_insertI = thm "analz_insertI";
+val analz_empty = thm "analz_empty";
+val analz_Un = thm "analz_Un";
+val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
+val analz_image_Key = thm "analz_image_Key";
+val analz_analzD = thm "analz_analzD";
+val analz_trans = thm "analz_trans";
+val analz_cut = thm "analz_cut";
+val analz_insert_eq = thm "analz_insert_eq";
+val analz_subset_cong = thm "analz_subset_cong";
+val analz_cong = thm "analz_cong";
+val analz_insert_cong = thm "analz_insert_cong";
+val analz_trivial = thm "analz_trivial";
+val analz_UN_analz = thm "analz_UN_analz";
+val synth_mono = thm "synth_mono";
+val synth_increasing = thm "synth_increasing";
+val synth_Un = thm "synth_Un";
+val synth_insert = thm "synth_insert";
+val synth_synthD = thm "synth_synthD";
+val synth_trans = thm "synth_trans";
+val synth_cut = thm "synth_cut";
+val Agent_synth = thm "Agent_synth";
+val Number_synth = thm "Number_synth";
+val Nonce_synth_eq = thm "Nonce_synth_eq";
+val Key_synth_eq = thm "Key_synth_eq";
+val Crypt_synth_eq = thm "Crypt_synth_eq";
+val keysFor_synth = thm "keysFor_synth";
+val parts_synth = thm "parts_synth";
+val analz_analz_Un = thm "analz_analz_Un";
+val analz_synth_Un = thm "analz_synth_Un";
+val analz_synth = thm "analz_synth";
+val parts_insert_subset_Un = thm "parts_insert_subset_Un";
+val Fake_parts_insert = thm "Fake_parts_insert";
+val Fake_analz_insert = thm "Fake_analz_insert";
+val analz_conj_parts = thm "analz_conj_parts";
+val analz_disj_parts = thm "analz_disj_parts";
+val MPair_synth_analz = thm "MPair_synth_analz";
+val Crypt_synth_analz = thm "Crypt_synth_analz";
+val Hash_synth_analz = thm "Hash_synth_analz";
+val pushes = thms "pushes";
+
+
+(*Prove base case (subgoal i) and simplify others. A typical base case
+ concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
+ alone.*)
+fun prove_simple_subgoals_tac i =
+ force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+ ALLGOALS Asm_simp_tac
+
+(*Analysis of Fake cases. Also works for messages that forward unknown parts,
+ but this application is no longer necessary if analz_insert_eq is used.
+ Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
+ DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+
+(*Apply rules to break down assumptions of the form
+ Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
+*)
+val Fake_insert_tac =
+ dresolve_tac [impOfSubs Fake_analz_insert,
+ impOfSubs Fake_parts_insert] THEN'
+ eresolve_tac [asm_rl, thm"synth.Inj"];
+
+fun Fake_insert_simp_tac ss i =
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+
+fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
+ (Fake_insert_simp_tac ss 1
+ THEN
+ IF_UNSOLVED (Blast.depth_tac
+ (cs addIs [analz_insertI,
+ impOfSubs analz_subset_parts]) 4 1))
+
+(*The explicit claset and simpset arguments help it work with Isar*)
+fun gen_spy_analz_tac (cs,ss) i =
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac ss 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
+
+fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+*}
+
+(*By default only o_apply is built-in. But in the presence of eta-expansion
+ this means that some terms displayed as (f o g) will be rewritten, and others
+ will not!*)
+declare o_def [simp]
+
+
+lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
+by auto
+
+lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
+by auto
+
+lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
+by (simp add: synth_mono analz_mono)
+
+lemma Fake_analz_eq [simp]:
+ "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
+apply (drule Fake_analz_insert[of _ _ "H"])
+apply (simp add: synth_increasing[THEN Un_absorb2])
+apply (drule synth_mono)
+apply (simp add: synth_idem)
+apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
+done
+
+text{*Two generalizations of @{text analz_insert_eq}*}
+lemma gen_analz_insert_eq [rule_format]:
+ "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
+
+lemma synth_analz_insert_eq [rule_format]:
+ "X \<in> synth (analz H)
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+apply (erule synth.induct)
+apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
+done
+
+lemma Fake_parts_sing:
+ "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
+apply (rule subset_trans)
+ apply (erule_tac [2] Fake_parts_insert)
+apply (simp add: parts_mono)
+done
+
+lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
+
+method_setup spy_analz = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_spy_analz_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1))*}
+ "for proving the Fake case when analz is involved"
+
+method_setup atomic_spy_analz = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ atomic_spy_analz_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1))*}
+ "for debugging spy_analz"
+
+method_setup Fake_insert_simp = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1))*}
+ "for debugging spy_analz"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/PublicSET.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,586 @@
+(* Title: HOL/Auth/SET/PublicSET
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+*)
+
+header{*The Public-Key Theory, Modified for SET*}
+
+theory PublicSET = EventSET:
+
+subsection{*Symmetric and Asymmetric Keys*}
+
+axioms
+ Key_supply_ax:
+ "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs & K \<in> symKeys"
+ --{*Unlike the corresponding property of nonces, this cannot be proved.
+ We have infinitely many agents and there is nothing to stop their
+ keys from exhausting all the natural numbers. The axiom
+ assumes that their keys are dispersed so as to leave room for infinitely
+ many fresh session keys. We could, alternatively, restrict agents to
+ an unspecified finite number.*}
+
+
+text{*definitions influenced by the wish to assign asymmetric keys
+ - since the beginning - only to RCA and CAs, namely we need a partial
+ function on type Agent*}
+
+
+text{*The SET specs mention two signature keys for CAs - we only have one*}
+
+consts
+ publicKey :: "[bool, agent] => key"
+ --{*the boolean is TRUE if a signing key*}
+
+syntax
+ pubEK :: "agent => key"
+ pubSK :: "agent => key"
+ priEK :: "agent => key"
+ priSK :: "agent => key"
+
+translations
+ "pubEK" == "publicKey False"
+ "pubSK" == "publicKey True"
+
+ (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
+ "priEK A" == "invKey (pubEK A)"
+ "priSK A" == "invKey (pubSK A)"
+
+text{*By freeness of agents, no two agents have the same key. Since
+ @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
+
+specification (publicKey)
+ injective_publicKey:
+ "publicKey b A = publicKey c A' ==> b=c & A=A'"
+ apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"])
+ apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split)
+ apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
+(*or this, but presburger won't abstract out the function applications
+ apply presburger+
+*)
+ done
+
+
+axioms
+ (*No private key equals any public key (essential to ensure that private
+ keys are private!) *)
+ privateKey_neq_publicKey [iff]:
+ "invKey (publicKey b A) \<noteq> publicKey b' A'"
+
+declare privateKey_neq_publicKey [THEN not_sym, iff]
+
+
+subsection{*Initial Knowledge*}
+
+text{*This information is not necessary. Each protocol distributes any needed
+certificates, and anyway our proofs require a formalization of the Spy's
+knowledge only. However, the initial knowledge is as follows:
+ All agents know RCA's public keys;
+ RCA and CAs know their own respective keys;
+ RCA (has already certified and therefore) knows all CAs public keys;
+ Spy knows all keys of all bad agents.*}
+primrec
+
+ initState_CA:
+ "initState (CA i) =
+ (if i=0 then Key ` ({priEK RCA, priSK RCA} Un
+ pubEK ` (range CA) Un pubSK ` (range CA))
+ else {Key (priEK (CA i)), Key (priSK (CA i)),
+ Key (pubEK (CA i)), Key (pubSK (CA i)),
+ Key (pubEK RCA), Key (pubSK RCA)})"
+
+ initState_Cardholder:
+ "initState (Cardholder i) =
+ {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
+ Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
+ Key (pubEK RCA), Key (pubSK RCA)}"
+
+ initState_Merchant:
+ "initState (Merchant i) =
+ {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
+ Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
+ Key (pubEK RCA), Key (pubSK RCA)}"
+
+ initState_PG:
+ "initState (PG i) =
+ {Key (priEK (PG i)), Key (priSK (PG i)),
+ Key (pubEK (PG i)), Key (pubSK (PG i)),
+ Key (pubEK RCA), Key (pubSK RCA)}"
+
+ initState_Spy:
+ "initState Spy = Key ` (invKey ` pubEK ` bad Un
+ invKey ` pubSK ` bad Un
+ range pubEK Un range pubSK)"
+
+
+text{*Injective mapping from agents to PANs: an agent can have only one card*}
+
+consts pan :: "agent => nat"
+
+specification (pan)
+ inj_pan: "inj pan"
+ --{*No two agents have the same PAN*}
+ apply (rule exI [of _ "nat_of_agent"])
+ apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq])
+ done
+
+declare inj_pan [THEN inj_eq, iff]
+
+consts
+ XOR :: "nat*nat => nat" --{*no properties are assumed of exclusive-or*}
+
+
+subsection{*Signature Primitives*}
+
+constdefs
+
+ (* Signature = Message + signed Digest *)
+ sign :: "[key, msg]=>msg"
+ "sign K X == {|X, Crypt K (Hash X) |}"
+
+ (* Signature Only = signed Digest Only *)
+ signOnly :: "[key, msg]=>msg"
+ "signOnly K X == Crypt K (Hash X)"
+
+ (* Signature for Certificates = Message + signed Message *)
+ signCert :: "[key, msg]=>msg"
+ "signCert K X == {|X, Crypt K X |}"
+
+ (* Certification Authority's Certificate.
+ Contains agent name, a key, a number specifying the key's target use,
+ a key to sign the entire certificate.
+
+ Should prove if signK=priSK RCA and C=CA i,
+ then Ka=pubEK i or pubSK i depending on T ??
+ *)
+ cert :: "[agent, key, msg, key] => msg"
+ "cert A Ka T signK == signCert signK {|Agent A, Key Ka, T|}"
+
+
+ (* Cardholder's Certificate.
+ Contains a PAN, the certified key Ka, the PANSecret PS,
+ a number specifying the target use for Ka, the signing key signK.
+ *)
+ certC :: "[nat, key, nat, msg, key] => msg"
+ "certC PAN Ka PS T signK ==
+ signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
+
+ (*cert and certA have no repeated elements, so they could be translations,
+ but that's tricky and makes proofs slower*)
+
+syntax
+ "onlyEnc" :: msg
+ "onlySig" :: msg
+ "authCode" :: msg
+
+translations
+ "onlyEnc" == "Number 0"
+ "onlySig" == "Number (Suc 0)"
+ "authCode" == "Number (Suc (Suc 0))"
+
+subsection{*Encryption Primitives*}
+
+constdefs
+
+ EXcrypt :: "[key,key,msg,msg] => msg"
+ --{*Extra Encryption*}
+ (*K: the symmetric key EK: the public encryption key*)
+ "EXcrypt K EK M m ==
+ {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
+
+ EXHcrypt :: "[key,key,msg,msg] => msg"
+ --{*Extra Encryption with Hashing*}
+ (*K: the symmetric key EK: the public encryption key*)
+ "EXHcrypt K EK M m ==
+ {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
+
+ Enc :: "[key,key,key,msg] => msg"
+ --{*Simple Encapsulation with SIGNATURE*}
+ (*SK: the sender's signing key
+ K: the symmetric key
+ EK: the public encryption key*)
+ "Enc SK K EK M ==
+ {|Crypt K (sign SK M), Crypt EK (Key K)|}"
+
+ EncB :: "[key,key,key,msg,msg] => msg"
+ --{*Encapsulation with Baggage. Keys as above, and baggage b.*}
+ "EncB SK K EK M b ==
+ {|Enc SK K EK {|M, Hash b|}, b|}"
+
+
+subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
+
+lemma publicKey_eq_iff [iff]:
+ "(publicKey b A = publicKey b' A') = (b=b' & A=A')"
+by (blast dest: injective_publicKey)
+
+lemma privateKey_eq_iff [iff]:
+ "(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' & A=A')"
+by auto
+
+lemma not_symKeys_publicKey [iff]: "publicKey b A \<notin> symKeys"
+by (simp add: symKeys_def)
+
+lemma not_symKeys_privateKey [iff]: "invKey (publicKey b A) \<notin> symKeys"
+by (simp add: symKeys_def)
+
+lemma symKeys_invKey_eq [simp]: "K \<in> symKeys ==> invKey K = K"
+by (simp add: symKeys_def)
+
+lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
+by (unfold symKeys_def, auto)
+
+text{*Can be slow (or even loop) as a simprule*}
+lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
+by blast
+
+text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
+in practice.*}
+lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
+by blast
+
+lemma symKey_neq_publicKey: "K \<in> symKeys ==> K \<noteq> publicKey b A"
+by blast
+
+lemma privateKey_neq_symKey: "K \<in> symKeys ==> invKey (publicKey b A) \<noteq> K"
+by blast
+
+lemma symKey_neq_privateKey: "K \<in> symKeys ==> K \<noteq> invKey (publicKey b A)"
+by blast
+
+lemma analz_symKeys_Decrypt:
+ "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
+ ==> X \<in> analz H"
+by auto
+
+
+subsection{*"Image" Equations That Hold for Injective Functions *}
+
+lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
+by auto
+
+text{*holds because invKey is injective*}
+lemma publicKey_image_eq [iff]:
+ "(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
+by auto
+
+lemma privateKey_image_eq [iff]:
+ "(invKey (publicKey b A) \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
+by auto
+
+lemma privateKey_notin_image_publicKey [iff]:
+ "invKey (publicKey b A) \<notin> publicKey c ` AS"
+by auto
+
+lemma publicKey_notin_image_privateKey [iff]:
+ "publicKey b A \<notin> invKey ` publicKey c ` AS"
+by auto
+
+lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
+apply (simp add: keysFor_def)
+apply (induct_tac "C")
+apply (auto intro: range_eqI)
+done
+
+text{*for proving @{text new_keys_not_used}*}
+lemma keysFor_parts_insert:
+ "[| K \<in> keysFor (parts (insert X H)); X \<in> synth (analz H) |]
+ ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
+apply (force dest!:
+ parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
+ analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
+ intro: analz_into_parts)
+done
+
+lemma Crypt_imp_keysFor [intro]:
+ "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
+by (drule Crypt_imp_invKey_keysFor, simp)
+
+text{*Agents see their own private keys!*}
+lemma privateKey_in_initStateCA [iff]:
+ "Key (invKey (publicKey b A)) \<in> initState A"
+by (case_tac "A", auto)
+
+text{*Agents see their own public keys!*}
+lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
+by (case_tac "A", auto)
+
+text{*RCA sees CAs' public keys! *}
+lemma pubK_CA_in_initState_RCA [iff]:
+ "Key (publicKey b (CA i)) \<in> initState RCA"
+by auto
+
+
+text{*Spy knows all public keys*}
+lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
+apply (induct_tac "evs")
+apply (simp_all add: imageI knows_Cons split add: event.split)
+done
+
+declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
+ (*needed????*)
+
+text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
+lemma knows_Spy_bad_privateKey [intro!]:
+ "A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
+apply (rule initState_subset_knows [THEN subsetD], simp)
+done
+
+
+subsection{*Fresh Nonces for Possibility Theorems*}
+
+lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
+by (induct_tac "B", auto)
+
+lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
+by (simp add: used_Nil)
+
+text{*In any trace, there is an upper bound N on the greatest nonce in use.*}
+lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
+apply (induct_tac "evs")
+apply (rule_tac x = 0 in exI)
+apply (simp_all add: used_Cons split add: event.split, safe)
+apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
+done
+
+lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
+by (rule Nonce_supply_lemma [THEN exE], blast)
+
+lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
+apply (rule Nonce_supply_lemma [THEN exE])
+apply (rule someI, fast)
+done
+
+
+subsection{*Fresh Numbers for Possibility Theorems*}
+
+lemma Number_notin_initState [iff]: "Number N \<notin> parts (initState B)"
+by (induct_tac "B", auto)
+
+lemma Number_notin_used_empty [simp]: "Number N \<notin> used []"
+by (simp add: used_Nil)
+
+text{*In any trace, there is an upper bound N on the greatest number in use.*}
+lemma Number_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Number n \<notin> used evs"
+apply (induct_tac "evs")
+apply (rule_tac x = 0 in exI)
+apply (simp_all add: used_Cons split add: event.split, safe)
+apply (rule msg_Number_supply [THEN exE], blast elim!: add_leE)+
+done
+
+lemma Number_supply1: "\<exists>N. Number N \<notin> used evs"
+by (rule Number_supply_lemma [THEN exE], blast)
+
+lemma Number_supply: "Number (@ N. Number N \<notin> used evs) \<notin> used evs"
+apply (rule Number_supply_lemma [THEN exE])
+apply (rule someI, fast)
+done
+
+
+subsection{*Fresh Keys for Possibility Theorems*}
+
+lemma Key_supply1: "\<exists>K. Key K \<notin> used evs & K \<in> symKeys"
+by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
+
+lemma Key_supply:
+ "(@K. K \<in> symKeys & Key K \<notin> used evs) \<in> symKeys &
+ Key (@K. K \<in> symKeys & Key K \<notin> used evs) \<notin> used evs"
+apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
+apply (rule someI, blast)
+done
+
+
+subsection{*Specialized Methods for Possibility Theorems*}
+
+ML
+{*
+val Nonce_supply1 = thm "Nonce_supply1";
+val Nonce_supply = thm "Nonce_supply";
+val Key_supply = thm "Key_supply";
+val Number_supply = thm "Number_supply";
+
+val used_Says = thm "used_Says";
+val used_Notes = thm "used_Notes";
+
+(*Tactic for possibility theorems (Isar interface)*)
+fun gen_possibility_tac ss state = state |>
+ REPEAT (*omit used_Says so that Nonces start from different traces!*)
+ (ALLGOALS (simp_tac (ss delsimps [used_Says,used_Notes]))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE'
+ resolve_tac [refl, conjI, Nonce_supply, Number_supply,
+ Key_supply RS conjunct1,
+ Key_supply RS conjunct2]))
+
+(*Tactic for possibility theorems (ML script version)*)
+fun possibility_tac state = gen_possibility_tac (simpset()) state
+
+(*For harder protocols (such as SET_CR!), where we have to set up some
+ nonces and keys initially*)
+fun basic_possibility_tac st = st |>
+ REPEAT
+ (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ THEN
+ REPEAT_FIRST (resolve_tac [refl, conjI]))
+*}
+
+method_setup possibility = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
+ "for proving possibility theorems"
+
+
+
+subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
+
+lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
+by blast
+
+lemma insert_Key_image:
+ "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
+by blast
+
+text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
+lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
+by auto
+
+lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
+by (blast intro!: initState_into_used)
+
+text{*Reverse the normal simplification of "image" to build up (not break down)
+ the set of keys. Based on @{text analz_image_freshK_ss}, but simpler.*}
+lemmas analz_image_keys_simps =
+ simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+ image_insert [THEN sym] image_Un [THEN sym]
+ rangeI symKeys_neq_imp_neq
+ insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
+
+
+(*General lemmas proved by Larry*)
+
+subsection{*Controlled Unfolding of Abbreviations*}
+
+text{*A set is expanded only if a relation is applied to it*}
+lemma def_abbrev_simp_relation:
+ "A == B ==> (A \<in> X) = (B \<in> X) &
+ (u = A) = (u = B) &
+ (A = u) = (B = u)"
+by auto
+
+text{*A set is expanded only if one of the given functions is applied to it*}
+lemma def_abbrev_simp_function:
+ "A == B
+ ==> parts (insert A X) = parts (insert B X) &
+ analz (insert A X) = analz (insert B X) &
+ keysFor (insert A X) = keysFor (insert B X)"
+by auto
+
+subsubsection{*Special Simplification Rules for @{term signCert}*}
+
+text{*Avoids duplicating X and its components!*}
+lemma parts_insert_signCert:
+ "parts (insert (signCert K X) H) =
+ insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"
+by (simp add: signCert_def insert_commute [of X])
+
+text{*Avoids a case split! [X is always available]*}
+lemma analz_insert_signCert:
+ "analz (insert (signCert K X) H) =
+ insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"
+by (simp add: signCert_def insert_commute [of X])
+
+lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
+by (simp add: signCert_def)
+
+text{*Controlled rewrite rules for @{term signCert}, just the definitions
+ of the others. Encryption primitives are just expanded, despite their huge
+ redundancy!*}
+lemmas abbrev_simps [simp] =
+ parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
+ sign_def [THEN def_abbrev_simp_relation]
+ sign_def [THEN def_abbrev_simp_function]
+ signCert_def [THEN def_abbrev_simp_relation]
+ signCert_def [THEN def_abbrev_simp_function]
+ certC_def [THEN def_abbrev_simp_relation]
+ certC_def [THEN def_abbrev_simp_function]
+ cert_def [THEN def_abbrev_simp_relation]
+ cert_def [THEN def_abbrev_simp_function]
+ EXcrypt_def [THEN def_abbrev_simp_relation]
+ EXcrypt_def [THEN def_abbrev_simp_function]
+ EXHcrypt_def [THEN def_abbrev_simp_relation]
+ EXHcrypt_def [THEN def_abbrev_simp_function]
+ Enc_def [THEN def_abbrev_simp_relation]
+ Enc_def [THEN def_abbrev_simp_function]
+ EncB_def [THEN def_abbrev_simp_relation]
+ EncB_def [THEN def_abbrev_simp_function]
+
+
+subsubsection{*Elimination Rules for Controlled Rewriting *}
+
+lemma Enc_partsE:
+ "!!R. [|Enc SK K EK M \<in> parts H;
+ [|Crypt K (sign SK M) \<in> parts H;
+ Crypt EK (Key K) \<in> parts H|] ==> R|]
+ ==> R"
+
+by (unfold Enc_def, blast)
+
+lemma EncB_partsE:
+ "!!R. [|EncB SK K EK M b \<in> parts H;
+ [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;
+ Crypt EK (Key K) \<in> parts H;
+ b \<in> parts H|] ==> R|]
+ ==> R"
+by (unfold EncB_def Enc_def, blast)
+
+lemma EXcrypt_partsE:
+ "!!R. [|EXcrypt K EK M m \<in> parts H;
+ [|Crypt K {|M, Hash m|} \<in> parts H;
+ Crypt EK {|Key K, m|} \<in> parts H|] ==> R|]
+ ==> R"
+by (unfold EXcrypt_def, blast)
+
+
+subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
+
+lemma analz_knows_absorb:
+ "Key K \<in> analz (knows Spy evs)
+ ==> analz (Key ` (insert K H) \<union> knows Spy evs) =
+ analz (Key ` H \<union> knows Spy evs)"
+by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
+
+lemma analz_knows_absorb2:
+ "Key K \<in> analz (knows Spy evs)
+ ==> analz (Key ` (insert X (insert K H)) \<union> knows Spy evs) =
+ analz (Key ` (insert X H) \<union> knows Spy evs)"
+apply (subst insert_commute)
+apply (erule analz_knows_absorb)
+done
+
+lemma analz_insert_subset_eq:
+ "[|X \<in> analz (knows Spy evs); knows Spy evs \<subseteq> H|]
+ ==> analz (insert X H) = analz H"
+apply (rule analz_insert_eq)
+apply (blast intro: analz_mono [THEN [2] rev_subsetD])
+done
+
+lemmas analz_insert_simps =
+ analz_insert_subset_eq Un_upper2
+ subset_insertI [THEN [2] subset_trans]
+
+
+subsection{*Freshness Lemmas*}
+
+lemma in_parts_Says_imp_used:
+ "[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
+by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
+
+text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
+lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
+by auto
+
+lemma fresh_notin_analz_knows_Spy:
+ "Key K \<notin> used evs ==> Key K \<notin> analz (knows Spy evs)"
+by (auto dest: analz_into_parts)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/Purchase.thy Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,1140 @@
+(* Title: HOL/Auth/SET/Purchase
+ ID: $Id$
+ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
+*)
+
+header{*Purchase Phase of SET*}
+
+theory Purchase = PublicSET:
+
+text{*
+Note: nonces seem to consist of 20 bytes. That includes both freshness
+challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
+
+This version omits @{text LID_C} but retains @{text LID_M}. At first glance
+(Programmer's Guide page 267) it seems that both numbers are just introduced
+for the respective convenience of the Cardholder's and Merchant's
+system. However, omitting both of them would create a problem of
+identification: how can the Merchant's system know what transaction is it
+supposed to process?
+
+Further reading (Programmer's guide page 309) suggest that there is an outside
+bootstrapping message (SET initiation message) which is used by the Merchant
+and the Cardholder to agree on the actual transaction. This bootstrapping
+message is described in the SET External Interface Guide and ought to generate
+@{text LID_M}. According SET Extern Interface Guide, this number might be a
+cookie, an invoice number etc. The Programmer's Guide on page 310, states that
+in absence of @{text LID_M} the protocol must somehow ("outside SET") identify
+the transaction from OrderDesc, which is assumed to be a searchable text only
+field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed
+out-of-bad on the value of @{text LID_M} (for instance a cookie in a web
+transaction etc.). This out-of-band agreement is expressed with a preliminary
+start action in which the merchant and the Cardholder agree on the appropriate
+values. Agreed values are stored with a suitable notes action.
+
+"XID is a transaction ID that is usually generated by the Merchant system,
+unless there is no PInitRes, in which case it is generated by the Cardholder
+system. It is a randomly generated 20 byte variable that is globally unique
+(statistically). Merchant and Cardholder systems shall use appropriate random
+number generators to ensure the global uniqueness of XID."
+--Programmer's Guide, page 267.
+
+PI (Payment Instruction) is the most central and sensitive data structure in
+SET. It is used to pass the data required to authorize a payment card payment
+from the Cardholder to the Payment Gateway, which will use the data to
+initiate a payment card transaction through the traditional payment card
+financial network. The data is encrypted by the Cardholder and sent via the
+Merchant, such that the data is hidden from the Merchant unless the Acquirer
+passes the data back to the Merchant.
+--Programmer's Guide, page 271.*}
+
+consts
+
+ CardSecret :: "nat => nat"
+ (*Maps Cardholders to CardSecrets.
+ A CardSecret of 0 means no cerificate, must use unsigned format.*)
+
+ PANSecret :: "nat => nat"
+ (*Maps Cardholders to PANSecrets.*)
+
+ set_pur :: "event list set"
+
+inductive set_pur
+ intros
+
+ Nil: --{*Initial trace is empty*}
+ "[] \<in> set_pur"
+
+ Fake: --{*The spy MAY say anything he CAN say.*}
+ "[| evsf \<in> set_pur; X \<in> synth(analz(knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> set_pur"
+
+
+ Reception: --{*If A sends a message X to B, then B might receive it*}
+ "[| evsr \<in> set_pur; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> set_pur"
+
+ Start:
+ --{*Added start event which is out-of-band for SET: the Cardholder and
+ the merchant agree on the amounts and uses @{text LID_M} as an
+ identifier.
+ This is suggested by the External Interface Guide. The Programmer's
+ Guide, in absence of @{text LID_M}, states that the merchant uniquely
+ identifies the order out of some data contained in OrderDesc.*}
+ "[|evsStart \<in> set_pur;
+ Number LID_M \<notin> used evsStart;
+ C = Cardholder k; M = Merchant i; P = PG j;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ LID_M \<notin> range CardSecret;
+ LID_M \<notin> range PANSecret |]
+ ==> Notes C {|Number LID_M, Transaction|}
+ # Notes M {|Number LID_M, Agent P, Transaction|}
+ # evsStart \<in> set_pur"
+
+ PInitReq:
+ --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
+ "[|evsPIReq \<in> set_pur;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ Nonce Chall_C \<notin> used evsPIReq;
+ Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;
+ Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
+ ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
+
+ PInitRes:
+ --{*Merchant replies with his own label XID and the encryption
+ key certificate of his chosen Payment Gateway. Page 74 of Formal
+ Protocol Desc. We use @{text LID_M} to identify Cardholder*}
+ "[|evsPIRes \<in> set_pur;
+ Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;
+ Nonce Chall_M \<notin> used evsPIRes;
+ Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;
+ Number XID \<notin> used evsPIRes;
+ XID \<notin> range CardSecret; XID \<notin> range PANSecret|]
+ ==> Says M C (sign (priSK M)
+ {|Number LID_M, Number XID,
+ Nonce Chall_C, Nonce Chall_M,
+ cert P (pubEK P) onlyEnc (priSK RCA)|})
+ # evsPIRes \<in> set_pur"
+
+ PReqUns:
+ --{*UNSIGNED Purchase request (CardSecret = 0).
+ Page 79 of Formal Protocol Desc.
+ Merchant never sees the amount in clear. This holds of the real
+ protocol, where XID identifies the transaction. We omit
+ Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
+ the CardSecret is 0 and because AuthReq treated the unsigned case
+ very differently from the signed one anyway.*}
+ "[|evsPReqU \<in> set_pur;
+ C = Cardholder k; CardSecret k = 0;
+ Key KC1 \<notin> used evsPReqU; KC1 \<in> symKeys;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ HOD = Hash{|Number OrderDesc, Number PurchAmt|};
+ OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
+ Gets C (sign (priSK M)
+ {|Number LID_M, Number XID,
+ Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)|})
+ \<in> set evsPReqU;
+ Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;
+ Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]
+ ==> Says C M
+ {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
+ OIData, Hash{|PIHead, Pan (pan C)|} |}
+ # Notes C {|Key KC1, Agent M|}
+ # evsPReqU \<in> set_pur"
+
+ PReqS:
+ --{*SIGNED Purchase request. Page 77 of Formal Protocol Desc.
+ We could specify the equation
+ @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
+ Formal Desc. gives PIHead the same format in the unsigned case.
+ However, there's little point, as P treats the signed and
+ unsigned cases differently.*}
+ "[|evsPReqS \<in> set_pur;
+ C = Cardholder k;
+ CardSecret k \<noteq> 0; Key KC2 \<notin> used evsPReqS; KC2 \<in> symKeys;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ HOD = Hash{|Number OrderDesc, Number PurchAmt|};
+ OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ Hash{|Number XID, Nonce (CardSecret k)|}|};
+ PANData = {|Pan (pan C), Nonce (PANSecret k)|};
+ PIData = {|PIHead, PANData|};
+ PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},
+ EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};
+ OIDualSigned = {|OIData, Hash PIData|};
+ Gets C (sign (priSK M)
+ {|Number LID_M, Number XID,
+ Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)|})
+ \<in> set evsPReqS;
+ Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;
+ Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]
+ ==> Says C M {|PIDualSigned, OIDualSigned|}
+ # Notes C {|Key KC2, Agent M|}
+ # evsPReqS \<in> set_pur"
+
+ --{*Authorization Request. Page 92 of Formal Protocol Desc.
+ Sent in response to Purchase Request.*}
+ AuthReq:
+ "[| evsAReq \<in> set_pur;
+ Key KM \<notin> used evsAReq; KM \<in> symKeys;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ HOD = Hash{|Number OrderDesc, Number PurchAmt|};
+ OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,
+ Nonce Chall_M|};
+ CardSecret k \<noteq> 0 -->
+ P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
+ Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;
+ Says M C (sign (priSK M) {|Number LID_M, Number XID,
+ Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)|})
+ \<in> set evsAReq;
+ Notes M {|Number LID_M, Agent P, Transaction|}
+ \<in> set evsAReq |]
+ ==> Says M P
+ (EncB (priSK M) KM (pubEK P)
+ {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
+ # evsAReq \<in> set_pur"
+
+ --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
+ Page 99 of Formal Protocol Desc.
+ PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and
+ HOIData occur independently in @{text P_I} and in M's message.
+ The authCode in AuthRes represents the baggage of EncB, which in the
+ full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
+ optional items for split shipments, recurring payments, etc.*}
+
+ AuthResUns:
+ --{*Authorization Response, UNSIGNED*}
+ "[| evsAResU \<in> set_pur;
+ C = Cardholder k; M = Merchant i;
+ Key KP \<notin> used evsAResU; KP \<in> symKeys;
+ CardSecret k = 0; KC1 \<in> symKeys; KM \<in> symKeys;
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
+ P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));
+ Gets P (EncB (priSK M) KM (pubEK P)
+ {|Number LID_M, Number XID, HOIData, HOD|} P_I)
+ \<in> set evsAResU |]
+ ==> Says P M
+ (EncB (priSK P) KP (pubEK M)
+ {|Number LID_M, Number XID, Number PurchAmt|}
+ authCode)
+ # evsAResU \<in> set_pur"
+
+ AuthResS:
+ --{*Authorization Response, SIGNED*}
+ "[| evsAResS \<in> set_pur;
+ C = Cardholder k;
+ Key KP \<notin> used evsAResS; KP \<in> symKeys;
+ CardSecret k \<noteq> 0; KC2 \<in> symKeys; KM \<in> symKeys;
+ P_I = {|sign (priSK C) {|Hash PIData, HOIData|},
+ EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};
+ PANData = {|Pan (pan C), Nonce (PANSecret k)|};
+ PIData = {|PIHead, PANData|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ Hash{|Number XID, Nonce (CardSecret k)|}|};
+ Gets P (EncB (priSK M) KM (pubEK P)
+ {|Number LID_M, Number XID, HOIData, HOD|}
+ P_I)
+ \<in> set evsAResS |]
+ ==> Says P M
+ (EncB (priSK P) KP (pubEK M)
+ {|Number LID_M, Number XID, Number PurchAmt|}
+ authCode)
+ # evsAResS \<in> set_pur"
+
+ PRes:
+ --{*Purchase response.*}
+ "[| evsPRes \<in> set_pur; KP \<in> symKeys; M = Merchant i;
+ Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+ Gets M (EncB (priSK P) KP (pubEK M)
+ {|Number LID_M, Number XID, Number PurchAmt|}
+ authCode)
+ \<in> set evsPRes;
+ Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
+ Says M P
+ (EncB (priSK M) KM (pubEK P)
+ {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
+ \<in> set evsPRes;
+ Notes M {|Number LID_M, Agent P, Transaction|}
+ \<in> set evsPRes
+ |]
+ ==> Says M C
+ (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)|})
+ # evsPRes \<in> set_pur"
+
+
+specification (CardSecret PANSecret)
+ inj_CardSecret: "inj CardSecret"
+ inj_PANSecret: "inj PANSecret"
+ CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
+ --{*No CardSecret equals any PANSecret*}
+ apply (rule_tac x="curry nat2_to_nat 0" in exI)
+ apply (rule_tac x="curry nat2_to_nat 1" in exI)
+ apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
+ done
+
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+declare CardSecret_neq_PANSecret [iff]
+ CardSecret_neq_PANSecret [THEN not_sym, iff]
+declare inj_CardSecret [THEN inj_eq, iff]
+ inj_PANSecret [THEN inj_eq, iff]
+
+
+subsection{*Possibility Properties*}
+
+lemma Says_to_Gets:
+ "Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"
+by (rule set_pur.Reception, auto)
+
+(* Possibility for UNSIGNED purchases*)
+lemma possibility_Uns:
+ "[| CardSecret k = 0;
+ \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
+ \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
+ \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
+ \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
+ |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
+ \<exists>evs \<in> set_pur.
+ Says (Merchant i) (Cardholder k)
+ (sign (priSK (Merchant i))
+ {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2]
+ set_pur.Nil [THEN set_pur.Start,
+ THEN set_pur.PInitReq, THEN Says_to_Gets,
+ THEN set_pur.PInitRes, THEN Says_to_Gets,
+ THEN set_pur.PReqUns, THEN Says_to_Gets,
+ THEN set_pur.AuthReq, THEN Says_to_Gets,
+ THEN set_pur.AuthResUns, THEN Says_to_Gets,
+ THEN set_pur.PRes])
+apply (possibility, erule spec)+
+done
+
+lemma possibility_S:
+ "[| CardSecret k \<noteq> 0;
+ \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
+ \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
+ \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
+ \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
+ |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
+ \<exists>evs \<in> set_pur.
+ Says (Merchant i) (Cardholder k)
+ (sign (priSK (Merchant i))
+ {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2]
+ set_pur.Nil [THEN set_pur.Start,
+ THEN set_pur.PInitReq, THEN Says_to_Gets,
+ THEN set_pur.PInitRes, THEN Says_to_Gets,
+ THEN set_pur.PReqS, THEN Says_to_Gets,
+ THEN set_pur.AuthReq, THEN Says_to_Gets,
+ THEN set_pur.AuthResS, THEN Says_to_Gets,
+ THEN set_pur.PRes])
+apply possibility --{*39 seconds on a 1.8GHz machine*}
+apply ((erule spec)+, auto)
+done
+
+(*General facts about message reception*)
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> set_pur |]
+ ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule set_pur.induct, auto)
+done
+
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> set_pur |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
+
+text{*Forwarding lemmas, to aid simplification*}
+
+lemma AuthReq_msg_in_parts_spies:
+ "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
+ evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"
+by auto
+
+lemma AuthReq_msg_in_analz_spies:
+ "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
+ evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
+by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
+
+
+subsection{*Proofs on Asymmetric Keys*}
+
+text{*Private Keys are Secret*}
+
+text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
+lemma Spy_see_private_Key [simp]:
+ "evs \<in> set_pur
+ ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply auto
+done
+declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
+
+lemma Spy_analz_private_Key [simp]:
+ "evs \<in> set_pur ==>
+ (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
+by auto
+declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
+
+text{*rewriting rule for priEK's*}
+lemma parts_image_priEK:
+ "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
+ evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"
+by auto
+
+text{*trivial proof because (priEK C) never appears even in (parts evs)*}
+lemma analz_image_priEK:
+ "evs \<in> set_pur ==>
+ (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
+ (priEK C \<in> KK | C \<in> bad)"
+by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
+
+subsection{*Public Keys in Certificates are Correct*}
+
+lemma Crypt_valid_pubEK [dest!]:
+ "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_pur |] ==> EKi = pubEK C"
+apply (erule rev_mp)
+apply (erule set_pur.induct, auto)
+done
+
+lemma Crypt_valid_pubSK [dest!]:
+ "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+ \<in> parts (knows Spy evs);
+ evs \<in> set_pur |] ==> SKi = pubSK C"
+apply (erule rev_mp)
+apply (erule set_pur.induct, auto)
+done
+
+lemma certificate_valid_pubEK:
+ "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_pur |]
+ ==> EKi = pubEK C"
+by (unfold cert_def signCert_def, auto)
+
+lemma certificate_valid_pubSK:
+ "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
+ evs \<in> set_pur |] ==> SKi = pubSK C"
+by (unfold cert_def signCert_def, auto)
+
+lemma Says_certificate_valid [simp]:
+ "[| Says A B (sign SK {|lid, xid, cc, cm,
+ cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
+ evs \<in> set_pur |]
+ ==> EK = pubEK C"
+by (unfold sign_def, auto)
+
+lemma Gets_certificate_valid [simp]:
+ "[| Gets A (sign SK {|lid, xid, cc, cm,
+ cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
+ evs \<in> set_pur |]
+ ==> EK = pubEK C"
+by (frule Gets_imp_Says, auto)
+
+ML
+{*
+val Gets_certificate_valid = thm "Gets_certificate_valid";
+
+fun valid_certificate_tac i =
+ EVERY [ftac Gets_certificate_valid i,
+ assume_tac i, REPEAT (hyp_subst_tac i)];
+*}
+
+
+subsection{*Proofs on Symmetric Keys*}
+
+text{*Nobody can have used non-existent keys!*}
+lemma new_keys_not_used [rule_format,simp]:
+ "evs \<in> set_pur
+ ==> Key K \<notin> used evs --> K \<in> symKeys -->
+ K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule set_pur.induct)
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply auto
+apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
+done
+
+lemma new_keys_not_analzd:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
+ ==> K \<notin> keysFor (analz (knows Spy evs))"
+by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used)
+
+lemma Crypt_parts_imp_used:
+ "[|Crypt K X \<in> parts (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
+apply (rule ccontr)
+apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
+done
+
+lemma Crypt_analz_imp_used:
+ "[|Crypt K X \<in> analz (knows Spy evs);
+ K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
+by (blast intro: Crypt_parts_imp_used)
+
+text{*New versions: as above, but generalized to have the KK argument*}
+
+lemma gen_new_keys_not_used:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
+ ==> Key K \<notin> used evs --> K \<in> symKeys -->
+ K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
+by auto
+
+lemma gen_new_keys_not_analzd:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
+ ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
+by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used)
+
+lemma analz_Key_image_insert_eq:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
+ ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
+ insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
+by (simp add: gen_new_keys_not_analzd)
+
+
+subsection{*Secrecy of Symmetric Keys*}
+
+lemma Key_analz_image_Key_lemma:
+ "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
+ ==>
+ P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+
+lemma symKey_compromise:
+ "evs \<in> set_pur ==>
+ (\<forall>SK KK. SK \<in> symKeys \<longrightarrow>
+ (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
+ (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
+ (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
+apply (erule set_pur.induct)
+apply (rule_tac [!] allI)+
+apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
+apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps disj_simps
+ analz_Key_image_insert_eq notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*35 seconds on a 1.8GHz machine*}
+apply spy_analz --{*Fake*}
+apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}
+done
+
+
+
+subsection{*Secrecy of Nonces*}
+
+text{*As usual: we express the property as a logical equivalence*}
+lemma Nonce_analz_image_Key_lemma:
+ "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
+ ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+text{*The @{text "(no_asm)"} attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.*}
+lemma Nonce_compromise [rule_format (no_asm)]:
+ "evs \<in> set_pur ==>
+ (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
+ (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
+ (Nonce N \<in> analz (knows Spy evs)))"
+apply (erule set_pur.induct)
+apply (rule_tac [!] allI)+
+apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
+apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps disj_simps symKey_compromise
+ analz_Key_image_insert_eq notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*35 seconds on a 1.8GHz machine*}
+apply spy_analz --{*Fake*}
+apply (blast elim!: ballE) --{*PReqS*}
+done
+
+lemma PANSecret_notin_spies:
+ "evs \<in> set_pur
+ ==> Nonce (PANSecret k) \<in> analz (knows Spy evs) -->
+ (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
+ Says (Cardholder k) M
+ {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
+ V|} \<in> set evs)"
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_analz_spies)
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps disj_simps
+ symKey_compromise pushes sign_def Nonce_compromise
+ analz_Key_image_insert_eq notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*13 seconds on a 1.8GHz machine*}
+apply spy_analz
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj]
+ Gets_imp_knows_Spy [THEN analz.Inj])
+apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*}
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj]
+ Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*}
+done
+
+text{*This theorem is a bit silly, in that many CardSecrets are 0!
+ But then we don't care. NOT USED*}
+lemma CardSecret_notin_spies:
+ "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"
+by (erule set_pur.induct, auto)
+
+subsection{*Confidentiality of PAN*}
+
+lemma analz_image_pan_lemma:
+ "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H) ==>
+ (Pan P \<in> analz (Key`nE Un H)) = (Pan P \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+text{*The @{text "(no_asm)"} attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.*}
+lemma analz_image_pan [rule_format (no_asm)]:
+ "evs \<in> set_pur ==>
+ \<forall>KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
+ (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
+ (Pan P \<in> analz (knows Spy evs))"
+apply (erule set_pur.induct)
+apply (rule_tac [!] allI impI)+
+apply (rule_tac [!] analz_image_pan_lemma)+
+apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps
+ symKey_compromise pushes sign_def
+ analz_Key_image_insert_eq notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*32 seconds on a 1.8GHz machine*}
+apply spy_analz --{*Fake*}
+apply auto
+done
+
+lemma analz_insert_pan:
+ "[| evs \<in> set_pur; K \<notin> range(\<lambda>C. priEK C) |] ==>
+ (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
+ (Pan P \<in> analz (knows Spy evs))"
+by (simp del: image_insert image_Un
+ add: analz_image_keys_simps analz_image_pan)
+
+text{*Confidentiality of the PAN, unsigned case.*}
+lemma pan_confidentiality_unsigned:
+ "[| Pan (pan C) \<in> analz(knows Spy evs); C = Cardholder k;
+ CardSecret k = 0; evs \<in> set_pur|]
+ ==> \<exists>P M KC1 K X Y.
+ Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
+ \<in> set evs &
+ P \<in> bad"
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_insert_pan analz_image_pan
+ notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*15 seconds on a 1.8GHz machine*}
+apply spy_analz --{*Fake*}
+apply blast --{*PReqUns: unsigned*}
+apply force --{*PReqS: signed*}
+done
+
+text{*Confidentiality of the PAN, signed case.*}
+lemma pan_confidentiality_signed:
+ "[| Pan (pan C) \<in> analz(knows Spy evs); C = Cardholder k;
+ CardSecret k \<noteq> 0; evs \<in> set_pur|]
+ ==> \<exists>B M KC2 K ps X Y Z.
+ Says C M {|{|X, EXcrypt KC2 (pubEK B) Y {|Pan (pan C), ps|}|}, Z|}
+ \<in> set evs &
+ B \<in> bad"
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
+apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (simp_all
+ del: image_insert image_Un imp_disjL
+ add: analz_image_keys_simps analz_insert_pan analz_image_pan
+ notin_image_iff
+ analz_insert_simps analz_image_priEK)
+ --{*17 seconds on a 1.8GHz machine*}
+apply spy_analz --{*Fake*}
+apply force --{*PReqUns: unsigned*}
+apply blast --{*PReqS: signed*}
+done
+
+text{*General goal: that C, M and PG agree on those details of the transaction
+ that they are allowed to know about. PG knows about price and account
+ details. M knows about the order description and price. C knows both.*}
+
+
+subsection{*Proofs Common to Signed and Unsigned Versions*}
+
+lemma M_Notes_PG:
+ "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;
+ evs \<in> set_pur|] ==> \<exists>j. P = PG j"
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+done
+
+text{*If we trust M, then @{term LID_M} determines his choice of P
+ (Payment Gateway)*}
+lemma goodM_gives_correct_PG:
+ "[| MsgPInitRes =
+ {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
+ Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
+ evs \<in> set_pur; M \<notin> bad |]
+ ==> \<exists>j trans.
+ P = PG j &
+ Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply (blast intro: M_Notes_PG)+
+done
+
+lemma C_gets_correct_PG:
+ "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,
+ cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>j trans.
+ P = PG j &
+ Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+ EKj = pubEK P"
+by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)
+
+text{*When C receives PInitRes, he learns M's choice of P*}
+lemma C_verifies_PInitRes:
+ "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)|};
+ Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>j trans.
+ Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+ P = PG j &
+ EKj = pubEK P"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply (blast intro: M_Notes_PG)+
+done
+
+text{*Corollary of previous one*}
+lemma Says_C_PInitRes:
+ "[|Says A C (sign (priSK M)
+ {|Number LID_M, Number XID,
+ Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)|})
+ \<in> set evs; M \<notin> bad; evs \<in> set_pur|]
+ ==> \<exists>j trans.
+ Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+ P = PG j &
+ EKj = pubEK (PG j)"
+apply (frule Says_certificate_valid)
+apply (auto simp add: sign_def)
+apply (blast dest: refl [THEN goodM_gives_correct_PG])
+apply (blast dest: refl [THEN C_verifies_PInitRes])
+done
+
+text{*When P receives an AuthReq, he knows that the signed part originated
+ with M. PIRes also has a signed message from M....*}
+lemma P_verifies_AuthReq:
+ "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
+ Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})
+ \<in> parts (knows Spy evs);
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>j trans KM OIData HPIData.
+ Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
+ Gets M {|P_I, OIData, HPIData|} \<in> set evs &
+ Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+apply (frule_tac [4] M_Notes_PG, auto)
+done
+
+text{*When M receives AuthRes, he knows that P signed it, including
+ the identifying tages and the purchase amount, which he can verify.
+ (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
+ send the same message to M.)*}
+lemma M_verifies_AuthRes:
+ "[| MsgAuthRes = {|Number LID_M, Number XID, Number PurchAmt|};
+ Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
+ evs \<in> set_pur; PG j \<notin> bad|]
+ ==> \<exists>i KM HOIData HOD P_I.
+ Gets (PG j)
+ (EncB (priSK (Merchant i)) KM (pubEK (PG j))
+ {|Number LID_M, Number XID, HOIData, HOD|}
+ P_I) \<in> set evs &
+ Says (PG j) (Merchant i)
+ (Crypt (pubEK (Merchant i)) (sign (priSK (PG j)) MsgAuthRes))
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply blast+
+done
+
+
+subsection{*Proofs for Unsigned Purchases*}
+
+text{*What we can derive from the ASSUMPTION that C issued a purchase request.
+ In the unsigned case, we must trust "C": there's no authentication.*}
+lemma C_determines_EKj:
+ "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
+ OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;
+ PIHead = {|Number LID_M, Trans_details|};
+ evs \<in> set_pur; C = Cardholder k; M \<notin> bad|]
+ ==> \<exists>trans j.
+ Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
+ EKj = pubEK (PG j)"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+apply (tactic{*valid_certificate_tac 2*}) --{*PReqUns*}
+apply auto
+apply (blast dest: Gets_imp_Says Says_C_PInitRes)
+done
+
+
+text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}
+lemma unique_LID_M:
+ "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;
+ Notes C {|Number LID_M, Agent M, Agent C, Number OD,
+ Number PA|} \<in> set evs;
+ evs \<in> set_pur|]
+ ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+apply (force dest!: Notes_imp_parts_subset_used)
+done
+
+text{*Unicity of @{term LID_M}, for two Merchant Notes events*}
+lemma unique_LID_M2:
+ "[|Notes M {|Number LID_M, Trans|} \<in> set evs;
+ Notes M {|Number LID_M, Trans'|} \<in> set evs;
+ evs \<in> set_pur|] ==> Trans' = Trans"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+apply (force dest!: Notes_imp_parts_subset_used)
+done
+
+text{*Lemma needed below: for the case that
+ if PRes is present, then @{term LID_M} has been used.*}
+lemma signed_imp_used:
+ "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);
+ M \<notin> bad; evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply safe
+apply blast+
+done
+
+text{*Similar, with nested Hash*}
+lemma signed_Hash_imp_used:
+ "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
+ C \<notin> bad; evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply safe
+apply blast+
+done
+
+text{*Lemma needed below: for the case that
+ if PRes is present, then @{text LID_M} has been used.*}
+lemma PRes_imp_LID_used:
+ "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);
+ M \<notin> bad; evs \<in> set_pur|] ==> N \<in> used evs"
+by (drule signed_imp_used, auto)
+
+text{*When C receives PRes, he knows that M and P agreed to the purchase details.
+ He also knows that P is the same PG as before*}
+lemma C_verifies_PRes_lemma:
+ "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);
+ Notes C {|Number LID_M, Trans |} \<in> set evs;
+ Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
+ MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)|};
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>j KP.
+ Notes M {|Number LID_M, Agent (PG j), Trans |}
+ \<in> set evs &
+ Gets M (EncB (priSK (PG j)) KP (pubEK M)
+ {|Number LID_M, Number XID, Number PurchAmt|}
+ authCode)
+ \<in> set evs &
+ Says M C (sign (priSK M) MsgPRes) \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply blast
+apply blast
+apply (blast dest: PRes_imp_LID_used)
+apply (frule M_Notes_PG, auto)
+apply (blast dest: unique_LID_M)
+done
+
+lemma C_verifies_PRes:
+ "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)|};
+ Gets C (sign (priSK M) MsgPRes) \<in> set evs;
+ Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
+ Number PurchAmt|} \<in> set evs;
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>P KP trans.
+ Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
+ Gets M (EncB (priSK P) KP (pubEK M)
+ {|Number LID_M, Number XID, Number PurchAmt|}
+ authCode)
+ \<in> set evs &
+ Says M C (sign (priSK M) MsgPRes) \<in> set evs"
+apply (rule C_verifies_PRes_lemma [THEN exE])
+apply (auto simp add: sign_def)
+done
+
+subsection{*Proofs for Signed Purchases*}
+
+text{*Some Useful Lemmas: the cardholder knows what he is doing*}
+
+lemma Crypt_imp_Says_Cardholder:
+ "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
+ \<in> parts (knows Spy evs);
+ PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
+ Key K \<notin> analz (knows Spy evs);
+ evs \<in> set_pur|]
+ ==> \<exists>M shash EK HPIData.
+ Says (Cardholder k) M {|{|shash,
+ Crypt K
+ {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
+ Crypt EK {|Key K, PANData|}|},
+ OIData, HPIData|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct, analz_mono_contra)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply auto
+done
+
+lemma Says_PReqS_imp_trans_details_C:
+ "[| MsgPReqS = {|{|shash,
+ Crypt K
+ {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
+ cryptek|}, data|};
+ Says (Cardholder k) M MsgPReqS \<in> set evs;
+ evs \<in> set_pur |]
+ ==> \<exists>trans.
+ Notes (Cardholder k)
+ {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (simp_all (no_asm_simp))
+apply auto
+done
+
+text{*Can't happen: only Merchants create this type of Note*}
+lemma Notes_Cardholder_self_False:
+ "[|Notes (Cardholder k)
+ {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;
+ evs \<in> set_pur|] ==> False"
+apply (erule rev_mp)
+apply (erule set_pur.induct, auto)
+done
+
+text{*When M sees a dual signature, he knows that it originated with C.
+ Using XID he knows it was intended for him.
+ This guarantee isn't useful to P, who never gets OIData.*}
+lemma M_verifies_Signed_PReq:
+ "[| MsgDualSign = {|HPIData, Hash OIData|};
+ OIData = {|Number LID_M, etc|};
+ Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
+ Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
+ M = Merchant i; C = Cardholder k; C \<notin> bad; evs \<in> set_pur|]
+ ==> \<exists>PIData PICrypt.
+ HPIData = Hash PIData &
+ Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct)
+apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
+apply simp_all
+apply blast
+apply (force dest!: signed_Hash_imp_used)
+apply (clarify) --{*speeds next step*}
+apply (blast dest: unique_LID_M)
+apply (blast dest!: Notes_Cardholder_self_False)
+done
+
+text{*When P sees a dual signature, he knows that it originated with C.
+ and was intended for M. This guarantee isn't useful to M, who never gets
+ PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
+ assuming @{term "M \<notin> bad"}.*}
+lemma P_verifies_Signed_PReq:
+ "[| MsgDualSign = {|Hash PIData, HOIData|};
+ PIData = {|PIHead, PANData|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain|};
+ Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
+ evs \<in> set_pur; C \<notin> bad; M \<notin> bad|]
+ ==> \<exists>OIData OrderDesc K j trans.
+ HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
+ HOIData = Hash OIData &
+ Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
+ Says C M {|{|sign (priSK C) MsgDualSign,
+ EXcrypt K (pubEK (PG j))
+ {|PIHead, Hash OIData|} PANData|},
+ OIData, Hash PIData|}
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all)
+apply (auto dest!: C_gets_correct_PG)
+done
+
+lemma C_determines_EKj_signed:
+ "[| Says C M {|{|sign (priSK C) text,
+ EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;
+ PIHead = {|Number LID_M, Number XID, W|};
+ C = Cardholder k; evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists> trans j.
+ Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
+ EKj = pubEK (PG j)"
+apply clarify
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all, auto)
+apply (blast dest: C_gets_correct_PG)
+done
+
+lemma M_Says_AuthReq:
+ "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
+ sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);
+ evs \<in> set_pur; M \<notin> bad|]
+ ==> \<exists>j trans KM.
+ Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
+ Says M (PG j)
+ (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
+ \<in> set evs"
+apply (rule refl [THEN P_verifies_AuthReq, THEN exE])
+apply (auto simp add: sign_def)
+done
+
+text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information.
+ Even here we cannot be certain about what C sent to M, since a bad
+ PG could have replaced the two key fields. (NOT USED)*}
+lemma Signed_PReq_imp_Says_Cardholder:
+ "[| MsgDualSign = {|Hash PIData, Hash OIData|};
+ OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain|};
+ PIData = {|PIHead, PANData|};
+ Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
+ M = Merchant i; C = Cardholder k; C \<notin> bad; evs \<in> set_pur|]
+ ==> \<exists>KC EKj.
+ Says C M {|{|sign (priSK C) MsgDualSign,
+ EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
+ OIData, Hash PIData|}
+ \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule set_pur.induct, simp_all, auto)
+done
+
+text{*When P receives an AuthReq and a dual signature, he knows that C and M
+ agree on the essential details. PurchAmt however is never sent by M to
+ P; instead C and M both send
+ @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}
+ and P compares the two copies of HOD.
+
+ Agreement can't be proved for some things, including the symmetric keys
+ used in the digital envelopes. On the other hand, M knows the true identity
+ of PG (namely j'), and sends AReq there; he can't, however, check that
+ the EXcrypt involves the correct PG's key.
+*}
+lemma P_sees_CM_agreement:
+ "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
+ KC \<in> symKeys;
+ Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
+ \<in> set evs;
+ C = Cardholder k;
+ PI_sign = sign (priSK C) {|Hash PIData, HOIData|};
+ P_I = {|PI_sign,
+ EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};
+ PANData = {|Pan (pan C), Nonce (PANSecret k)|};
+ PIData = {|PIHead, PANData|};
+ PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain|};
+ evs \<in> set_pur; C \<notin> bad; M \<notin> bad|]
+ ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.
+ HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
+ HOIData = Hash OIData &
+ Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &
+ Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &
+ Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
+ AuthReqData P_I'') \<in> set evs &
+ P_I' = {|PI_sign,
+ EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &
+ P_I'' = {|PI_sign,
+ EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"
+apply clarify
+apply (rule exE)
+apply (rule P_verifies_Signed_PReq [OF refl refl refl])
+apply (simp (no_asm_use) add: sign_def EncB_def, blast)
+apply (assumption+, clarify, simp)
+apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
+apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2)
+done
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/ROOT.ML Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,16 @@
+(* Title: HOL/SET-Protocol/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2003 University of Cambridge
+
+Root file for the SET protocol proofs.
+*)
+
+goals_limit := 1;
+set timing;
+
+no_document use_thy "NatPair";
+time_use_thy "Cardholder_Registration";
+time_use_thy "Merchant_Registration";
+time_use_thy "Purchase";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET-Protocol/document/root.tex Tue Sep 23 15:40:27 2003 +0200
@@ -0,0 +1,27 @@
+\documentclass[10pt,a4paper,twoside]{article}
+\usepackage{graphicx}
+\usepackage{latexsym,theorem}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\begin{document}
+
+\pagestyle{headings}
+\pagenumbering{arabic}
+
+\title{Verification of The SET Protocol}
+\author{Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson et al.}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+ \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+\end{document}