--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Thu May 26 17:51:22 2016 +0200
@@ -5,33 +5,33 @@
Author: Piero Tramontano
*)
-section{*The SET Cardholder Registration Protocol*}
+section\<open>The SET Cardholder Registration Protocol\<close>
theory Cardholder_Registration
imports Public_SET
begin
-text{*Note: nonces seem to consist of 20 bytes. That includes both freshness
+text\<open>Note: nonces seem to consist of 20 bytes. That includes both freshness
challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
-*}
+\<close>
-text{*Simplifications involving @{text analz_image_keys_simps} appear to
+text\<open>Simplifications involving \<open>analz_image_keys_simps\<close> 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.*}
+and the rewriting is very sensitive to the set of rewrite rules given.\<close>
-subsection{*Predicate Formalizing the Encryption Association between Keys *}
+subsection\<open>Predicate Formalizing the Encryption Association between Keys\<close>
primrec KeyCryptKey :: "[key, key, event list] => bool"
where
KeyCryptKey_Nil:
"KeyCryptKey DK K [] = False"
| KeyCryptKey_Cons:
- --{*Says is the only important case.
+ \<comment>\<open>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). *}
+ priEK C is never sent (and so can't be lost except at the start).\<close>
"KeyCryptKey DK K (ev # evs) =
(KeyCryptKey DK K evs |
(case ev of
@@ -44,23 +44,23 @@
| Notes A' X => False))"
-subsection{*Predicate formalizing the association between keys and nonces *}
+subsection\<open>Predicate formalizing the association between keys and nonces\<close>
primrec KeyCryptNonce :: "[key, key, event list] => bool"
where
KeyCryptNonce_Nil:
"KeyCryptNonce EK K [] = False"
| KeyCryptNonce_Cons:
- --{*Says is the only important case.
+ \<comment>\<open>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
+ But we can't prove \<open>Nonce_compromise\<close> unless the relation covers ALL
nonces that the protocol keeps secret.
- *}
+\<close>
"KeyCryptNonce DK N (ev # evs) =
(KeyCryptNonce DK N evs |
(case ev of
@@ -85,28 +85,28 @@
| Notes A' X => False))"
-subsection{*Formal protocol definition *}
+subsection\<open>Formal protocol definition\<close>
inductive_set
set_cr :: "event list set"
where
- Nil: --{*Initial trace is empty*}
+ Nil: \<comment>\<open>Initial trace is empty\<close>
"[] \<in> set_cr"
-| Fake: --{*The spy MAY say anything he CAN say.*}
+| Fake: \<comment>\<open>The spy MAY say anything he CAN say.\<close>
"[| 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*}
+| Reception: \<comment>\<open>If A sends a message X to B, then B might receive it\<close>
"[| 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*}
+| SET_CR1: \<comment>\<open>CardCInitReq: C initiates a run, sending a nonce to CCA\<close>
"[| evs1 \<in> set_cr; C = Cardholder k; Nonce NC1 \<notin> used evs1 |]
==> Says C (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> # evs1 \<in> set_cr"
-| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
+| SET_CR2: \<comment>\<open>CardCInitRes: CA responds sending NC1 and its certificates\<close>
"[| evs2 \<in> set_cr;
Gets (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> \<in> set evs2 |]
==> Says (CA i) C
@@ -116,7 +116,7 @@
# evs2 \<in> set_cr"
| SET_CR3:
- --{*RegFormReq: C sends his PAN and a new nonce to CA.
+ \<comment>\<open>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;
@@ -126,7 +126,7 @@
checking the signature).
C generates a fresh symmetric key KC1.
The point of encrypting @{term "\<lbrace>Agent C, Nonce NC2, Hash (Pan(pan C))\<rbrace>"}
- is not clear. *}
+ is not clear.\<close>
"[| evs3 \<in> set_cr; C = Cardholder k;
Nonce NC2 \<notin> used evs3;
Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
@@ -140,11 +140,11 @@
# evs3 \<in> set_cr"
| SET_CR4:
- --{*RegFormRes:
+ \<comment>\<open>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) *}
+ envelope (here, KC1)\<close>
"[| evs4 \<in> set_cr;
Nonce NCA \<notin> used evs4; KC1 \<in> symKeys;
Gets (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan X)))
@@ -156,11 +156,11 @@
# evs4 \<in> set_cr"
| SET_CR5:
- --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
+ \<comment>\<open>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.*}
+ The encryption below is actually EncX.\<close>
"[| 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;
@@ -183,13 +183,13 @@
# evs5 \<in> set_cr"
- --{* CertRes: CA responds sending NC3 back with its half of the secret value,
+ \<comment>\<open>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)"}.
-*}
+\<close>
| SET_CR6:
"[| evs6 \<in> set_cr;
@@ -218,15 +218,15 @@
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.*}
+text\<open>A "possibility property": there are traces that reach the end.
+ An unconstrained proof with many subgoals.\<close>
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.*}
+text\<open>The many nonces and keys generated, some simultaneously, force us to
+ introduce them explicitly as shown below.\<close>
lemma possibility_CR6:
"[|NC1 < (NC2::nat); NC2 < NC3; NC3 < NCA ;
NCA < NonceCCA; NonceCCA < CardSecret;
@@ -262,7 +262,7 @@
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
done
-text{*General facts about message reception*}
+text\<open>General facts about message reception\<close>
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)
@@ -275,9 +275,9 @@
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
-subsection{*Proofs on keys *}
+subsection\<open>Proofs on keys\<close>
-text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
+text\<open>Spy never sees an agent's private keys! (unless it's bad at start)\<close>
lemma Spy_see_private_Key [simp]:
"evs \<in> set_cr
@@ -293,8 +293,8 @@
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 *}
+subsection\<open>Begin Piero's Theorems on Certificates\<close>
+text\<open>Trivial in the current model, where certificates by RCA are secure\<close>
lemma Crypt_valid_pubEK:
"[| Crypt (priSK RCA) \<lbrace>Agent C, Key EKi, onlyEnc\<rbrace>
@@ -334,7 +334,7 @@
==> EKi = pubEK C & SKi = pubSK C"
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
-text{*Nobody can have used non-existent keys!*}
+text\<open>Nobody can have used non-existent keys!\<close>
lemma new_keys_not_used:
"[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
==> K \<notin> keysFor (parts (knows Spy evs))"
@@ -343,12 +343,12 @@
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*}
+apply (force dest!: usedI keysFor_parts_insert) \<comment>\<open>Fake\<close>
+apply (blast,auto) \<comment>\<open>Others\<close>
done
-subsection{*New versions: as above, but generalized to have the KK argument *}
+subsection\<open>New versions: as above, but generalized to have the KK argument\<close>
lemma gen_new_keys_not_used:
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
@@ -382,10 +382,10 @@
(*<*)
-subsection{*Messages signed by CA*}
+subsection\<open>Messages signed by CA\<close>
-text{*Message @{text SET_CR2}: C can check CA's signature if he has received
- CA's certificate.*}
+text\<open>Message \<open>SET_CR2\<close>: C can check CA's signature if he has received
+ CA's certificate.\<close>
lemma CA_Says_2_lemma:
"[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
\<in> parts (knows Spy evs);
@@ -396,7 +396,7 @@
apply (erule set_cr.induct, auto)
done
-text{*Ever used?*}
+text\<open>Ever used?\<close>
lemma CA_Says_2:
"[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
\<in> parts (knows Spy evs);
@@ -407,8 +407,8 @@
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.*}
+text\<open>Message \<open>SET_CR4\<close>: C can check CA's signature if he has received
+ CA's certificate.\<close>
lemma CA_Says_4_lemma:
"[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
\<in> parts (knows Spy evs);
@@ -419,7 +419,7 @@
apply (erule set_cr.induct, auto)
done
-text{*NEVER USED*}
+text\<open>NEVER USED\<close>
lemma CA_Says_4:
"[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
\<in> parts (knows Spy evs);
@@ -430,8 +430,8 @@
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.*}
+text\<open>Message \<open>SET_CR6\<close>: C can check CA's signature if he has
+ received CA's certificate.\<close>
lemma CA_Says_6_lemma:
"[| Crypt (priSK (CA i))
(Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
@@ -443,7 +443,7 @@
apply (erule set_cr.induct, auto)
done
-text{*NEVER USED*}
+text\<open>NEVER USED\<close>
lemma CA_Says_6:
"[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
\<in> parts (knows Spy evs);
@@ -455,17 +455,17 @@
(*>*)
-subsection{*Useful lemmas *}
+subsection\<open>Useful lemmas\<close>
-text{*Rewriting rule for private encryption keys. Analogous rewriting rules
-for other keys aren't needed.*}
+text\<open>Rewriting rule for private encryption keys. Analogous rewriting rules
+for other keys aren't needed.\<close>
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)*}
+text\<open>trivial proof because (priEK C) never appears even in (parts evs)\<close>
lemma analz_image_priEK:
"evs \<in> set_cr ==>
(Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
@@ -473,12 +473,12 @@
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
-subsection{*Secrecy of Session Keys *}
+subsection\<open>Secrecy of Session Keys\<close>
-subsubsection{*Lemmas about the predicate KeyCryptKey *}
+subsubsection\<open>Lemmas about the predicate KeyCryptKey\<close>
-text{*A fresh DK cannot be associated with any other
- (with respect to a given trace). *}
+text\<open>A fresh DK cannot be associated with any other
+ (with respect to a given trace).\<close>
lemma DK_fresh_not_KeyCryptKey:
"[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
apply (erule rev_mp)
@@ -487,9 +487,9 @@
apply (blast dest: Crypt_analz_imp_used)+
done
-text{*A fresh K cannot be associated with any other. The assumption that
+text\<open>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.*}
+ definition of KeyCryptKey.\<close>
lemma K_fresh_not_KeyCryptKey:
"[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
apply (induct evs)
@@ -497,8 +497,8 @@
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}*}
+text\<open>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}\<close>
lemma cardSK_neq_priEK:
"[|Key cardSK \<notin> analz (knows Spy evs);
Key cardSK : parts (knows Spy evs);
@@ -510,16 +510,16 @@
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.*}
+text\<open>Lemma for message 5: pubSK C is never used to encrypt Keys.\<close>
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)
+text\<open>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.*}
+ \<open>SET_CR5\<close> is executed only by honest agents.\<close>
lemma msg6_KeyCryptKey_disj:
"[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs;
@@ -528,23 +528,23 @@
(\<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*}
+text\<open>As usual: we express the property as a logical equivalence\<close>
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])
-method_setup valid_certificate_tac = {*
+method_setup valid_certificate_tac = \<open>
Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
(fn i =>
EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
assume_tac ctxt i,
eresolve_tac ctxt [conjE] i, REPEAT (hyp_subst_tac ctxt i)]))
-*}
+\<close>
-text{*The @{text "(no_asm)"} attribute is essential, since it retains
- the quantifier and allows the simprule's condition to itself be simplified.*}
+text\<open>The \<open>(no_asm)\<close> attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.\<close>
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) -->
@@ -553,8 +553,8 @@
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 (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
+apply (valid_certificate_tac [6]) \<comment>\<open>for message 5\<close>
apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -563,15 +563,15 @@
K_fresh_not_KeyCryptKey
DK_fresh_not_KeyCryptKey ball_conj_distrib
analz_image_priEK disj_simps)
- --{*9 seconds on a 1.6GHz machine*}
+ \<comment>\<open>9 seconds on a 1.6GHz machine\<close>
apply spy_analz
-apply blast --{*3*}
-apply blast --{*5*}
+apply blast \<comment>\<open>3\<close>
+apply blast \<comment>\<open>5\<close>
done
-text{*The remaining quantifiers seem to be essential.
+text\<open>The remaining quantifiers seem to be essential.
NO NEED to assume the cardholder's OK: bad cardholders don't do anything
- wrong!!*}
+ wrong!!\<close>
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 -->
@@ -579,8 +579,8 @@
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 (frule_tac [8] Gets_certificate_valid) \<comment>\<open>for message 5\<close>
+apply (frule_tac [6] Gets_certificate_valid) \<comment>\<open>for message 3\<close>
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
@@ -589,18 +589,18 @@
K_fresh_not_KeyCryptKey
DK_fresh_not_KeyCryptKey
analz_image_priEK)
- --{*2.5 seconds on a 1.6GHz machine*}
-apply spy_analz --{*Fake*}
+ \<comment>\<open>2.5 seconds on a 1.6GHz machine\<close>
+apply spy_analz \<comment>\<open>Fake\<close>
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
done
-subsection{*Primary Goals of Cardholder Registration *}
+subsection\<open>Primary Goals of Cardholder Registration\<close>
-text{*The cardholder's certificate really was created by the CA, provided the
- CA is uncompromised *}
+text\<open>The cardholder's certificate really was created by the CA, provided the
+ CA is uncompromised\<close>
-text{*Lemma concerning the actual signed message digest*}
+text\<open>Lemma concerning the actual signed message digest\<close>
lemma cert_valid_lemma:
"[|Crypt (priSK (CA i)) \<lbrace>Hash \<lbrace>Nonce N, Pan(pan C)\<rbrace>, Key cardSK, N1\<rbrace>
\<in> parts (knows Spy evs);
@@ -615,8 +615,8 @@
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.*}
+text\<open>Pre-packaged version for cardholder. We don't try to confirm the values
+ of KC2, X and Y, since they are not important.\<close>
lemma certificate_valid_cardSK:
"[|Gets C (Crypt KC2 \<lbrace>X, certC (pan C) cardSK N onlySig (invKey SKi),
cert (CA i) SKi onlySig (priSK RCA)\<rbrace>) \<in> set evs;
@@ -648,12 +648,12 @@
done
-subsection{*Secrecy of Nonces*}
+subsection\<open>Secrecy of Nonces\<close>
-subsubsection{*Lemmas about the predicate KeyCryptNonce *}
+subsubsection\<open>Lemmas about the predicate KeyCryptNonce\<close>
-text{*A fresh DK cannot be associated with any other
- (with respect to a given trace). *}
+text\<open>A fresh DK cannot be associated with any other
+ (with respect to a given trace).\<close>
lemma DK_fresh_not_KeyCryptNonce:
"[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
==> ~ KeyCryptNonce DK K evs"
@@ -666,8 +666,8 @@
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). *}
+text\<open>A fresh N cannot be associated with any other
+ (with respect to a given trace).\<close>
lemma N_fresh_not_KeyCryptNonce:
"\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
apply (induct_tac "evs")
@@ -680,21 +680,21 @@
"[|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)
-apply (blast dest: not_KeyCryptKey_cardSK) --{*6*}
+apply (blast dest: not_KeyCryptKey_cardSK) \<comment>\<open>6\<close>
done
-subsubsection{*Lemmas for message 5 and 6:
+subsubsection\<open>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. *}
+ or else cardSK hasn't been used to encrypt K.\<close>
-text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
+text\<open>Lemma for message 5: pubSK C is never used to encrypt Nonces.\<close>
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.*}
+text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
+ or else cardSK hasn't been used to encrypt K.\<close>
lemma msg6_KeyCryptNonce_disj:
"[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs;
@@ -706,15 +706,15 @@
intro: cardSK_neq_priEK)
-text{*As usual: we express the property as a logical equivalence*}
+text\<open>As usual: we express the property as a logical equivalence\<close>
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.*}
+text\<open>The \<open>(no_asm)\<close> attribute is essential, since it retains
+ the quantifier and allows the simprule's condition to itself be simplified.\<close>
lemma Nonce_compromise [rule_format (no_asm)]:
"evs \<in> set_cr ==>
(\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs) -->
@@ -723,8 +723,8 @@
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 [8] Gets_certificate_valid) \<comment>\<open>for message 5\<close>
+apply (frule_tac [6] Gets_certificate_valid) \<comment>\<open>for message 3\<close>
apply (frule_tac [11] msg6_KeyCryptNonce_disj)
apply (erule_tac [13] disjE)
apply (simp_all del: image_insert image_Un
@@ -734,21 +734,21 @@
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*}
+ \<comment>\<open>14 seconds on a 1.6GHz machine\<close>
+apply spy_analz \<comment>\<open>Fake\<close>
+apply blast \<comment>\<open>3\<close>
+apply blast \<comment>\<open>5\<close>
+txt\<open>Message 6\<close>
apply (metis symKey_compromise)
- --{*cardSK compromised*}
-txt{*Simplify again--necessary because the previous simplification introduces
- some logical connectives*}
+ \<comment>\<open>cardSK compromised\<close>
+txt\<open>Simplify again--necessary because the previous simplification introduces
+ some logical connectives\<close>
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*}
+subsection\<open>Secrecy of CardSecret: the Cardholder's secret\<close>
lemma NC2_not_CardSecret:
"[|Crypt EKj \<lbrace>Key K, Pan p, Hash \<lbrace>Agent D, Nonce N\<rbrace>\<rbrace>
@@ -773,12 +773,12 @@
Cardholder k \<notin> bad & CA i \<notin> bad)"
apply (erule_tac P = "U \<in> H" for H in rev_mp)
apply (erule set_cr.induct)
-apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
apply (simp_all del: image_insert image_Un imp_disjL
add: analz_image_keys_simps analz_knows_absorb
analz_knows_absorb2 notin_image_iff)
- --{*4 seconds on a 1.6GHz machine*}
-apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
+ \<comment>\<open>4 seconds on a 1.6GHz machine\<close>
+apply (simp_all (no_asm_simp)) \<comment>\<open>leaves 4 subgoals\<close>
apply (blast intro!: analz_insertI)+
done
@@ -790,7 +790,7 @@
by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
-text{*Inductive version*}
+text\<open>Inductive version\<close>
lemma CardSecret_secrecy_lemma [rule_format]:
"[|CA i \<notin> bad; evs \<in> set_cr|]
==> Key K \<notin> analz (knows Spy evs) -->
@@ -798,8 +798,8 @@
\<in> parts (knows Spy evs) -->
Nonce CardSecret \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
-apply (valid_certificate_tac [8]) --{*for message 5*}
-apply (valid_certificate_tac [6]) --{*for message 5*}
+apply (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
+apply (valid_certificate_tac [6]) \<comment>\<open>for message 5\<close>
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -809,19 +809,19 @@
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
ball_conj_distrib Nonce_compromise symKey_compromise
analz_image_priEK)
- --{*2.5 seconds on a 1.6GHz machine*}
-apply spy_analz --{*Fake*}
+ \<comment>\<open>2.5 seconds on a 1.6GHz machine\<close>
+apply spy_analz \<comment>\<open>Fake\<close>
apply (simp_all (no_asm_simp))
-apply blast --{*1*}
-apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*}
-apply blast --{*3*}
-apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) --{*4*}
-apply blast --{*5*}
-apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*}
+apply blast \<comment>\<open>1\<close>
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) \<comment>\<open>2\<close>
+apply blast \<comment>\<open>3\<close>
+apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) \<comment>\<open>4\<close>
+apply blast \<comment>\<open>5\<close>
+apply (blast dest: KC2_secrecy)+ \<comment>\<open>Message 6: two cases\<close>
done
-text{*Packaged version for cardholder*}
+text\<open>Packaged version for cardholder\<close>
lemma CardSecret_secrecy:
"[|Cardholder k \<notin> bad; CA i \<notin> bad;
Says (Cardholder k) (CA i)
@@ -838,7 +838,7 @@
done
-subsection{*Secrecy of NonceCCA [the CA's secret] *}
+subsection\<open>Secrecy of NonceCCA [the CA's secret]\<close>
lemma NC2_not_NonceCCA:
"[|Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace>
@@ -853,7 +853,7 @@
done
-text{*Inductive version*}
+text\<open>Inductive version\<close>
lemma NonceCCA_secrecy_lemma [rule_format]:
"[|CA i \<notin> bad; evs \<in> set_cr|]
==> Key K \<notin> analz (knows Spy evs) -->
@@ -864,8 +864,8 @@
\<in> parts (knows Spy evs) -->
Nonce NonceCCA \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
-apply (valid_certificate_tac [8]) --{*for message 5*}
-apply (valid_certificate_tac [6]) --{*for message 5*}
+apply (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
+apply (valid_certificate_tac [6]) \<comment>\<open>for message 5\<close>
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -875,18 +875,18 @@
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
ball_conj_distrib Nonce_compromise symKey_compromise
analz_image_priEK)
- --{*3 seconds on a 1.6GHz machine*}
-apply spy_analz --{*Fake*}
-apply blast --{*1*}
-apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*}
-apply blast --{*3*}
-apply (blast dest: NC2_not_NonceCCA) --{*4*}
-apply blast --{*5*}
-apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*}
+ \<comment>\<open>3 seconds on a 1.6GHz machine\<close>
+apply spy_analz \<comment>\<open>Fake\<close>
+apply blast \<comment>\<open>1\<close>
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) \<comment>\<open>2\<close>
+apply blast \<comment>\<open>3\<close>
+apply (blast dest: NC2_not_NonceCCA) \<comment>\<open>4\<close>
+apply blast \<comment>\<open>5\<close>
+apply (blast dest: KC2_secrecy)+ \<comment>\<open>Message 6: two cases\<close>
done
-text{*Packaged version for cardholder*}
+text\<open>Packaged version for cardholder\<close>
lemma NonceCCA_secrecy:
"[|Cardholder k \<notin> bad; CA i \<notin> bad;
Gets (Cardholder k)
@@ -906,16 +906,16 @@
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!*}
+text\<open>We don't bother to prove guarantees for the CA. He doesn't care about
+ the PANSecret: it isn't his credit card!\<close>
-subsection{*Rewriting Rule for PANs*}
+subsection\<open>Rewriting Rule for PANs\<close>
-text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
+text\<open>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)"}.*}
+ the expression @{term "analz (insert (Key cardSK) X)"}.\<close>
lemma msg6_cardSK_disj:
"[|Gets A \<lbrace>Crypt K \<lbrace>c, n, k', Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs; evs \<in> set_cr |]
@@ -935,16 +935,16 @@
apply (erule set_cr.induct)
apply (rule_tac [!] allI impI)+
apply (rule_tac [!] analz_image_pan_lemma)
-apply (valid_certificate_tac [8]) --{*for message 5*}
-apply (valid_certificate_tac [6]) --{*for message 5*}
+apply (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
+apply (valid_certificate_tac [6]) \<comment>\<open>for message 5\<close>
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)
- --{*6 seconds on a 1.6GHz machine*}
+ \<comment>\<open>6 seconds on a 1.6GHz machine\<close>
apply spy_analz
-apply (simp add: insert_absorb) --{*6*}
+apply (simp add: insert_absorb) \<comment>\<open>6\<close>
done
lemma analz_insert_pan:
@@ -955,9 +955,9 @@
add: analz_image_keys_simps analz_image_pan)
-text{*Confidentiality of the PAN\@. Maybe we could combine the statements of
+text\<open>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.*}
+ a much more difficult proof.\<close>
lemma pan_confidentiality:
"[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
==> \<exists>i X K HN.
@@ -966,22 +966,22 @@
& (CA i) \<in> bad"
apply (erule rev_mp)
apply (erule set_cr.induct)
-apply (valid_certificate_tac [8]) --{*for message 5*}
-apply (valid_certificate_tac [6]) --{*for message 5*}
+apply (valid_certificate_tac [8]) \<comment>\<open>for message 5\<close>
+apply (valid_certificate_tac [6]) \<comment>\<open>for message 5\<close>
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)
- --{*3.5 seconds on a 1.6GHz machine*}
-apply spy_analz --{*fake*}
-apply blast --{*3*}
-apply blast --{*5*}
-apply (simp (no_asm_simp) add: insert_absorb) --{*6*}
+ \<comment>\<open>3.5 seconds on a 1.6GHz machine\<close>
+apply spy_analz \<comment>\<open>fake\<close>
+apply blast \<comment>\<open>3\<close>
+apply blast \<comment>\<open>5\<close>
+apply (simp (no_asm_simp) add: insert_absorb) \<comment>\<open>6\<close>
done
-subsection{*Unicity*}
+subsection\<open>Unicity\<close>
lemma CR6_Says_imp_Notes:
"[|Says (CA i) C (Crypt KC2
@@ -995,8 +995,8 @@
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.*}
+text\<open>Unicity of cardSK: it uniquely identifies the other components.
+ This holds because a CA accepts a cardSK at most once.\<close>
lemma cardholder_key_unicity:
"[|Says (CA i) C (Crypt KC2
\<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce Y\<rbrace>,
@@ -1018,7 +1018,7 @@
(*<*)
-text{*UNUSED unicity result*}
+text\<open>UNUSED unicity result\<close>
lemma unique_KC1:
"[|Says C B \<lbrace>Crypt KC1 X, Crypt EK \<lbrace>Key KC1, Y\<rbrace>\<rbrace>
\<in> set evs;
@@ -1030,7 +1030,7 @@
apply (erule set_cr.induct, auto)
done
-text{*UNUSED unicity result*}
+text\<open>UNUSED unicity result\<close>
lemma unique_KC2:
"[|Says C B \<lbrace>Crypt K \<lbrace>Agent C, nn, Key KC2, X\<rbrace>, Y\<rbrace> \<in> set evs;
Says C B' \<lbrace>Crypt K' \<lbrace>Agent C, nn', Key KC2, X'\<rbrace>, Y'\<rbrace> \<in> set evs;
@@ -1042,8 +1042,8 @@
(*>*)
-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]*}
+text\<open>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]\<close>
end