# HG changeset patch
# User wenzelm
# Date 1256061803 -7200
# Node ID 9aa8bfb1649d8ae83f684852fc1f9119ba24dbec
# Parent 9cf389429f6df980c84b68fb90238c58900fad0b
modernized session SET_Protocol;
diff -r 9cf389429f6d -r 9aa8bfb1649d Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats Tue Oct 20 19:52:04 2009 +0200
+++ b/Admin/isatest/isatest-stats Tue Oct 20 20:03:23 2009 +0200
@@ -27,7 +27,7 @@
HOL-Nominal-Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
- HOL-SET-Protocol \
+ HOL-SET_Protocol \
HOL-UNITY \
HOL-Word \
HOL-ex \
diff -r 9cf389429f6d -r 9aa8bfb1649d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Tue Oct 20 19:52:04 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Oct 20 20:03:23 2009 +0200
@@ -38,7 +38,7 @@
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Prolog \
- HOL-SET-Protocol \
+ HOL-SET_Protocol \
HOL-SizeChange \
HOL-SMT-Examples \
HOL-Statespace \
@@ -932,16 +932,16 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
-## HOL-SET-Protocol
+## HOL-SET_Protocol
-HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
+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
- @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol
+$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \
+ SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
+ SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
+ SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
+ SET_Protocol/document/root.tex
+ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
## HOL-Matrix
@@ -1315,7 +1315,7 @@
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \
$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
- $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET-Protocol.gz \
+ $(LOG)/HOL-Hahn_Banach.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 $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \
diff -r 9cf389429f6d -r 9aa8bfb1649d src/HOL/README.html
--- a/src/HOL/README.html Tue Oct 20 19:52:04 2009 +0200
+++ b/src/HOL/README.html Tue Oct 20 20:03:23 2009 +0200
@@ -99,7 +99,7 @@
Hahn_Banach
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
-SET-Protocol
+SET_Protocol
verification of the SET Protocol
Subst
diff -r 9cf389429f6d -r 9aa8bfb1649d src/HOL/SET-Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Tue Oct 20 19:52:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1054 +0,0 @@
-(* Title: HOL/SET-Protocol/Cardholder_Registration.thy
- Author: Giampaolo Bella
- Author: Fabio Massacci
- Author: Lawrence C Paulson
- Author: Piero Tramontano
-*)
-
-header{*The SET Cardholder Registration Protocol*}
-
-theory Cardholder_Registration imports PublicSET begin
-
-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 =>
- ((\N X Y. A \ Spy &
- DK \ symKeys &
- Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
- (\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 \ Spy &
- ((\X Y. DK \ symKeys &
- Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
- (\X Y. DK \ symKeys &
- Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
- (\K i X Y.
- K \ symKeys &
- Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
- (DK=K | KeyCryptKey DK K evs)) |
- (\K C NC3 Y.
- K \ symKeys &
- Z = Crypt K
- {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
- Y|} &
- (DK=K | KeyCryptKey DK K evs)) |
- (\C. DK = priEK C))
- | Gets A' X => False
- | Notes A' X => False))"
-
-
-subsection{*Formal protocol definition *}
-
-inductive_set
- set_cr :: "event list set"
-where
-
- Nil: --{*Initial trace is empty*}
- "[] \ set_cr"
-
-| Fake: --{*The spy MAY say anything he CAN say.*}
- "[| evsf \ set_cr; X \ synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \ set_cr"
-
-| Reception: --{*If A sends a message X to B, then B might receive it*}
- "[| evsr \ set_cr; Says A B X \ set evsr |]
- ==> Gets B X # evsr \ set_cr"
-
-| SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
- "[| evs1 \ set_cr; C = Cardholder k; Nonce NC1 \ used evs1 |]
- ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \ set_cr"
-
-| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
- "[| evs2 \ set_cr;
- Gets (CA i) {|Agent C, Nonce NC1|} \ 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 \ 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 \ set_cr; C = Cardholder k;
- Nonce NC2 \ used evs3;
- Key KC1 \ used evs3; KC1 \ symKeys;
- Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
- cert (CA i) EKi onlyEnc (priSK RCA),
- cert (CA i) SKi onlySig (priSK RCA)|}
- \ set evs3;
- Says C (CA i) {|Agent C, Nonce NC1|} \ set evs3|]
- ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
- # Notes C {|Key KC1, Agent (CA i)|}
- # evs3 \ 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 \ set_cr;
- Nonce NCA \ used evs4; KC1 \ symKeys;
- Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
- \ 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 \ 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 \ set_cr; C = Cardholder k;
- Nonce NC3 \ used evs5; Nonce CardSecret \ used evs5; NC3\CardSecret;
- Key KC2 \ used evs5; KC2 \ symKeys;
- Key KC3 \ used evs5; KC3 \ symKeys; KC2\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) |}
- \ set evs5;
- Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
- \ 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 \ 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 \ set_cr;
- Nonce NonceCCA \ used evs6;
- KC2 \ symKeys; KC3 \ symKeys; cardSK \ symKeys;
- Notes (CA i) (Key cardSK) \ 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|} |}
- \ 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 \ 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 \ set_cr ==> Gets B X # Says A B X # evs \ 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 \ symKeys; Key KC1 \ used [];
- KC2 \ symKeys; Key KC2 \ used [];
- KC3 \ symKeys; Key KC3 \ used [];
- C = Cardholder k|]
- ==> \evs \ 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)|})
- \ set evs"
-apply (intro exI bexI)
-apply (rule_tac [2]
- set_cr.Nil
- [THEN set_cr.SET_CR1 [of concl: C i NC1],
- THEN Says_to_Gets,
- THEN set_cr.SET_CR2 [of concl: i C NC1],
- THEN Says_to_Gets,
- THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2],
- THEN Says_to_Gets,
- THEN set_cr.SET_CR4 [of concl: i C NC2 NCA],
- THEN Says_to_Gets,
- THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
- THEN Says_to_Gets,
- THEN set_cr.SET_CR6 [of concl: i C KC2]])
-apply basic_possibility
-apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
-done
-
-text{*General facts about message reception*}
-lemma Gets_imp_Says:
- "[| Gets B X \ set evs; evs \ set_cr |] ==> \A. Says A B X \ set evs"
-apply (erule rev_mp)
-apply (erule set_cr.induct, auto)
-done
-
-lemma Gets_imp_knows_Spy:
- "[| Gets B X \ set evs; evs \ set_cr |] ==> X \ 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 \ set_cr
- ==> (Key(invKey (publicKey b A)) \ parts(knows Spy evs)) = (A \ bad)"
-by (erule set_cr.induct, auto)
-
-lemma Spy_analz_private_Key [simp]:
- "evs \ set_cr ==>
- (Key(invKey (publicKey b A)) \ analz(knows Spy evs)) = (A \ 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|}
- \ parts (knows Spy evs);
- evs \ 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) \ parts (knows Spy evs);
- evs \ 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|}
- \ parts (knows Spy evs);
- evs \ 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) \ parts (knows Spy evs);
- evs \ 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)|} \ set evs;
- evs \ 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 \ symKeys; Key K \ used evs; evs \ set_cr|]
- ==> K \ 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)
-apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
-apply (blast,auto) --{*Others*}
-done
-
-
-subsection{*New versions: as above, but generalized to have the KK argument *}
-
-lemma gen_new_keys_not_used:
- "[|Key K \ used evs; K \ symKeys; evs \ set_cr |]
- ==> Key K \ used evs --> K \ symKeys -->
- K \ keysFor (parts (Key`KK Un knows Spy evs))"
-by (auto simp add: new_keys_not_used)
-
-lemma gen_new_keys_not_analzd:
- "[|Key K \ used evs; K \ symKeys; evs \ set_cr |]
- ==> K \ 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 \ symKeys; Key K \ used evs; evs \ set_cr |]
- ==> analz (Key ` (insert K KK) \ knows Spy evs) =
- insert (Key K) (analz (Key ` KK \ knows Spy evs))"
-by (simp add: gen_new_keys_not_analzd)
-
-lemma Crypt_parts_imp_used:
- "[|Crypt K X \ parts (knows Spy evs);
- K \ symKeys; evs \ set_cr |] ==> Key K \ 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 \ analz (knows Spy evs);
- K \ symKeys; evs \ set_cr |] ==> Key K \ 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|})
- \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
- \ 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|})
- \ parts (knows Spy evs);
- cert (CA i) SK onlySig (priSK RCA) \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
- \ 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|})
- \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y. Says (CA i) C {|sign (priSK (CA i))
- {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \ 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|})
- \ parts (knows Spy evs);
- cert (CA i) SK onlySig (priSK RCA) \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y. Says (CA i) C {|sign (priSK (CA i))
- {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \ 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|})
- \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
- {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \ 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|})
- \ parts (knows Spy evs);
- cert (CA i) SK onlySig (priSK RCA) \ parts (knows Spy evs);
- evs \ set_cr; (CA i) \ bad |]
- ==> \Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
- {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \ 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) \ parts (Key`KK Un (knows Spy evs));
- evs \ set_cr|] ==> priEK C \ KK | C \ bad"
-by auto
-
-text{*trivial proof because (priEK C) never appears even in (parts evs)*}
-lemma analz_image_priEK:
- "evs \ set_cr ==>
- (Key (priEK C) \ analz (Key`KK Un (knows Spy evs))) =
- (priEK C \ KK | C \ 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 \ used evs; evs \ 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:
- "[|\C. DK \ priEK C; Key K \ 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 \ analz (knows Spy evs);
- Key cardSK : parts (knows Spy evs);
- evs \ set_cr|] ==> cardSK \ priEK C"
-by blast
-
-lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
- "[|cardSK \ symKeys; \C. cardSK \ priEK C; evs \ set_cr|] ==>
- Key cardSK \ 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|}
- \ set evs;
- cardSK \ symKeys; evs \ set_cr|]
- ==> Key cardSK \ analz (knows Spy evs) |
- (\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 \ analz (Key`KK Un H)) --> (K \ KK | Key K \ analz H)
- ==>
- P --> (Key K \ analz (Key`KK Un H)) = (K \ KK | Key K \ analz H)"
-by (blast intro: analz_mono [THEN [2] rev_subsetD])
-
-method_setup valid_certificate_tac = {*
- Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
- (fn i =>
- EVERY [ftac @{thm 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 \ set_cr ==>
- (\SK KK. SK \ symKeys \ (\K \ KK. ~ KeyCryptKey K SK evs) -->
- (Key SK \ analz (Key`KK Un (knows Spy evs))) =
- (SK \ KK | Key SK \ 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 (valid_certificate_tac [8]) --{*for message 5*}
-apply (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)
- --{*9 seconds on a 1.6GHz machine*}
-apply spy_analz
-apply blast --{*3*}
-apply blast --{*5*}
-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 \ bad; K \ symKeys; evs \ set_cr|]
- ==> \X c. Says (Cardholder c) (CA i) X \ set evs -->
- Key K \ parts{X} -->
- Cardholder c \ bad -->
- Key K \ 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)
- --{*2.5 seconds on a 1.6GHz machine*}
-apply spy_analz --{*Fake*}
-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|}
- \ parts (knows Spy evs);
- CA i \ bad; evs \ set_cr|]
- ==> \KC2 X Y. Says (CA i) C
- (Crypt KC2
- {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
- \ 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)|}) \ set evs;
- CA i \ bad; evs \ set_cr|]
- ==> \KC2 X Y. Says (CA i) C
- (Crypt KC2
- {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
- \ 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 \ set_cr
- ==> Hash{|X, Nonce N|} \ parts (knows Spy evs) -->
- Nonce N \ 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 \ set_cr
- ==> Hash{|X, Nonce M, Y, Nonce N|} \ parts (knows Spy evs) -->
- Nonce M \ parts (knows Spy evs) & Nonce N \ 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 \ symKeys; Key DK \ used evs; evs \ 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:
- "\C. DK \ priEK C ==> Nonce N \ 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 \ symKeys; \C. cardSK \ priEK C; evs \ set_cr|] ==>
- Key cardSK \ analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
-apply (erule set_cr.induct, analz_mono_contra, simp_all)
-apply (blast dest: not_KeyCryptKey_cardSK) --{*6*}
-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|}
- \ set evs;
- cardSK \ symKeys; evs \ set_cr|]
- ==> Key cardSK \ analz (knows Spy evs) |
- ((\K. ~ KeyCryptKey cardSK K evs) &
- (\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 \ analz (Key`KK Un H)) --> (Nonce N \ analz H)
- ==> P --> (Nonce N \ analz (Key`KK Un H)) = (Nonce N \ 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 \ set_cr ==>
- (\N KK. (\K \ KK. ~ KeyCryptNonce K N evs) -->
- (Nonce N \ analz (Key`KK Un (knows Spy evs))) =
- (Nonce N \ 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)
- --{*14 seconds on a 1.6GHz machine*}
-apply spy_analz --{*Fake*}
-apply blast --{*3*}
-apply blast --{*5*}
-txt{*Message 6*}
-apply (metis symKey_compromise)
- --{*cardSK compromised*}
-txt{*Simplify again--necessary because the previous simplification introduces
- some logical connectives*}
-apply (force simp del: image_insert image_Un imp_disjL
- simp add: analz_image_keys_simps symKey_compromise)
-done
-
-
-subsection{*Secrecy of CardSecret: the Cardholder's secret*}
-
-lemma NC2_not_CardSecret:
- "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
- \ parts (knows Spy evs);
- Key K \ analz (knows Spy evs);
- Nonce N \ analz (knows Spy evs);
- evs \ set_cr|]
- ==> Crypt EKi {|Key K', Pan p', Nonce N|} \ 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 \ parts (knows Spy evs);
- evs \