--- a/src/HOL/Metis_Examples/Message.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Wed Dec 30 18:17:28 2015 +0100
@@ -47,21 +47,17 @@
| Crypt key msg --{*Encryption, public- or shared-key*}
-text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
+text{*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, 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|}" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
--{*Message Y paired with a MAC computed with the help of X*}
- "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
+ "Hash[X] Y == \<lbrace> Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
definition keysFor :: "msg set => key set" where
--{*Keys useful to decrypt elements of a message set*}
@@ -75,8 +71,8 @@
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
@@ -134,7 +130,7 @@
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"
+lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Crypt [simp]:
@@ -151,7 +147,7 @@
subsection{*Inductive relation "parts"*}
lemma MPair_parts:
- "[| {|X,Y|} \<in> parts H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
[| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
by (blast dest: parts.Fst parts.Snd)
@@ -294,8 +290,8 @@
done
lemma parts_insert_MPair [simp]:
- "parts (insert {|X,Y|} H) =
- insert {|X,Y|} (parts (insert X (insert Y H)))"
+ "parts (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
@@ -325,8 +321,8 @@
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
| Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -340,7 +336,7 @@
text{*Making it safe speeds up proofs*}
lemma MPair_analz [elim!]:
- "[| {|X,Y|} \<in> analz H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
[| X \<in> analz H; Y \<in> analz H |] ==> P
|] ==> P"
by (blast dest: analz.Fst analz.Snd)
@@ -424,8 +420,8 @@
done
lemma analz_insert_MPair [simp]:
- "analz (insert {|X,Y|} H) =
- insert {|X,Y|} (analz (insert X (insert Y H)))"
+ "analz (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct, auto)
@@ -541,7 +537,7 @@
text{*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"
+ "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
apply safe
apply (erule analz.induct, blast+)
done
@@ -572,7 +568,7 @@
| 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"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
| Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
text{*Monotonicity*}
@@ -584,7 +580,7 @@
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 MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Dec 30 18:17:28 2015 +0100
@@ -27,22 +27,18 @@
| Crypt key msg
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|}" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
inductive_set
parts :: "msg set => msg set"
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
inductive_set
@@ -50,8 +46,8 @@
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
| Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -61,7 +57,7 @@
where
Inj [intro]: "X \<in> H ==> X \<in> synth H"
| Agent [intro]: "Agent agt \<in> synth H"
- | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
| Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
primrec initState
@@ -172,13 +168,13 @@
lemma [code]:
"analz H = (let
- H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+ H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
in if H' = H then H else analz H')"
sorry
lemma [code]:
"parts H = (let
- H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+ H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
in if H' = H then H else parts H')"
sorry
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Wed Dec 30 18:17:28 2015 +0100
@@ -61,9 +61,9 @@
assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
assumes "evs =
[Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
- Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
- Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+ Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+ Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
proof -
from assms show "A \<noteq> Spy" by auto
@@ -79,14 +79,14 @@
qed
then have "[?e2, ?e1, ?e0] : ns_public"
proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+ show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
show " Nonce 1 ~: used [?e1, ?e0]" by eval
qed
then show "evs : ns_public"
unfolding assms
proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
+ show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>)
: set [?e2, ?e1, ?e0]" by simp
qed
from assms show "Nonce NB : analz (knows Spy evs)"
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Wed Dec 30 18:17:28 2015 +0100
@@ -57,9 +57,9 @@
assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
assumes "evs =
[Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
- Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
- Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+ Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+ Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
proof -
from assms show "A \<noteq> Spy" by auto
@@ -71,19 +71,19 @@
qed
then have "[?e1, ?e0] : ns_public"
proof (rule Fake)
- show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
+ show "Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace> : synth (analz (knows Spy [?e0]))"
by (intro synth.intros(2,3,4,1)) eval+
qed
then have "[?e2, ?e1, ?e0] : ns_public"
proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+ show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
show " Nonce 1 ~: used [?e1, ?e0]" by eval
qed
then show "evs : ns_public"
unfolding assms
proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
+ show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) : set [?e2, ?e1, ?e0]" by simp
qed
from assms show "Nonce NB : analz (knows Spy evs)"
apply simp
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Dec 30 18:17:28 2015 +0100
@@ -38,7 +38,7 @@
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|}) |
+ Z = \<lbrace>Crypt DK \<lbrace>Agent A, Nonce N, Key K, X\<rbrace>, Y\<rbrace>) |
(\<exists>C. DK = priEK C))
| Gets A' X => False
| Notes A' X => False))"
@@ -67,18 +67,18 @@
Says A B Z =>
A \<noteq> Spy &
((\<exists>X Y. DK \<in> symKeys &
- Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
+ Z = (EXHcrypt DK X \<lbrace>Agent A, Nonce N\<rbrace> Y)) |
(\<exists>X Y. DK \<in> symKeys &
- Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
+ Z = \<lbrace>Crypt DK \<lbrace>Agent A, Nonce N, X\<rbrace>, Y\<rbrace>) |
(\<exists>K i X Y.
K \<in> symKeys &
- Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
+ Z = Crypt K \<lbrace>sign (priSK (CA i)) \<lbrace>Agent B, Nonce N, X\<rbrace>, Y\<rbrace> &
(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|} &
+ \<lbrace>sign (priSK C) \<lbrace>Agent B, Nonce NC3, Agent C, Nonce N\<rbrace>,
+ Y\<rbrace> &
(DK=K | KeyCryptKey DK K evs)) |
(\<exists>C. DK = priEK C))
| Gets A' X => False
@@ -104,15 +104,15 @@
| 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"
+ ==> Says C (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> # 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 |]
+ Gets (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> \<in> set evs2 |]
==> Says (CA i) C
- {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>,
cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
# evs2 \<in> set_cr"
| SET_CR3:
@@ -125,18 +125,18 @@
- 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))|}"}
+ The point of encrypting @{term "\<lbrace>Agent C, Nonce NC2, Hash (Pan(pan C))\<rbrace>"}
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|},
+ Gets C \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NC1\<rbrace>,
cert (CA i) EKi onlyEnc (priSK RCA),
- cert (CA i) SKi onlySig (priSK RCA)|}
+ cert (CA i) SKi onlySig (priSK RCA)\<rbrace>
\<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)|}
+ Says C (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> \<in> set evs3|]
+ ==> Says C (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan C)))
+ # Notes C \<lbrace>Key KC1, Agent (CA i)\<rbrace>
# evs3 \<in> set_cr"
| SET_CR4:
@@ -147,12 +147,12 @@
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)))
+ Gets (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan X)))
\<in> set evs4 |]
==> Says (CA i) C
- {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>,
cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
# evs4 \<in> set_cr"
| SET_CR5:
@@ -165,21 +165,21 @@
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|},
+ Gets C \<lbrace>sign (invKey SKi) \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>,
cert (CA i) EKi onlyEnc (priSK RCA),
- cert (CA i) SKi onlySig (priSK RCA) |}
+ cert (CA i) SKi onlySig (priSK RCA) \<rbrace>
\<in> set evs5;
- Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
+ Says C (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan C)))
\<in> set evs5 |]
==> Says C (CA i)
- {|Crypt KC3
- {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
+ \<lbrace>Crypt KC3
+ \<lbrace>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)|}
+ (Hash \<lbrace>Agent C, Nonce NC3, Key KC2,
+ Key (pubSK C), Pan (pan C), Nonce CardSecret\<rbrace>)\<rbrace>,
+ Crypt EKi \<lbrace>Key KC3, Pan (pan C), Nonce CardSecret\<rbrace> \<rbrace>
+ # Notes C \<lbrace>Key KC2, Agent (CA i)\<rbrace>
+ # Notes C \<lbrace>Key KC3, Agent (CA i)\<rbrace>
# evs5 \<in> set_cr"
@@ -197,18 +197,18 @@
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,
+ \<lbrace>Crypt KC3 \<lbrace>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|} |}
+ (Hash \<lbrace>Agent C, Nonce NC3, Key KC2,
+ Key cardSK, Pan (pan C), Nonce CardSecret\<rbrace>)\<rbrace>,
+ Crypt (pubEK (CA i)) \<lbrace>Key KC3, Pan (pan C), Nonce CardSecret\<rbrace> \<rbrace>
\<in> set evs6 |]
==> Says (CA i) C
(Crypt KC2
- {|sign (priSK (CA i))
- {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+ \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA\<rbrace>,
certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
# Notes (CA i) (Key cardSK)
# evs6 \<in> set_cr"
@@ -238,11 +238,11 @@
==> \<exists>evs \<in> set_cr.
Says (CA i) C
(Crypt KC2
- {|sign (priSK (CA i))
- {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+ \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA\<rbrace>,
certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
onlySig (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
@@ -297,7 +297,7 @@
text{*Trivial in the current model, where certificates by RCA are secure *}
lemma Crypt_valid_pubEK:
- "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent C, Key EKi, onlyEnc\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_cr |] ==> EKi = pubEK C"
apply (erule rev_mp)
@@ -313,7 +313,7 @@
done
lemma Crypt_valid_pubSK:
- "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent C, Key SKi, onlySig\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_cr |] ==> SKi = pubSK C"
apply (erule rev_mp)
@@ -328,8 +328,8 @@
done
lemma Gets_certificate_valid:
- "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
- cert C SKi onlySig (priSK RCA)|} \<in> set evs;
+ "[| Gets A \<lbrace> X, cert C EKi onlyEnc (priSK RCA),
+ cert C SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
evs \<in> set_cr |]
==> EKi = pubEK C & SKi = pubSK C"
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
@@ -387,10 +387,10 @@
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|})
+ "[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
\<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|}
+ ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>, Y\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule set_cr.induct, auto)
@@ -398,11 +398,11 @@
text{*Ever used?*}
lemma CA_Says_2:
- "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
+ "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
\<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|}
+ ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>, Y\<rbrace>
\<in> set evs"
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
@@ -410,23 +410,23 @@
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|})
+ "[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
\<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"
+ ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>, Y\<rbrace> \<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|})
+ "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
\<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"
+ ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>, Y\<rbrace> \<in> set evs"
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
@@ -434,23 +434,23 @@
received CA's certificate.*}
lemma CA_Says_6_lemma:
"[| Crypt (priSK (CA i))
- (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
+ (Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
\<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"
+ ==> \<exists>Y K. Says (CA i) C (Crypt K \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>, Y\<rbrace>) \<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|})
+ "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
\<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"
+ ==> \<exists>Y K. Says (CA i) C (Crypt K \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>, Y\<rbrace>) \<in> set evs"
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
(*>*)
@@ -521,7 +521,7 @@
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|}
+ "[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs;
cardSK \<notin> symKeys; evs \<in> set_cr|]
==> Key cardSK \<in> analz (knows Spy evs) |
@@ -602,12 +602,12 @@
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|}
+ "[|Crypt (priSK (CA i)) \<lbrace>Hash \<lbrace>Nonce N, Pan(pan C)\<rbrace>, Key cardSK, N1\<rbrace>
\<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|})
+ \<lbrace>X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y\<rbrace>)
\<in> set evs"
apply (erule rev_mp)
apply (erule set_cr.induct)
@@ -618,12 +618,12 @@
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;
+ "[|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;
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|})
+ \<lbrace>X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y\<rbrace>)
\<in> set evs"
by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
certificate_valid_pubSK cert_valid_lemma)
@@ -631,7 +631,7 @@
lemma Hash_imp_parts [rule_format]:
"evs \<in> set_cr
- ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
+ ==> Hash\<lbrace>X, Nonce N\<rbrace> \<in> parts (knows Spy evs) -->
Nonce N \<in> parts (knows Spy evs)"
apply (erule set_cr.induct, force)
apply (simp_all (no_asm_simp))
@@ -640,7 +640,7 @@
lemma Hash_imp_parts2 [rule_format]:
"evs \<in> set_cr
- ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
+ ==> Hash\<lbrace>X, Nonce M, Y, Nonce N\<rbrace> \<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))
@@ -696,7 +696,7 @@
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|}
+ "[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs;
cardSK \<notin> symKeys; evs \<in> set_cr|]
==> Key cardSK \<in> analz (knows Spy evs) |
@@ -751,12 +751,12 @@
subsection{*Secrecy of CardSecret: the Cardholder's secret*}
lemma NC2_not_CardSecret:
- "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
+ "[|Crypt EKj \<lbrace>Key K, Pan p, Hash \<lbrace>Agent D, Nonce N\<rbrace>\<rbrace>
\<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)"
+ ==> Crypt EKi \<lbrace>Key K', Pan p', Nonce N\<rbrace> \<notin> parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
@@ -765,11 +765,11 @@
done
lemma KC2_secure_lemma [rule_format]:
- "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
+ "[|U = Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, X\<rbrace>;
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 &
+ (\<exists>k i W. Says (Cardholder k) (CA i) \<lbrace>U,W\<rbrace> \<in> set evs &
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)
@@ -783,7 +783,7 @@
done
lemma KC2_secrecy:
- "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
+ "[|Gets B \<lbrace>Crypt K \<lbrace>Agent C, Nonce N, Key KC2, X\<rbrace>, Y\<rbrace> \<in> set evs;
Nonce N \<notin> analz (knows Spy evs); KC2 \<in> symKeys;
evs \<in> set_cr|]
==> Key KC2 \<notin> analz (knows Spy evs)"
@@ -794,7 +794,7 @@
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|}
+ Crypt (pubEK (CA i)) \<lbrace>Key K, Pan p, Nonce CardSecret\<rbrace>
\<in> parts (knows Spy evs) -->
Nonce CardSecret \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
@@ -825,9 +825,9 @@
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;
+ \<lbrace>X, Crypt EKi \<lbrace>Key KC3, Pan p, Nonce CardSecret\<rbrace>\<rbrace> \<in> set evs;
+ Gets A \<lbrace>Z, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
KC3 \<in> symKeys; evs \<in> set_cr|]
==> Nonce CardSecret \<notin> analz (knows Spy evs)"
apply (frule Gets_certificate_valid, assumption)
@@ -841,11 +841,11 @@
subsection{*Secrecy of NonceCCA [the CA's secret] *}
lemma NC2_not_NonceCCA:
- "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
+ "[|Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace>
\<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)"
+ ==> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule set_cr.induct, analz_mono_contra, simp_all)
@@ -858,9 +858,9 @@
"[|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|}
+ \<lbrace>sign (priSK (CA i))
+ \<lbrace>Agent C, Nonce N, Agent(CA i), Nonce NonceCCA\<rbrace>,
+ X, Y\<rbrace>
\<in> parts (knows Spy evs) -->
Nonce NonceCCA \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
@@ -891,12 +891,12 @@
"[|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;
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce N, Agent(CA i), Nonce NonceCCA\<rbrace>,
+ X, Y\<rbrace>) \<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;
+ \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce NC3, Key KC2, X'\<rbrace>, Y'\<rbrace> \<in> set evs;
+ Gets A \<lbrace>Z, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
KC2 \<in> symKeys; evs \<in> set_cr|]
==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
apply (frule Gets_certificate_valid, assumption)
@@ -917,7 +917,7 @@
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|}
+ "[|Gets A \<lbrace>Crypt K \<lbrace>c, n, k', Key cardSK, X\<rbrace>, Y\<rbrace>
\<in> set evs; evs \<in> set_cr |]
==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
by auto
@@ -961,7 +961,7 @@
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|} |}
+ Says C (CA i) \<lbrace>X, Crypt (pubEK (CA i)) \<lbrace>Key K, Pan (pan C), HN\<rbrace> \<rbrace>
\<in> set evs
& (CA i) \<in> bad"
apply (erule rev_mp)
@@ -985,9 +985,9 @@
lemma CR6_Says_imp_Notes:
"[|Says (CA i) C (Crypt KC2
- {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce Y\<rbrace>,
certC (pan C) cardSK X onlySig (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}) \<in> set evs;
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>) \<in> set evs;
evs \<in> set_cr |]
==> Notes (CA i) (Key cardSK) \<in> set evs"
apply (erule rev_mp)
@@ -999,14 +999,14 @@
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|},
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce Y\<rbrace>,
certC (pan C) cardSK X onlySig (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
\<in> set evs;
Says (CA i) C' (Crypt KC2'
- {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
+ \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C', Nonce NC3', Agent (CA i), Nonce Y'\<rbrace>,
certC (pan C') cardSK X' onlySig (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
\<in> set evs;
evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
apply (erule rev_mp)
@@ -1020,9 +1020,9 @@
(*<*)
text{*UNUSED unicity result*}
lemma unique_KC1:
- "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
+ "[|Says C B \<lbrace>Crypt KC1 X, Crypt EK \<lbrace>Key KC1, Y\<rbrace>\<rbrace>
\<in> set evs;
- Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
+ Says C B' \<lbrace>Crypt KC1 X', Crypt EK' \<lbrace>Key KC1, Y'\<rbrace>\<rbrace>
\<in> set evs;
C \<notin> bad; evs \<in> set_cr|] ==> B'=B & Y'=Y"
apply (erule rev_mp)
@@ -1032,8 +1032,8 @@
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;
+ "[|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;
C \<notin> bad; evs \<in> set_cr|] ==> B'=B & X'=X"
apply (erule rev_mp)
apply (erule rev_mp)
--- a/src/HOL/SET_Protocol/Merchant_Registration.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Merchant_Registration.thy Wed Dec 30 18:17:28 2015 +0100
@@ -36,16 +36,16 @@
| 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"
+ ==> Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> # 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|},
+ Gets (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<in> set evs2 |]
+ ==> Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM1, Nonce NCA\<rbrace>,
cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) \<rbrace>
# evs2 \<in> set_mr"
| SET_MR3:
@@ -57,16 +57,16 @@
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|},
+ Gets M \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NM1, Nonce NCA\<rbrace>,
cert (CA i) EKi onlyEnc (priSK RCA),
- cert (CA i) SKi onlySig (priSK RCA) |}
+ cert (CA i) SKi onlySig (priSK RCA) \<rbrace>
\<in> set evs3;
- Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
+ Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<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)|}
+ \<lbrace>Crypt KM1 (sign (priSK M) \<lbrace>Agent M, Nonce NM2,
+ Key (pubSK M), Key (pubEK M)\<rbrace>),
+ Crypt EKi (Key KM1)\<rbrace>
+ # Notes M \<lbrace>Key KM1, Agent (CA i)\<rbrace>
# evs3 \<in> set_mr"
| SET_MR4:
@@ -80,14 +80,14 @@
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) |}
+ Gets (CA i) \<lbrace>Crypt KM1 (sign (invKey merSK)
+ \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>),
+ Crypt (pubEK (CA i)) (Key KM1) \<rbrace>
\<in> set evs4 |]
- ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
+ ==> Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent(CA i)\<rbrace>,
cert M merSK onlySig (priSK (CA i)),
cert M merEK onlyEnc (priSK (CA i)),
- cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
# Notes (CA i) (Key merSK)
# Notes (CA i) (Key merEK)
# evs4 \<in> set_mr"
@@ -148,7 +148,7 @@
they hold, as in CR, because RCA's keys are secure*}
lemma Crypt_valid_pubEK:
- "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key EKi, onlyEnc\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
apply (erule rev_mp)
@@ -164,7 +164,7 @@
done
lemma Crypt_valid_pubSK:
- "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key SKi, onlySig\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
apply (erule rev_mp)
@@ -179,8 +179,8 @@
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;
+ "[| Gets A \<lbrace> X, cert (CA i) EKi onlyEnc (priSK RCA),
+ cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
evs \<in> set_mr |]
==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
@@ -261,9 +261,9 @@
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;
+ "[|Gets B \<lbrace>Crypt KM1
+ (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>),
+ Y\<rbrace> \<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))"
@@ -320,10 +320,10 @@
subsection{*Unicity *}
lemma msg4_Says_imp_Notes:
- "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
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;
+ cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
evs \<in> set_mr |]
==> Notes (CA i) (Key merSK) \<in> set evs
& Notes (CA i) (Key merEK) \<in> set evs"
@@ -335,14 +335,14 @@
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)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
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 (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
+ Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>,
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;
+ cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
apply (erule rev_mp)
apply (erule rev_mp)
@@ -354,14 +354,14 @@
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)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
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 (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
+ Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>,
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;
+ cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
evs \<in> set_mr |]
==> M=M' & NM2=NM2' & merSK=merSK'"
apply (erule rev_mp)
@@ -386,11 +386,11 @@
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|}
+ "[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merSK, onlySig\<rbrace>
\<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"
+ \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule set_mr.induct)
apply (simp_all (no_asm_simp))
@@ -401,15 +401,15 @@
"[| 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"
+ \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs"
by auto
lemma certificate_merEK_valid_lemma [intro]:
- "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
+ "[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merEK, onlyEnc\<rbrace>
\<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"
+ \<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule set_mr.induct)
apply (simp_all (no_asm_simp))
@@ -420,7 +420,7 @@
"[| 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"
+ \<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs"
by auto
text{*The two certificates - for merSK and for merEK - cannot be proved to
--- a/src/HOL/SET_Protocol/Message_SET.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Wed Dec 30 18:17:28 2015 +0100
@@ -67,16 +67,12 @@
| Crypt key msg --{*Encryption, public- or shared-key*}
-(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
+(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, 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|}" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
definition nat_of_agent :: "agent => nat" where
@@ -104,8 +100,8 @@
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
@@ -180,7 +176,7 @@
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"
+lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Crypt [simp]:
@@ -197,7 +193,7 @@
subsection{*Inductive relation "parts"*}
lemma MPair_parts:
- "[| {|X,Y|} \<in> parts H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
[| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
by (blast dest: parts.Fst parts.Snd)
@@ -346,8 +342,8 @@
done
lemma parts_insert_MPair [simp]:
- "parts (insert {|X,Y|} H) =
- insert {|X,Y|} (parts (insert X (insert Y H)))"
+ "parts (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
@@ -398,8 +394,8 @@
for H :: "msg set"
where
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"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
| Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -413,7 +409,7 @@
text{*Making it safe speeds up proofs*}
lemma MPair_analz [elim!]:
- "[| {|X,Y|} \<in> analz H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
[| X \<in> analz H; Y \<in> analz H |] ==> P
|] ==> P"
by (blast dest: analz.Fst analz.Snd)
@@ -497,8 +493,8 @@
done
lemma analz_insert_MPair [simp]:
- "analz (insert {|X,Y|} H) =
- insert {|X,Y|} (analz (insert X (insert Y H)))"
+ "analz (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct, auto)
@@ -619,7 +615,7 @@
(*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"
+ "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
apply safe
apply (erule analz.induct, blast+)
done
@@ -650,7 +646,7 @@
| 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"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
| Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
(*Monotonicity*)
@@ -664,7 +660,7 @@
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 MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
inductive_cases Pan_synth [elim!]: "Pan A \<in> synth H"
@@ -790,7 +786,7 @@
(*Without this equation, other rules for synth and analz would yield
redundant cases*)
lemma MPair_synth_analz [iff]:
- "({|X,Y|} \<in> synth (analz H)) =
+ "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
(X \<in> synth (analz H) & Y \<in> synth (analz H))"
by blast
@@ -802,7 +798,7 @@
lemma Hash_synth_analz [simp]:
"X \<notin> synth (analz H)
- ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+ ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
by blast
--- a/src/HOL/SET_Protocol/Public_SET.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Dec 30 18:17:28 2015 +0100
@@ -128,7 +128,7 @@
definition
(* Signature = Message + signed Digest *)
sign :: "[key, msg]=>msg"
- where "sign K X = {|X, Crypt K (Hash X) |}"
+ where "sign K X = \<lbrace>X, Crypt K (Hash X) \<rbrace>"
definition
(* Signature Only = signed Digest Only *)
@@ -138,7 +138,7 @@
definition
(* Signature for Certificates = Message + signed Message *)
signCert :: "[key, msg]=>msg"
- where "signCert K X = {|X, Crypt K X |}"
+ where "signCert K X = \<lbrace>X, Crypt K X \<rbrace>"
definition
(* Certification Authority's Certificate.
@@ -149,7 +149,7 @@
then Ka=pubEK i or pubSK i depending on T ??
*)
cert :: "[agent, key, msg, key] => msg"
- where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"
+ where "cert A Ka T signK = signCert signK \<lbrace>Agent A, Key Ka, T\<rbrace>"
definition
(* Cardholder's Certificate.
@@ -158,7 +158,7 @@
*)
certC :: "[nat, key, nat, msg, key] => msg"
where "certC PAN Ka PS T signK =
- signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
+ signCert signK \<lbrace>Hash \<lbrace>Nonce PS, Pan PAN\<rbrace>, Key Ka, T\<rbrace>"
(*cert and certA have no repeated elements, so they could be abbreviations,
but that's tricky and makes proofs slower*)
@@ -173,13 +173,13 @@
--{*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|}|}"
+ \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m\<rbrace>\<rbrace>"
definition EXHcrypt :: "[key,key,msg,msg] => msg" where
--{*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|}|}"
+ \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m, Hash M\<rbrace>\<rbrace>"
definition Enc :: "[key,key,key,msg] => msg" where
--{*Simple Encapsulation with SIGNATURE*}
@@ -187,12 +187,12 @@
K: the symmetric key
EK: the public encryption key*)
"Enc SK K EK M =
- {|Crypt K (sign SK M), Crypt EK (Key K)|}"
+ \<lbrace>Crypt K (sign SK M), Crypt EK (Key K)\<rbrace>"
definition EncB :: "[key,key,key,msg,msg] => msg" where
--{*Encapsulation with Baggage. Keys as above, and baggage b.*}
"EncB SK K EK M b =
- {|Enc SK K EK {|M, Hash b|}, b|}"
+ \<lbrace>Enc SK K EK \<lbrace>M, Hash b\<rbrace>, b\<rbrace>"
subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
@@ -416,13 +416,13 @@
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))"
+ insert \<lbrace>X, Crypt K X\<rbrace> (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)))"
+ insert \<lbrace>X, Crypt K X\<rbrace> (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"
@@ -463,7 +463,7 @@
lemma EncB_partsE:
"!!R. [|EncB SK K EK M b \<in> parts H;
- [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;
+ [|Crypt K (sign SK \<lbrace>M, Hash b\<rbrace>) \<in> parts H;
Crypt EK (Key K) \<in> parts H;
b \<in> parts H|] ==> R|]
==> R"
@@ -471,8 +471,8 @@
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|]
+ [|Crypt K \<lbrace>M, Hash m\<rbrace> \<in> parts H;
+ Crypt EK \<lbrace>Key K, m\<rbrace> \<in> parts H|] ==> R|]
==> R"
by (unfold EXcrypt_def, blast)
--- a/src/HOL/SET_Protocol/Purchase.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy Wed Dec 30 18:17:28 2015 +0100
@@ -86,38 +86,38 @@
"[|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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
LID_M \<notin> range CardSecret;
LID_M \<notin> range PANSecret |]
- ==> Notes C {|Number LID_M, Transaction|}
- # Notes M {|Number LID_M, Agent P, Transaction|}
+ ==> Notes C \<lbrace>Number LID_M, Transaction\<rbrace>
+ # Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
# 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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
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"
+ Notes C \<lbrace>Number LID_M, Transaction \<rbrace> \<in> set evsPIReq |]
+ ==> Says C M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> # 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;
+ Gets M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPIRes;
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+ Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace> \<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,
+ \<lbrace>Number LID_M, Number XID,
Nonce Chall_C, Nonce Chall_M,
- cert P (pubEK P) onlyEnc (priSK RCA)|})
+ cert P (pubEK P) onlyEnc (priSK RCA)\<rbrace>)
# evsPIRes \<in> set_pur"
| PReqUns:
@@ -125,34 +125,34 @@
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
+ \<open>Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<close> from PIHead because
the CardSecret is 0 and because AuthReq treated the unsigned case
very differently from the signed one anyway.*}
"!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
[|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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+ HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+ OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M\<rbrace>;
Gets C (sign (priSK M)
- {|Number LID_M, Number XID,
+ \<lbrace>Number LID_M, Number XID,
Nonce Chall_C, Nonce Chall_M,
- cert P EKj onlyEnc (priSK RCA)|})
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>)
\<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 \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPReqU;
+ Notes C \<lbrace>Number LID_M, Transaction\<rbrace> \<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|}
+ \<lbrace>EXHcrypt KC1 EKj \<lbrace>PIHead, Hash OIData\<rbrace> (Pan (pan C)),
+ OIData, Hash\<lbrace>PIHead, Pan (pan C)\<rbrace> \<rbrace>
+ # Notes C \<lbrace>Key KC1, Agent M\<rbrace>
# 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
+ @{term "PIReqSigned = \<lbrace> PIDualSigned, OIDualSigned \<rbrace>"}, 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.*}
@@ -162,25 +162,25 @@
[|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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+ HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+ OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<rbrace>;
+ PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+ PIData = \<lbrace>PIHead, PANData\<rbrace>;
+ PIDualSigned = \<lbrace>sign (priSK C) \<lbrace>Hash PIData, Hash OIData\<rbrace>,
+ EXcrypt KC2 EKj \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>;
+ OIDualSigned = \<lbrace>OIData, Hash PIData\<rbrace>;
Gets C (sign (priSK M)
- {|Number LID_M, Number XID,
+ \<lbrace>Number LID_M, Number XID,
Nonce Chall_C, Nonce Chall_M,
- cert P EKj onlyEnc (priSK RCA)|})
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>)
\<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|}
+ Says C M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPReqS;
+ Notes C \<lbrace>Number LID_M, Transaction\<rbrace> \<in> set evsPReqS |]
+ ==> Says C M \<lbrace>PIDualSigned, OIDualSigned\<rbrace>
+ # Notes C \<lbrace>Key KC2, Agent M\<rbrace>
# evsPReqS \<in> set_pur"
--{*Authorization Request. Page 92 of Formal Protocol Desc.
@@ -188,22 +188,22 @@
| 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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+ HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+ OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD,
+ Nonce Chall_M\<rbrace>;
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,
+ P_I = \<lbrace>sign (priSK C) \<lbrace>HPIData, Hash OIData\<rbrace>, encPANData\<rbrace>;
+ Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evsAReq;
+ Says M C (sign (priSK M) \<lbrace>Number LID_M, Number XID,
Nonce Chall_C, Nonce Chall_M,
- cert P EKj onlyEnc (priSK RCA)|})
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>)
\<in> set evsAReq;
- Notes M {|Number LID_M, Agent P, Transaction|}
+ Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
\<in> set evsAReq |]
==> Says M P
(EncB (priSK M) KM (pubEK P)
- {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
+ \<lbrace>Number LID_M, Number XID, Hash OIData, HOD\<rbrace> P_I)
# evsAReq \<in> set_pur"
--{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
@@ -220,14 +220,14 @@
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));
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M\<rbrace>;
+ P_I = EXHcrypt KC1 EKj \<lbrace>PIHead, HOIData\<rbrace> (Pan (pan C));
Gets P (EncB (priSK M) KM (pubEK P)
- {|Number LID_M, Number XID, HOIData, HOD|} P_I)
+ \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace> P_I)
\<in> set evsAResU |]
==> Says P M
(EncB (priSK P) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
authCode)
# evsAResU \<in> set_pur"
@@ -237,41 +237,41 @@
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)|}|};
+ P_I = \<lbrace>sign (priSK C) \<lbrace>Hash PIData, HOIData\<rbrace>,
+ EXcrypt KC2 (pubEK P) \<lbrace>PIHead, HOIData\<rbrace> PANData\<rbrace>;
+ PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+ PIData = \<lbrace>PIHead, PANData\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<rbrace>;
Gets P (EncB (priSK M) KM (pubEK P)
- {|Number LID_M, Number XID, HOIData, HOD|}
+ \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>
P_I)
\<in> set evsAResS |]
==> Says P M
(EncB (priSK P) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
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|};
+ Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
Gets M (EncB (priSK P) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
authCode)
\<in> set evsPRes;
- Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
+ Gets M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPRes;
Says M P
(EncB (priSK M) KM (pubEK P)
- {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
+ \<lbrace>Number LID_M, Number XID, Hash OIData, HOD\<rbrace> P_I)
\<in> set evsPRes;
- Notes M {|Number LID_M, Agent P, Transaction|}
+ Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
\<in> set evsPRes
|]
==> Says M C
- (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
- Hash (Number PurchAmt)|})
+ (sign (priSK M) \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)\<rbrace>)
# evsPRes \<in> set_pur"
@@ -320,8 +320,8 @@
==> \<exists>evs \<in> set_pur.
Says M C
(sign (priSK M)
- {|Number LID_M, Number XID, Nonce Chall_C,
- Hash (Number PurchAmt)|})
+ \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)\<rbrace>)
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
@@ -356,8 +356,8 @@
LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |]
==> \<exists>evs \<in> set_pur.
Says M C
- (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
- Hash (Number PurchAmt)|})
+ (sign (priSK M) \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)\<rbrace>)
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
@@ -395,12 +395,12 @@
text{*Forwarding lemmas, to aid simplification*}
lemma AuthReq_msg_in_parts_spies:
- "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
+ "[|Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<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;
+ "[|Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evs;
evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
@@ -443,13 +443,13 @@
subsection{*Public Keys in Certificates are Correct*}
lemma Crypt_valid_pubEK [dest!]:
- "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent C, Key EKi, onlyEnc\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_pur |] ==> EKi = pubEK C"
by (erule rev_mp, erule set_pur.induct, auto)
lemma Crypt_valid_pubSK [dest!]:
- "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+ "[| Crypt (priSK RCA) \<lbrace>Agent C, Key SKi, onlySig\<rbrace>
\<in> parts (knows Spy evs);
evs \<in> set_pur |] ==> SKi = pubSK C"
by (erule rev_mp, erule set_pur.induct, auto)
@@ -466,15 +466,15 @@
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;
+ "[| Says A B (sign SK \<lbrace>lid, xid, cc, cm,
+ cert C EK onlyEnc (priSK RCA)\<rbrace>) \<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;
+ "[| Gets A (sign SK \<lbrace>lid, xid, cc, cm,
+ cert C EK onlyEnc (priSK RCA)\<rbrace>) \<in> set evs;
evs \<in> set_pur |]
==> EK = pubEK C"
by (frule Gets_imp_Says, auto)
@@ -607,8 +607,8 @@
==>
(\<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)"
+ \<lbrace>\<lbrace>W, EXcrypt KC2 (pubEK P) X \<lbrace>Y, Nonce (PANSecret k)\<rbrace>\<rbrace>,
+ V\<rbrace> \<in> set evs)"
apply (erule rev_mp)
apply (erule set_pur.induct)
apply (frule_tac [9] AuthReq_msg_in_analz_spies)
@@ -679,7 +679,7 @@
"[| 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|}
+ Says C M \<lbrace>EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y\<rbrace>
\<in> set evs &
P \<in> bad"
apply (erule rev_mp)
@@ -703,9 +703,9 @@
"[|Pan (pan C) \<in> analz(knows Spy evs); C = Cardholder k;
CardSecret k \<noteq> 0; evs \<in> set_pur|]
==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.
- Says C M {|{|PIDualSign_1,
- EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|},
- OIDualSign|} \<in> set evs & P \<in> bad"
+ Says C M \<lbrace>\<lbrace>PIDualSign_1,
+ EXcrypt KC2 (pubEK P) PIDualSign_2 \<lbrace>Pan (pan C), other\<rbrace>\<rbrace>,
+ OIDualSign\<rbrace> \<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*}
@@ -730,7 +730,7 @@
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;
+ "[|Notes M \<lbrace>Number LID_M, Agent P, Agent M, Agent C, etc\<rbrace> \<in> set evs;
evs \<in> set_pur|] ==> \<exists>j. P = PG j"
by (erule rev_mp, erule set_pur.induct, simp_all)
@@ -738,12 +738,12 @@
(Payment Gateway)*}
lemma goodM_gives_correct_PG:
"[| MsgPInitRes =
- {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
+ \<lbrace>Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)\<rbrace>;
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"
+ Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule set_pur.induct)
@@ -753,23 +753,23 @@
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;
+ "[| Gets A (sign (priSK M) \<lbrace>Number LID_M, xid, cc, cm,
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>) \<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 &
+ Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<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)|};
+ "[| MsgPInitRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>;
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 &
+ Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs &
P = PG j &
EKj = pubEK P"
apply clarify
@@ -783,12 +783,12 @@
text{*Corollary of previous one*}
lemma Says_C_PInitRes:
"[|Says A C (sign (priSK M)
- {|Number LID_M, Number XID,
+ \<lbrace>Number LID_M, Number XID,
Nonce Chall_C, Nonce Chall_M,
- cert P EKj onlyEnc (priSK RCA)|})
+ cert P EKj onlyEnc (priSK RCA)\<rbrace>)
\<in> set evs; M \<notin> bad; evs \<in> set_pur|]
==> \<exists>j trans.
- Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+ Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs &
P = PG j &
EKj = pubEK (PG j)"
apply (frule Says_certificate_valid)
@@ -800,13 +800,13 @@
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|})
+ "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
+ Crypt (priSK M) (Hash \<lbrace>AuthReqData, Hash P_I\<rbrace>)
\<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 &
+ Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
+ Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evs &
Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
\<in> set evs"
apply clarify
@@ -825,18 +825,18 @@
@{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
otherwise the Spy could create that message.*}
theorem M_verifies_AuthRes:
- "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|},
- Hash authCode|};
+ "[| MsgAuthRes = \<lbrace>\<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>,
+ Hash authCode\<rbrace>;
Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
PG j \<notin> bad; evs \<in> set_pur|]
==> \<exists>M KM KP HOIData HOD P_I.
Gets (PG j)
(EncB (priSK M) KM (pubEK (PG j))
- {|Number LID_M, Number XID, HOIData, HOD|}
+ \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>
P_I) \<in> set evs &
Says (PG j) M
(EncB (priSK (PG j)) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
authCode) \<in> set evs"
apply clarify
apply (erule rev_mp)
@@ -852,12 +852,12 @@
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|};
+ "[| Says C M \<lbrace>EXHcrypt KC1 EKj \<lbrace>PIHead, Hash OIData\<rbrace> (Pan (pan C)),
+ OIData, Hash\<lbrace>PIHead, Pan (pan C)\<rbrace> \<rbrace> \<in> set evs;
+ PIHead = \<lbrace>Number LID_M, Trans_details\<rbrace>;
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 &
+ Notes M \<lbrace>Number LID_M, Agent (PG j), trans \<rbrace> \<in> set evs &
EKj = pubEK (PG j)"
apply clarify
apply (erule rev_mp)
@@ -870,11 +870,11 @@
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;
+ "[|Notes (Merchant i) \<lbrace>Number LID_M, Agent P, Trans\<rbrace> \<in> set evs;
+ Notes C \<lbrace>Number LID_M, Agent M, Agent C, Number OD,
+ Number PA\<rbrace> \<in> set evs;
evs \<in> set_pur|]
- ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
+ ==> M = Merchant i & Trans = \<lbrace>Agent M, Agent C, Number OD, Number PA\<rbrace>"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule set_pur.induct, simp_all)
@@ -883,8 +883,8 @@
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;
+ "[|Notes M \<lbrace>Number LID_M, Trans\<rbrace> \<in> set evs;
+ Notes M \<lbrace>Number LID_M, Trans'\<rbrace> \<in> set evs;
evs \<in> set_pur|] ==> Trans' = Trans"
apply (erule rev_mp)
apply (erule rev_mp)
@@ -907,7 +907,7 @@
text{*Similar, with nested Hash*}
lemma signed_Hash_imp_used:
- "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
+ "[| Crypt (priSK C) (Hash \<lbrace>H, Hash X\<rbrace>) \<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)
@@ -920,7 +920,7 @@
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);
+ "[| Crypt (priSK M) (Hash \<lbrace>N, X\<rbrace>) \<in> parts (knows Spy evs);
M \<notin> bad; evs \<in> set_pur|] ==> N \<in> used evs"
by (drule signed_imp_used, auto)
@@ -928,16 +928,16 @@
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)|};
+ Notes C \<lbrace>Number LID_M, Trans \<rbrace> \<in> set evs;
+ Trans = \<lbrace> Agent M, Agent C, Number OrderDesc, Number PurchAmt \<rbrace>;
+ MsgPRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)\<rbrace>;
evs \<in> set_pur; M \<notin> bad|]
==> \<exists>j KP.
- Notes M {|Number LID_M, Agent (PG j), Trans |}
+ Notes M \<lbrace>Number LID_M, Agent (PG j), Trans \<rbrace>
\<in> set evs &
Gets M (EncB (priSK (PG j)) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
authCode)
\<in> set evs &
Says M C (sign (priSK M) MsgPRes) \<in> set evs"
@@ -958,16 +958,16 @@
Merchant, he knows that M sent it. He also knows that M received a message signed
by a Payment Gateway chosen by M to authorize the purchase.*}
theorem C_verifies_PRes:
- "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
- Hash (Number PurchAmt)|};
+ "[| MsgPRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)\<rbrace>;
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;
+ Notes C \<lbrace>Number LID_M, Agent M, Agent C, Number OrderDesc,
+ Number PurchAmt\<rbrace> \<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 &
+ Notes M \<lbrace>Number LID_M,Agent P, trans\<rbrace> \<in> set evs &
Gets M (EncB (priSK P) KP (pubEK M)
- {|Number LID_M, Number XID, Number PurchAmt|}
+ \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
authCode) \<in> set evs &
Says M C (sign (priSK M) MsgPRes) \<in> set evs"
apply (rule C_verifies_PRes_lemma [THEN exE])
@@ -979,17 +979,17 @@
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|}
+ "[| Crypt K \<lbrace>\<lbrace>\<lbrace>Number LID_M, others\<rbrace>, Hash OIData\<rbrace>, Hash PANData\<rbrace>
\<in> parts (knows Spy evs);
- PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
+ PANData = \<lbrace>Pan (pan (Cardholder k)), Nonce (PANSecret k)\<rbrace>;
Key K \<notin> analz (knows Spy evs);
evs \<in> set_pur|]
==> \<exists>M shash EK HPIData.
- Says (Cardholder k) M {|{|shash,
+ Says (Cardholder k) M \<lbrace>\<lbrace>shash,
Crypt K
- {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
- Crypt EK {|Key K, PANData|}|},
- OIData, HPIData|} \<in> set evs"
+ \<lbrace>\<lbrace>\<lbrace>Number LID_M, others\<rbrace>, Hash OIData\<rbrace>, Hash PANData\<rbrace>,
+ Crypt EK \<lbrace>Key K, PANData\<rbrace>\<rbrace>,
+ OIData, HPIData\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
@@ -1000,15 +1000,15 @@
done
lemma Says_PReqS_imp_trans_details_C:
- "[| MsgPReqS = {|{|shash,
+ "[| MsgPReqS = \<lbrace>\<lbrace>shash,
Crypt K
- {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
- cryptek|}, data|};
+ \<lbrace>\<lbrace>\<lbrace>Number LID_M, PIrest\<rbrace>, Hash OIData\<rbrace>, hashpd\<rbrace>,
+ cryptek\<rbrace>, data\<rbrace>;
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|}
+ \<lbrace>Number LID_M, Agent M, Agent (Cardholder k), trans\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule rev_mp)
@@ -1020,7 +1020,7 @@
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;
+ \<lbrace>Number n, Agent P, Agent (Cardholder k), Agent C, etc\<rbrace> \<in> set evs;
evs \<in> set_pur|] ==> False"
by (erule rev_mp, erule set_pur.induct, auto)
@@ -1028,14 +1028,14 @@
Using XID he knows it was intended for him.
This guarantee isn't useful to P, who never gets OIData.*}
theorem M_verifies_Signed_PReq:
- "[| MsgDualSign = {|HPIData, Hash OIData|};
- OIData = {|Number LID_M, etc|};
+ "[| MsgDualSign = \<lbrace>HPIData, Hash OIData\<rbrace>;
+ OIData = \<lbrace>Number LID_M, etc\<rbrace>;
Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
- Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
+ Notes M \<lbrace>Number LID_M, Agent P, extras\<rbrace> \<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|}
+ Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign, PICrypt\<rbrace>, OIData, Hash PIData\<rbrace>
\<in> set evs"
apply clarify
apply (erule rev_mp)
@@ -1054,20 +1054,20 @@
PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
assuming @{term "M \<notin> bad"}.*}
theorem P_verifies_Signed_PReq:
- "[| MsgDualSign = {|Hash PIData, HOIData|};
- PIData = {|PIHead, PANData|};
- PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
- TransStain|};
+ "[| MsgDualSign = \<lbrace>Hash PIData, HOIData\<rbrace>;
+ PIData = \<lbrace>PIHead, PANData\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain\<rbrace>;
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|} &
+ HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace> &
HOIData = Hash OIData &
- Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
- Says C M {|{|sign (priSK C) MsgDualSign,
+ Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
+ Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign,
EXcrypt K (pubEK (PG j))
- {|PIHead, Hash OIData|} PANData|},
- OIData, Hash PIData|}
+ \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>,
+ OIData, Hash PIData\<rbrace>
\<in> set evs"
apply clarify
apply (erule rev_mp)
@@ -1076,12 +1076,12 @@
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|};
+ "[| Says C M \<lbrace>\<lbrace>sign (priSK C) text,
+ EXcrypt K EKj \<lbrace>PIHead, X\<rbrace> Y\<rbrace>, Z\<rbrace> \<in> set evs;
+ PIHead = \<lbrace>Number LID_M, Number XID, W\<rbrace>;
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 &
+ Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
EKj = pubEK (PG j)"
apply clarify
apply (erule rev_mp)
@@ -1090,11 +1090,11 @@
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);
+ "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
+ sign (priSK M) \<lbrace>AuthReqData, Hash P_I\<rbrace> \<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 &
+ Notes M \<lbrace>Number LID_M, Agent (PG j), trans \<rbrace> \<in> set evs &
Says M (PG j)
(EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
\<in> set evs"
@@ -1106,17 +1106,17 @@
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|};
+ "[| MsgDualSign = \<lbrace>Hash PIData, Hash OIData\<rbrace>;
+ OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD, etc\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain\<rbrace>;
+ PIData = \<lbrace>PIHead, PANData\<rbrace>;
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|}
+ Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign,
+ EXcrypt KC EKj \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>,
+ OIData, Hash PIData\<rbrace>
\<in> set evs"
apply clarify
apply hypsubst_thin
@@ -1128,7 +1128,7 @@
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|}"}
+ @{term "HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>"}
and P compares the two copies of HOD.
Agreement can't be proved for some things, including the symmetric keys
@@ -1137,30 +1137,30 @@
the EXcrypt involves the correct PG's key.
*}
theorem P_sees_CM_agreement:
- "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
+ "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
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|};
+ PI_sign = sign (priSK C) \<lbrace>Hash PIData, HOIData\<rbrace>;
+ P_I = \<lbrace>PI_sign,
+ EXcrypt KC (pubEK (PG j)) \<lbrace>PIHead, HOIData\<rbrace> PANData\<rbrace>;
+ PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+ PIData = \<lbrace>PIHead, PANData\<rbrace>;
+ PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+ TransStain\<rbrace>;
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|} &
+ HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace> &
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 &
+ Notes M \<lbrace>Number LID_M, Agent (PG j'), trans\<rbrace> \<in> set evs &
+ Says C M \<lbrace>P_I', OIData, Hash PIData\<rbrace> \<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|}"
+ P_I' = \<lbrace>PI_sign,
+ EXcrypt KC' (pubEK (PG j')) \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace> &
+ P_I'' = \<lbrace>PI_sign,
+ EXcrypt KC'' (pubEK (PG j)) \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>"
apply clarify
apply (rule exE)
apply (rule P_verifies_Signed_PReq [OF refl refl refl])