--- a/src/HOL/Auth/CertifiedEmail.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/CertifiedEmail.thy Mon Dec 28 23:13:33 2015 +0100
@@ -25,7 +25,7 @@
text\<open>We formalize a fixed way of computing responses. Could be better.\<close>
definition "response" :: "agent => agent => nat => msg" where
- "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"
+ "response S R q == Hash \<lbrace>Agent S, Key (shrK R), Nonce q\<rbrace>"
inductive_set certified_mail :: "event list set"
@@ -42,28 +42,28 @@
| FakeSSL: \<comment>\<open>The Spy may open SSL sessions with TTP, who is the only agent
equipped with the necessary credentials to serve as an SSL server.\<close>
"[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
- ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
+ ==> Notes TTP \<lbrace>Agent Spy, Agent TTP, X\<rbrace> # evsfssl \<in> certified_mail"
| CM1: \<comment>\<open>The sender approaches the recipient. The message is a number.\<close>
"[|evs1 \<in> certified_mail;
Key K \<notin> used evs1;
K \<in> symKeys;
Nonce q \<notin> used evs1;
- hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
- S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
- ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth,
- Number cleartext, Nonce q, S2TTP|} # evs1
+ hs = Hash\<lbrace>Number cleartext, Nonce q, response S R q, Crypt K (Number m)\<rbrace>;
+ S2TTP = Crypt(pubEK TTP) \<lbrace>Agent S, Number BothAuth, Key K, Agent R, hs\<rbrace>|]
+ ==> Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number BothAuth,
+ Number cleartext, Nonce q, S2TTP\<rbrace> # evs1
\<in> certified_mail"
| CM2: \<comment>\<open>The recipient records @{term S2TTP} while transmitting it and her
password to @{term TTP} over an SSL channel.\<close>
"[|evs2 \<in> certified_mail;
- Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext,
- Nonce q, S2TTP|} \<in> set evs2;
+ Gets R \<lbrace>Agent S, Agent TTP, em, Number BothAuth, Number cleartext,
+ Nonce q, S2TTP\<rbrace> \<in> set evs2;
TTP \<noteq> R;
- hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
+ hr = Hash \<lbrace>Number cleartext, Nonce q, response S R q, em\<rbrace> |]
==>
- Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
+ Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> # evs2
\<in> certified_mail"
| CM3: \<comment>\<open>@{term TTP} simultaneously reveals the key to the recipient and gives
@@ -72,12 +72,12 @@
if the given password is that of the claimed sender, @{term R}.
He replies over the established SSL channel.\<close>
"[|evs3 \<in> certified_mail;
- Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs3;
+ Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> \<in> set evs3;
S2TTP = Crypt (pubEK TTP)
- {|Agent S, Number BothAuth, Key k, Agent R, hs|};
+ \<lbrace>Agent S, Number BothAuth, Key k, Agent R, hs\<rbrace>;
TTP \<noteq> R; hs = hr; k \<in> symKeys|]
==>
- Notes R {|Agent TTP, Agent R, Key k, hr|} #
+ Notes R \<lbrace>Agent TTP, Agent R, Key k, hr\<rbrace> #
Gets S (Crypt (priSK TTP) S2TTP) #
Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
@@ -116,8 +116,8 @@
done
lemma CM2_S2TTP_analz_knows_Spy:
- "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext,
- Nonce q, S2TTP|} \<in> set evs;
+ "[|Gets R \<lbrace>Agent A, Agent B, em, Number AO, Number cleartext,
+ Nonce q, S2TTP\<rbrace> \<in> set evs;
evs \<in> certified_mail|]
==> S2TTP \<in> analz(spies evs)"
apply (drule Gets_imp_Says, simp)
@@ -130,9 +130,9 @@
lemma hr_form_lemma [rule_format]:
"evs \<in> certified_mail
==> hr \<notin> synth (analz (spies evs)) -->
- (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
+ (\<forall>S2TTP. Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace>
\<in> set evs -->
- (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
+ (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>))"
apply (erule certified_mail.induct)
apply (synth_analz_mono_contra, simp_all, blast+)
done
@@ -141,10 +141,10 @@
the fakessl rule allows Spy to spoof the sender's name. Maybe can
strengthen the second disjunct with @{term "R\<noteq>Spy"}.\<close>
lemma hr_form:
- "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
+ "[|Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace> \<in> set evs;
evs \<in> certified_mail|]
==> hr \<in> synth (analz (spies evs)) |
- (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
+ (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>)"
by (blast intro: hr_form_lemma)
lemma Spy_dont_know_private_keys [dest!]:
@@ -184,9 +184,9 @@
lemma CM3_k_parts_knows_Spy:
"[| evs \<in> certified_mail;
- Notes TTP {|Agent A, Agent TTP,
- Crypt (pubEK TTP) {|Agent S, Number AO, Key K,
- Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
+ Notes TTP \<lbrace>Agent A, Agent TTP,
+ Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K,
+ Agent R, hs\<rbrace>, Key (RPwd R), hs\<rbrace> \<in> set evs|]
==> Key K \<in> parts(spies evs)"
apply (rotate_tac 1)
apply (erule rev_mp)
@@ -273,7 +273,7 @@
provided @{term K} is secure. Proof is surprisingly hard.\<close>
lemma Notes_SSL_imp_used:
- "[|Notes B {|Agent A, Agent B, X|} \<in> set evs|] ==> X \<in> used evs"
+ "[|Notes B \<lbrace>Agent A, Agent B, X\<rbrace> \<in> set evs|] ==> X \<in> used evs"
by (blast dest!: Notes_imp_used)
@@ -283,14 +283,14 @@
"evs \<in> certified_mail ==>
Key K \<notin> analz (spies evs) -->
(\<forall>AO. Crypt (pubEK TTP)
- {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
+ \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs -->
(\<exists>m ctxt q.
- hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
+ hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
Says S R
- {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number ctxt, Nonce q,
Crypt (pubEK TTP)
- {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))"
+ \<lbrace>Agent S, Number AO, Key K, Agent R, hs \<rbrace>\<rbrace> \<in> set evs))"
apply (erule certified_mail.induct, analz_mono_contra)
apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
apply (simp add: used_Nil Crypt_notin_initState, simp_all)
@@ -310,16 +310,16 @@
done
lemma S2TTP_sender:
- "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
+ "[|Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs;
Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
==> \<exists>m ctxt q.
- hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
+ hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
Says S R
- {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number ctxt, Nonce q,
Crypt (pubEK TTP)
- {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs"
+ \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace> \<in> set evs"
by (blast intro: S2TTP_sender_lemma)
@@ -348,15 +348,15 @@
Key K \<notin> analz (spies evs) -->
(\<forall>m cleartext q hs.
Says S R
- {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q,
- Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
+ Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace>
\<in> set evs -->
(\<forall>m' cleartext' q' hs'.
Says S' R'
- {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+ \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO',
Number cleartext', Nonce q',
- Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+ Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace>
\<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))"
apply (erule certified_mail.induct, analz_mono_contra, simp_all)
prefer 2
@@ -369,14 +369,14 @@
text\<open>The key determines the sender, recipient and protocol options.\<close>
lemma Key_unique:
"[|Says S R
- {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q,
- Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
+ Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace>
\<in> set evs;
Says S' R'
- {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+ \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO',
Number cleartext', Nonce q',
- Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+ Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace>
\<in> set evs;
Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
@@ -390,9 +390,9 @@
If Spy gets the key then @{term R} is bad and @{term S} moreover
gets his return receipt (and therefore has no grounds for complaint).\<close>
theorem S_fairness_bad_R:
- "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
- Number cleartext, Nonce q, S2TTP|} \<in> set evs;
- S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+ "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+ S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
Key K \<in> analz (spies evs);
evs \<in> certified_mail;
S\<noteq>Spy|]
@@ -418,9 +418,9 @@
text\<open>Confidentially for the symmetric key\<close>
theorem Spy_not_see_encrypted_key:
- "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
- Number cleartext, Nonce q, S2TTP|} \<in> set evs;
- S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+ "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+ S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
evs \<in> certified_mail;
S\<noteq>Spy; R \<notin> bad|]
==> Key K \<notin> analz(spies evs)"
@@ -430,10 +430,10 @@
text\<open>Agent @{term R}, who may be the Spy, doesn't receive the key
until @{term S} has access to the return receipt.\<close>
theorem S_guarantee:
- "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
- Number cleartext, Nonce q, S2TTP|} \<in> set evs;
- S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
- Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
+ "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+ S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
+ Notes R \<lbrace>Agent TTP, Agent R, Key K, hs\<rbrace> \<in> set evs;
S\<noteq>Spy; evs \<in> certified_mail|]
==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
apply (erule rev_mp)
@@ -453,11 +453,11 @@
theorem RR_validity:
"[|Crypt (priSK TTP) S2TTP \<in> used evs;
S2TTP = Crypt (pubEK TTP)
- {|Agent S, Number AO, Key K, Agent R,
- Hash {|Number cleartext, Nonce q, r, em|}|};
- hr = Hash {|Number cleartext, Nonce q, r, em|};
+ \<lbrace>Agent S, Number AO, Key K, Agent R,
+ Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>\<rbrace>;
+ hr = Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>;
R\<noteq>Spy; evs \<in> certified_mail|]
- ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
+ ==> Notes R \<lbrace>Agent TTP, Agent R, Key K, hr\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule ssubst)
--- a/src/HOL/Auth/Guard/Analz.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Mon Dec 28 23:13:33 2015 +0100
@@ -17,8 +17,8 @@
for H :: "msg set"
where
Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H"
-| Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H"
-| Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H"
+| Fst [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair X |] ==> X:pparts H"
+| Snd [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair Y |] ==> Y:pparts H"
subsection\<open>basic facts about @{term pparts}\<close>
@@ -53,8 +53,8 @@
= pparts {X} Un pparts {Y} Un pparts H"
by (rule eq, (erule pparts.induct, auto)+)
-lemma pparts_insert_MPair [iff]: "pparts (insert {|X,Y|} H)
-= insert {|X,Y|} (pparts ({X,Y} Un H))"
+lemma pparts_insert_MPair [iff]: "pparts (insert \<lbrace>X,Y\<rbrace> H)
+= insert \<lbrace>X,Y\<rbrace> (pparts ({X,Y} \<union> H))"
apply (rule eq, (erule pparts.induct, auto)+)
apply (rule_tac Y=Y in pparts.Fst, auto)
apply (erule pparts.induct, auto)
@@ -119,8 +119,8 @@
for H :: "msg set"
where
Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H"
-| Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H"
-| Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H"
+| Fst [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair X |] ==> X:kparts H"
+| Snd [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair Y |] ==> Y:kparts H"
subsection\<open>basic facts about @{term kparts}\<close>
@@ -137,8 +137,8 @@
= kparts {X} Un kparts {Y} Un kparts H"
by (rule eq, (erule kparts.induct, auto)+)
-lemma kparts_insert_MPair [iff]: "kparts (insert {|X,Y|} H)
-= kparts ({X,Y} Un H)"
+lemma kparts_insert_MPair [iff]: "kparts (insert \<lbrace>X,Y\<rbrace> H)
+= kparts ({X,Y} \<union> H)"
by (rule eq, (erule kparts.induct, auto)+)
lemma kparts_insert_Nonce [iff]: "kparts (insert (Nonce n) H)
--- a/src/HOL/Auth/Guard/Extensions.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Mon Dec 28 23:13:33 2015 +0100
@@ -51,11 +51,11 @@
subsubsection\<open>messages that are pairs\<close>
definition is_MPair :: "msg => bool" where
-"is_MPair X == EX Y Z. X = {|Y,Z|}"
+"is_MPair X == EX Y Z. X = \<lbrace>Y,Z\<rbrace>"
declare is_MPair_def [simp]
-lemma MPair_is_MPair [iff]: "is_MPair {|X,Y|}"
+lemma MPair_is_MPair [iff]: "is_MPair \<lbrace>X,Y\<rbrace>"
by simp
lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)"
@@ -86,7 +86,7 @@
declare is_MPair_def [simp del]
definition has_no_pair :: "msg set => bool" where
-"has_no_pair H == ALL X Y. {|X,Y|} ~:H"
+"has_no_pair H == ALL X Y. \<lbrace>X,Y\<rbrace> \<notin> H"
declare has_no_pair_def [simp]
@@ -218,7 +218,7 @@
fun greatest_msg :: "msg => nat"
where
"greatest_msg (Nonce n) = n"
-| "greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
+| "greatest_msg \<lbrace>X,Y\<rbrace> = max (greatest_msg X) (greatest_msg Y)"
| "greatest_msg (Crypt K X) = greatest_msg X"
| "greatest_msg other = 0"
@@ -233,7 +233,7 @@
lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K"
by (auto simp: keyset_def)
-lemma MPair_notin_keyset [simp]: "keyset G ==> {|X,Y|} ~:G"
+lemma MPair_notin_keyset [simp]: "keyset G ==> \<lbrace>X,Y\<rbrace> \<notin> G"
by auto
lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G"
@@ -332,7 +332,7 @@
subsubsection\<open>lemma on knows\<close>
-lemma Says_imp_spies2: "Says A B {|X,Y|}:set evs ==> Y:parts (spies evs)"
+lemma Says_imp_spies2: "Says A B \<lbrace>X,Y\<rbrace> \<in> set evs ==> Y \<in> parts (spies evs)"
by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp)
lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |]
--- a/src/HOL/Auth/Guard/Guard.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Mon Dec 28 23:13:33 2015 +0100
@@ -19,7 +19,7 @@
No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks"
| Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks"
| Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks"
-| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> {|X,Y|}:guard n Ks"
+| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> \<lbrace>X,Y\<rbrace> \<in> guard n Ks"
subsection\<open>basic facts about @{term guard}\<close>
@@ -58,8 +58,8 @@
lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
-lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)"
-by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+)
+lemma guard_MPair [iff]: "(\<lbrace>X,Y\<rbrace> \<in> guard n Ks) = (X \<in> guard n Ks \<and> Y \<in> guard n Ks)"
+by (auto, (ind_cases "\<lbrace>X,Y\<rbrace> \<in> guard n Ks", auto)+)
lemma guard_not_guard [rule_format]: "X:guard n Ks ==>
Crypt K Y:kparts {X} --> Nonce n:kparts {Y} --> Y ~:guard n Ks"
@@ -175,7 +175,7 @@
fun crypt_nb :: "msg => nat"
where
"crypt_nb (Crypt K X) = Suc (crypt_nb X)"
-| "crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
+| "crypt_nb \<lbrace>X,Y\<rbrace> = crypt_nb X + crypt_nb Y"
| "crypt_nb X = 0" (* otherwise *)
subsection\<open>basic facts about @{term crypt_nb}\<close>
--- a/src/HOL/Auth/Guard/GuardK.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Mon Dec 28 23:13:33 2015 +0100
@@ -26,7 +26,7 @@
No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks"
| Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks"
| Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks"
-| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks"
+| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> \<lbrace>X,Y\<rbrace>:guardK n Ks"
subsection\<open>basic facts about @{term guardK}\<close>
@@ -65,9 +65,9 @@
lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
-lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
+lemma guardK_MPair [iff]: "(\<lbrace>X,Y\<rbrace>:guardK n Ks)
= (X:guardK n Ks & Y:guardK n Ks)"
-by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+)
+by (auto, (ind_cases "\<lbrace>X,Y\<rbrace>:guardK n Ks", auto)+)
lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==>
Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks"
@@ -172,7 +172,7 @@
fun crypt_nb :: "msg => nat" where
"crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
-"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
+"crypt_nb \<lbrace>X,Y\<rbrace> = crypt_nb X + crypt_nb Y" |
"crypt_nb X = 0" (* otherwise *)
subsection\<open>basic facts about @{term crypt_nb}\<close>
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Mon Dec 28 23:13:33 2015 +0100
@@ -13,19 +13,19 @@
abbreviation (input)
ns1 :: "agent => agent => nat => event" where
- "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+ "ns1 A B NA == Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"
abbreviation (input)
ns1' :: "agent => agent => agent => nat => event" where
- "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+ "ns1' A' A B NA == Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"
abbreviation (input)
ns2 :: "agent => agent => nat => nat => event" where
- "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+ "ns2 B A NA NB == Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"
abbreviation (input)
ns2' :: "agent => agent => agent => nat => nat => event" where
- "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+ "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"
abbreviation (input)
ns3 :: "agent => agent => nat => event" where
@@ -80,28 +80,28 @@
subsection\<open>nonce are used only once\<close>
lemma NA_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
---> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
+--> Crypt (pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace>:parts (spies evs)
--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
-Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
---> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs)
+--> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
--> Nonce NA:analz (spies evs)"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
lemma no_Nonce_NS1_NS2' [rule_format]:
-"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
+"[| Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs);
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs); evs:nsp |]
==> Nonce NA:analz (spies evs)"
by (rule no_Nonce_NS1_NS2, auto)
lemma NB_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
---> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
+Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
+--> Crypt (pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace>:parts (spies evs)
--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
@@ -166,13 +166,13 @@
subsection\<open>Agents' Authentication\<close>
lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
---> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
+--> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
--> ns2 B A NA NB:set evs"
apply (erule nsp.induct, simp_all, safe)
apply (frule_tac B=B in ns1_imp_Guard, simp+)
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Mon Dec 28 23:13:33 2015 +0100
@@ -16,43 +16,43 @@
abbreviation
or1 :: "agent => agent => nat => event" where
"or1 A B NA ==
- Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
+ Says A B \<lbrace>Nonce NA, Agent A, Agent B, Ciph A \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>"
abbreviation
or1' :: "agent => agent => agent => nat => msg => event" where
- "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
+ "or1' A' A B NA X == Says A' B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace>"
abbreviation
or2 :: "agent => agent => nat => nat => msg => event" where
"or2 A B NA NB X ==
- Says B Server {|Nonce NA, Agent A, Agent B, X,
- Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+ Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X,
+ Ciph B \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>"
abbreviation
or2' :: "agent => agent => agent => nat => nat => event" where
"or2' B' A B NA NB ==
- Says B' Server {|Nonce NA, Agent A, Agent B,
- Ciph A {|Nonce NA, Agent A, Agent B|},
- Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+ Says B' Server \<lbrace>Nonce NA, Agent A, Agent B,
+ Ciph A \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
+ Ciph B \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>"
abbreviation
or3 :: "agent => agent => nat => nat => key => event" where
"or3 A B NA NB K ==
- Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
- Ciph B {|Nonce NB, Key K|}|}"
+ Says Server B \<lbrace>Nonce NA, Ciph A \<lbrace>Nonce NA, Key K\<rbrace>,
+ Ciph B \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>"
abbreviation
or3':: "agent => msg => agent => agent => nat => nat => key => event" where
"or3' S Y A B NA NB K ==
- Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
+ Says S B \<lbrace>Nonce NA, Y, Ciph B \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>"
abbreviation
or4 :: "agent => agent => nat => msg => event" where
- "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
+ "or4 A B NA X == Says B A \<lbrace>Nonce NA, X, nil\<rbrace>"
abbreviation
or4' :: "agent => agent => nat => key => event" where
- "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
+ "or4' B' A NA K == Says B' A \<lbrace>Nonce NA, Ciph A \<lbrace>Nonce NA, Key K\<rbrace>, nil\<rbrace>"
subsection\<open>definition of the protocol\<close>
@@ -108,7 +108,7 @@
==> X:parts (spies evs)"
by blast
-lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
+lemma or3_parts_spies [dest]: "Says S B \<lbrace>NA, Y, Ciph B \<lbrace>NB, K\<rbrace>\<rbrace>:set evs
==> K:parts (spies evs)"
by blast
@@ -169,13 +169,13 @@
apply (case_tac "Aa=B", clarsimp)
apply (case_tac "NAa=NB", clarsimp)
apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
+apply (drule_tac Y="\<lbrace>Nonce NB, Agent Aa, Agent Ba\<rbrace>"
and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
apply (simp add: No_Nonce)
apply (case_tac "Ba=B", clarsimp)
apply (case_tac "NBa=NB", clarify)
apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
+apply (drule_tac Y="\<lbrace>Nonce NAa, Nonce NB, Agent Aa, Agent Ba\<rbrace>"
and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
apply (simp add: No_Nonce)
(* OR4 *)
--- a/src/HOL/Auth/Guard/Guard_Public.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Mon Dec 28 23:13:33 2015 +0100
@@ -14,7 +14,7 @@
subsubsection\<open>signature\<close>
definition sign :: "agent => msg => msg" where
-"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"
+"sign A X == \<lbrace>Agent A, X, Crypt (priK A) (Hash X)\<rbrace>"
lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
by (auto simp: sign_def)
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Mon Dec 28 23:13:33 2015 +0100
@@ -11,38 +11,38 @@
abbreviation (input)
ya1 :: "agent => agent => nat => event" where
- "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
+ "ya1 A B NA == Says A B \<lbrace>Agent A, Nonce NA\<rbrace>"
abbreviation (input)
ya1' :: "agent => agent => agent => nat => event" where
- "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
+ "ya1' A' A B NA == Says A' B \<lbrace>Agent A, Nonce NA\<rbrace>"
abbreviation (input)
ya2 :: "agent => agent => nat => nat => event" where
- "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+ "ya2 A B NA NB == Says B Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>"
abbreviation (input)
ya2' :: "agent => agent => agent => nat => nat => event" where
- "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+ "ya2' B' A B NA NB == Says B' Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>"
abbreviation (input)
ya3 :: "agent => agent => nat => nat => key => event" where
"ya3 A B NA NB K ==
- Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
- Ciph B {|Agent A, Key K|}|}"
+ Says Server A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+ Ciph B \<lbrace>Agent A, Key K\<rbrace>\<rbrace>"
abbreviation (input)
ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
"ya3' S Y A B NA NB K ==
- Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
+ Says S A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, Y\<rbrace>"
abbreviation (input)
ya4 :: "agent => agent => nat => nat => msg => event" where
- "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
+ "ya4 A B K NB Y == Says A B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>"
abbreviation (input)
ya4' :: "agent => agent => nat => nat => msg => event" where
- "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
+ "ya4' A' B K NB Y == Says A' B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>"
subsection\<open>definition of the protocol\<close>
@@ -128,19 +128,19 @@
lemma ya2'_parts_imp_ya1'_parts [rule_format]:
"[| evs:ya; B ~:bad |] ==>
- Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
- {|Agent A, Nonce NA|}:spies evs"
+ Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
+ \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
-==> {|Agent A, Nonce NA|}:spies evs"
+==> \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
subsection\<open>uniqueness of NB\<close>
lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
-Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
-Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
+Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
+Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace>:parts (spies evs) -->
A=A' & B=B' & NA=NA'"
apply (erule ya.induct, simp_all, clarify)
apply (drule Crypt_synth_insert, simp+)
@@ -156,15 +156,15 @@
subsection\<open>ya3' implies ya2'\<close>
lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
---> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
+--> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)"
apply (erule ya.induct, simp_all)
apply (clarify, drule Crypt_synth_insert, simp+)
apply (blast intro: parts_sub, blast)
by (auto dest: Says_imp_spies parts_parts)
lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
--> (EX B'. ya2' B' A B NA NB:set evs)"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
@@ -180,7 +180,7 @@
subsection\<open>ya3' implies ya3\<close>
lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts(spies evs)
--> ya3 A B NA NB K:set evs"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
--- a/src/HOL/Auth/Guard/List_Msg.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy Mon Dec 28 23:13:33 2015 +0100
@@ -13,7 +13,7 @@
abbreviation (input)
cons :: "msg => msg => msg" where
- "cons x l == {|x,l|}"
+ "cons x l == \<lbrace>x,l\<rbrace>"
subsubsection\<open>induction principle\<close>
--- a/src/HOL/Auth/Guard/P1.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Mon Dec 28 23:13:33 2015 +0100
@@ -18,7 +18,7 @@
the contents of the messages are not completely specified in the paper
we assume that the user sends his request and his itinerary in the clear
-we will adopt the following format for messages: {|A,r,I,L|}
+we will adopt the following format for messages: \<lbrace>A,r,I,L\<rbrace>
A: originator (agent)
r: request (number)
I: next shops (agent list)
@@ -36,8 +36,8 @@
definition chain :: "agent => nat => agent => msg => agent => msg" where
"chain B ofr A L C ==
let m1= Crypt (pubK A) (Nonce ofr) in
-let m2= Hash {|head L, Agent C|} in
-sign B {|m1,m2|}"
+let m2= Hash \<lbrace>head L, Agent C\<rbrace> in
+sign B \<lbrace>m1,m2\<rbrace>"
declare Let_def [simp]
@@ -51,7 +51,7 @@
subsubsection\<open>agent whose key is used to sign an offer\<close>
fun shop :: "msg => msg" where
-"shop {|B,X,Crypt K H|} = Agent (agt K)"
+"shop \<lbrace>B,X,Crypt K H\<rbrace> = Agent (agt K)"
lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
by (simp add: chain_def sign_def)
@@ -59,7 +59,7 @@
subsubsection\<open>nonce used in an offer\<close>
fun nonce :: "msg => msg" where
-"nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr"
+"nonce \<lbrace>B,\<lbrace>Crypt K ofr,m2\<rbrace>,CryptH\<rbrace> = ofr"
lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
by (simp add: chain_def sign_def)
@@ -67,7 +67,7 @@
subsubsection\<open>next shop\<close>
fun next_shop :: "msg => agent" where
-"next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C"
+"next_shop \<lbrace>B,\<lbrace>m1,Hash\<lbrace>headL,Agent C\<rbrace>\<rbrace>,CryptH\<rbrace> = C"
lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C"
by (simp add: chain_def sign_def)
@@ -96,8 +96,8 @@
subsubsection\<open>request event\<close>
definition reqm :: "agent => nat => nat => msg => agent => msg" where
-"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
-cons (anchor A n B) nil|}"
+"reqm A r n I B == \<lbrace>Agent A, Number r, cons (Agent A) (cons (Agent B) I),
+cons (anchor A n B) nil\<rbrace>"
lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
= (A=A' & r=r' & n=n' & I=I' & B=B')"
@@ -117,8 +117,8 @@
definition prom :: "agent => nat => agent => nat => msg => msg =>
msg => agent => msg" where
-"prom B ofr A r I L J C == {|Agent A, Number r,
-app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
+"prom B ofr A r I L J C == \<lbrace>Agent A, Number r,
+app (J, del (Agent B, I)), cons (chain B ofr A L C) L\<rbrace>"
lemma prom_inj [dest]: "prom B ofr A r I L J C
= prom B' ofr' A' r' I' L' J' C'
@@ -147,7 +147,7 @@
| Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1"
-| Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
+| Propose: "[| evsp:p1; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1"
@@ -198,7 +198,7 @@
subsubsection\<open>list of offers\<close>
fun offers :: "msg => msg" where
-"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
+"offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (offers L)" |
"offers other = nil"
subsubsection\<open>list of agents whose keys are used to sign a list of offers\<close>
@@ -262,15 +262,15 @@
apply clarify
apply (frule len_not_empty, clarsimp)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
-apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
apply (simp add: chain_def)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
by (drule_tac x=l' in spec, simp, blast)
subsubsection\<open>insertion resilience:
@@ -286,15 +286,15 @@
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
-apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
-apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l', simp)
+apply (ind_cases "\<lbrace>x,M,l'\<rbrace>:valid A n B" for x l', clarsimp)
+apply (ind_cases "\<lbrace>head l',l'\<rbrace>:valid A n B" for l', simp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
@@ -307,14 +307,14 @@
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|M,l'|}:valid A n B" for l')
+apply (ind_cases "\<lbrace>M,l'\<rbrace>:valid A n B" for l')
apply (frule len_not_empty, clarsimp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
@@ -326,7 +326,7 @@
subsubsection\<open>get components of a message\<close>
-lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==>
+lemma get_ML [dest]: "Says A' B \<lbrace>A,r,I,M,L\<rbrace>:set evs ==>
M:parts (spies evs) & L:parts (spies evs)"
by blast
@@ -400,15 +400,15 @@
lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
by (erule agl.induct, auto)
-lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
+lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace>:set evs;
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
by (auto dest: Says_to_knows_max')
-lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
+lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace>:set evs;
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
by (auto dest: Says_from_knows_max')
-lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
+lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace>:set evs;
Nonce n ~:used evs |] ==> L:guard n Ks"
by (drule not_used_not_parts, auto)
--- a/src/HOL/Auth/Guard/P2.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Mon Dec 28 23:13:33 2015 +0100
@@ -23,8 +23,8 @@
definition chain :: "agent => nat => agent => msg => agent => msg" where
"chain B ofr A L C ==
let m1= sign B (Nonce ofr) in
-let m2= Hash {|head L, Agent C|} in
-{|Crypt (pubK A) m1, m2|}"
+let m2= Hash \<lbrace>head L, Agent C\<rbrace> in
+\<lbrace>Crypt (pubK A) m1, m2\<rbrace>"
declare Let_def [simp]
@@ -38,7 +38,7 @@
subsubsection\<open>agent whose key is used to sign an offer\<close>
fun shop :: "msg => msg" where
-"shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')"
+"shop \<lbrace>Crypt K \<lbrace>B,ofr,Crypt K' H\<rbrace>,m2\<rbrace> = Agent (agt K')"
lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
by (simp add: chain_def sign_def)
@@ -46,7 +46,7 @@
subsubsection\<open>nonce used in an offer\<close>
fun nonce :: "msg => msg" where
-"nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr"
+"nonce \<lbrace>Crypt K \<lbrace>B,ofr,CryptH\<rbrace>,m2\<rbrace> = ofr"
lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
by (simp add: chain_def sign_def)
@@ -54,7 +54,7 @@
subsubsection\<open>next shop\<close>
fun next_shop :: "msg => agent" where
-"next_shop {|m1,Hash {|headL,Agent C|}|} = C"
+"next_shop \<lbrace>m1,Hash \<lbrace>headL,Agent C\<rbrace>\<rbrace> = C"
lemma "next_shop (chain B ofr A L C) = C"
by (simp add: chain_def sign_def)
@@ -77,8 +77,8 @@
subsubsection\<open>request event\<close>
definition reqm :: "agent => nat => nat => msg => agent => msg" where
-"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
-cons (anchor A n B) nil|}"
+"reqm A r n I B == \<lbrace>Agent A, Number r, cons (Agent A) (cons (Agent B) I),
+cons (anchor A n B) nil\<rbrace>"
lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
= (A=A' & r=r' & n=n' & I=I' & B=B')"
@@ -98,8 +98,8 @@
definition prom :: "agent => nat => agent => nat => msg => msg =>
msg => agent => msg" where
-"prom B ofr A r I L J C == {|Agent A, Number r,
-app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
+"prom B ofr A r I L J C == \<lbrace>Agent A, Number r,
+app (J, del (Agent B, I)), cons (chain B ofr A L C) L\<rbrace>"
lemma prom_inj [dest]: "prom B ofr A r I L J C = prom B' ofr' A' r' I' L' J' C'
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
@@ -127,7 +127,7 @@
| Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2"
-| Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
+| Propose: "[| evsp:p2; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2"
@@ -154,7 +154,7 @@
fun offers :: "msg => msg"
where
- "offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
+ "offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (offers L)"
| "offers other = nil"
@@ -173,15 +173,15 @@
apply clarify
apply (frule len_not_empty, clarsimp)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
-apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
apply (simp add: chain_def)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
by (drule_tac x=l' in spec, simp, blast)
subsection\<open>insertion resilience:
@@ -197,15 +197,15 @@
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
-apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
-apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l', simp)
+apply (ind_cases "\<lbrace>x,M,l'\<rbrace>:valid A n B" for x l', clarsimp)
+apply (ind_cases "\<lbrace>head l',l'\<rbrace>:valid A n B" for l', simp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
@@ -218,14 +218,14 @@
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|M,l'|}:valid A n B" for l')
+apply (ind_cases "\<lbrace>M,l'\<rbrace>:valid A n B" for l')
apply (frule len_not_empty, clarsimp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
@@ -237,7 +237,7 @@
subsection\<open>get components of a message\<close>
-lemma get_ML [dest]: "Says A' B {|A,R,I,M,L|}:set evs ==>
+lemma get_ML [dest]: "Says A' B \<lbrace>A,R,I,M,L\<rbrace>:set evs ==>
M:parts (spies evs) & L:parts (spies evs)"
by blast
@@ -312,15 +312,15 @@
lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
by (erule agl.induct, auto)
-lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
+lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace>:set evs;
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
by (auto dest: Says_to_knows_max')
-lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
+lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace>:set evs;
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
by (auto dest: Says_from_knows_max')
-lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
+lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace>:set evs;
Nonce n ~:used evs |] ==> L:guard n Ks"
by (drule not_used_not_parts, auto)
--- a/src/HOL/Auth/Guard/Proto.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Mon Dec 28 23:13:33 2015 +0100
@@ -39,7 +39,7 @@
if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
else Crypt (key s K) (apm s X))"
-| "apm s {|X,Y|} = {|apm s X, apm s Y|}"
+| "apm s \<lbrace>X,Y\<rbrace> = \<lbrace>apm s X, apm s Y\<rbrace>"
lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}"
apply (erule parts.induct, simp_all, blast)
@@ -371,17 +371,17 @@
abbreviation
ns1 :: rule where
- "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+ "ns1 == ({}, Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>))"
abbreviation
ns2 :: rule where
- "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
- Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
+ "ns2 == ({Says a' b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)},
+ Says b a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>))"
abbreviation
ns3 :: rule where
- "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
- Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
+ "ns3 == ({Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>),
+ Says b' a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)},
Says a b (Crypt (pubK b) (Nonce Nb)))"
inductive_set ns :: proto where
@@ -391,11 +391,11 @@
abbreviation (input)
ns3a :: event where
- "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
+ "ns3a == Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)"
abbreviation (input)
ns3b :: event where
- "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
+ "ns3b == Says b' a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)"
definition keys :: "keyfun" where
"keys R' s' n evs == {priK' s' a, priK' s' b}"
@@ -405,8 +405,8 @@
definition secret :: "secfun" where
"secret R n s Ks ==
-(if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|})
-else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})
+(if R=ns1 then apm s (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)
+else if R=ns2 then apm s (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)
else Number 0)"
definition inf :: "rule => rule => bool" where
--- a/src/HOL/Auth/Message.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Message.thy Mon Dec 28 23:13:33 2015 +0100
@@ -48,21 +48,17 @@
| Crypt key msg \<comment>\<open>Encryption, public- or shared-key\<close>
-text\<open>Concrete syntax: messages appear as {|A,B,NA|}, etc...\<close>
+text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
-
-syntax (xsymbols)
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
-
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
- "{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
\<comment>\<open>Message Y paired with a MAC computed with the help of X\<close>
- "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
\<comment>\<open>Keys useful to decrypt elements of a message set\<close>
@@ -75,9 +71,9 @@
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"
+ Inj [intro]: "X \<in> H ==> X \<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"
@@ -136,7 +132,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]:
@@ -153,7 +149,7 @@
subsection\<open>Inductive relation "parts"\<close>
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)
@@ -330,9 +326,9 @@
analz :: "msg set => msg set"
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"
+ Inj [intro,simp]: "X \<in> H ==> X \<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"
@@ -346,7 +342,7 @@
text\<open>Making it safe speeds up proofs\<close>
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)
@@ -427,8 +423,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)
@@ -540,7 +536,7 @@
text\<open>If there are no pairs or encryptions then analz does nothing\<close>
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
@@ -571,7 +567,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\<open>Monotonicity\<close>
@@ -585,7 +581,7 @@
"Nonce n \<in> synth H"
"Key K \<in> synth H"
"Hash X \<in> synth H"
- "{|X,Y|} \<in> synth H"
+ "\<lbrace>X,Y\<rbrace> \<in> synth H"
"Crypt K X \<in> synth H"
lemma synth_increasing: "H \<subseteq> synth(H)"
@@ -694,7 +690,7 @@
text\<open>Without this equation, other rules for synth and analz would yield
redundant cases\<close>
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
@@ -706,7 +702,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
@@ -742,11 +738,11 @@
by (simp add: HPair_def)
lemma MPair_eq_HPair [iff]:
- "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
+ "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
by (simp add: HPair_def)
lemma HPair_eq_MPair [iff]:
- "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
+ "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
by (auto simp add: HPair_def)
@@ -757,18 +753,18 @@
lemma parts_insert_HPair [simp]:
"parts (insert (Hash[X] Y) H) =
- insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
+ insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
by (simp add: HPair_def)
lemma analz_insert_HPair [simp]:
"analz (insert (Hash[X] Y) H) =
- insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
+ insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
by (simp add: HPair_def)
lemma HPair_synth_analz [simp]:
"X \<notin> synth (analz H)
==> (Hash[X] Y \<in> synth (analz H)) =
- (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
+ (Hash \<lbrace>X, Y\<rbrace> \<in> analz H & Y \<in> synth (analz H))"
by (auto simp add: HPair_def)
@@ -814,14 +810,14 @@
| Number: "Number N \<in> keyfree"
| Nonce: "Nonce N \<in> keyfree"
| Hash: "Hash X \<in> keyfree"
- | MPair: "[|X \<in> keyfree; Y \<in> keyfree|] ==> {|X,Y|} \<in> keyfree"
+ | MPair: "[|X \<in> keyfree; Y \<in> keyfree|] ==> \<lbrace>X,Y\<rbrace> \<in> keyfree"
| Crypt: "[|X \<in> keyfree|] ==> Crypt K X \<in> keyfree"
declare keyfree.intros [intro]
inductive_cases keyfree_KeyE: "Key K \<in> keyfree"
-inductive_cases keyfree_MPairE: "{|X,Y|} \<in> keyfree"
+inductive_cases keyfree_MPairE: "\<lbrace>X,Y\<rbrace> \<in> keyfree"
inductive_cases keyfree_CryptE: "Crypt K X \<in> keyfree"
lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree"
--- a/src/HOL/Auth/OtwayRees.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Mon Dec 28 23:13:33 2015 +0100
@@ -31,17 +31,17 @@
(*Alice initiates a protocol run*)
| OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
- ==> Says A B {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+ ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace>
# evs1 : otway"
(*Bob's response to Alice's message. Note that NB is encrypted.*)
| OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
- Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+ Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2 |]
==> Says B Server
- {|Nonce NA, Agent A, Agent B, X,
+ \<lbrace>Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
- {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+ \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
# evs2 : otway"
(*The Server receives Bob's message and checks that the three NAs
@@ -49,34 +49,34 @@
forwarding to Alice.*)
| OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server
- {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
- Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+ \<lbrace>Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
+ Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
: set evs3 |]
==> Says Server B
- {|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key KAB|},
- Crypt (shrK B) {|Nonce NB, Key KAB|}|}
+ \<lbrace>Nonce NA,
+ Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
# evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
Need B \<noteq> Server because we allow messages to self.*)
| OR4: "[| evs4 \<in> otway; B \<noteq> Server;
- Says B Server {|Nonce NA, Agent A, Agent B, X',
+ Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
- {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+ \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
: set evs4;
- Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
: set evs4 |]
- ==> Says B A {|Nonce NA, X|} # evs4 : otway"
+ ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
| Oops: "[| evso \<in> otway;
- Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
: set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+ ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso : otway"
declare Says_imp_analz_Spy [dest]
@@ -88,7 +88,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
==> \<exists>evs \<in> otway.
- Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+ Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
@@ -108,12 +108,12 @@
(** For reasoning about the encrypted portion of messages **)
lemma OR2_analz_knows_Spy:
- "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |]
+ "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway |]
==> X \<in> analz (knows Spy evs)"
by blast
lemma OR4_analz_knows_Spy:
- "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |]
==> X \<in> analz (knows Spy evs)"
by blast
@@ -151,7 +151,7 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
lemma Says_Server_message_form:
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
by (erule rev_mp, erule otway.induct, simp_all)
@@ -190,8 +190,8 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
- Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+ "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs;
+ Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
apply (erule rev_mp)
apply (erule rev_mp)
@@ -205,27 +205,27 @@
text\<open>Only OR1 can have caused such a part of a message to appear.\<close>
lemma Crypt_imp_OR1 [rule_format]:
"[| A \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
- Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
+ Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
by (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Crypt_imp_OR1_Gets:
- "[| Gets B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ "[| Gets B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
A \<notin> bad; evs \<in> otway |]
- ==> Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ ==> Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest: Crypt_imp_OR1)
text\<open>The Nonce NA uniquely identifies A's message\<close>
lemma unique_NA:
- "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
- Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs);
evs \<in> otway; A \<notin> bad |]
==> B = C"
apply (erule rev_mp, erule rev_mp)
@@ -238,9 +238,9 @@
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close>
lemma no_nonce_OR1_OR2:
- "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
+ ==> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
@@ -250,13 +250,13 @@
to start a run, then it originated with the Server!\<close>
lemma NA_Crypt_imp_Server_msg [rule_format]:
"[| A \<notin> bad; evs \<in> otway |]
- ==> Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs -->
- Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs)
+ ==> Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs -->
+ Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<exists>NB. Says Server B
- {|NA,
- Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
+ \<lbrace>NA,
+ Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
apply blast \<comment>\<open>OR1: by freshness\<close>
@@ -270,14 +270,14 @@
bad form of this protocol, even though we can prove
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma A_trusts_OR4:
- "[| Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
- Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
+ "[| Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
+ Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
A \<notin> bad; evs \<in> otway |]
==> \<exists>NB. Says Server B
- {|NA,
- Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|}
+ \<lbrace>NA,
+ Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast intro!: NA_Crypt_imp_Server_msg)
@@ -288,9 +288,9 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
- Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
@@ -303,9 +303,9 @@
theorem Spy_not_see_encrypted_key:
"[| Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
- Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)
@@ -319,9 +319,9 @@
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
lemma Spy_not_know_encrypted_key:
"[| Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
- Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> knows Spy evs"
by (blast dest: Spy_not_see_encrypted_key)
@@ -330,10 +330,10 @@
text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.\<close>
lemma A_gets_good_key:
- "[| Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
- Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
- \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ "[| Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
+ Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
@@ -344,11 +344,11 @@
text\<open>Only OR2 can have caused such a part of a message to appear. We do not
know anything about X: it does NOT have to have the right form.\<close>
lemma Crypt_imp_OR2:
- "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> otway |]
==> \<exists>X. Says B Server
- {|NA, Agent A, Agent B, X,
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+ \<lbrace>NA, Agent A, Agent B, X,
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule otway.induct, force,
@@ -358,8 +358,8 @@
text\<open>The Nonce NB uniquely identifies B's message\<close>
lemma unique_NB:
- "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs);
- Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs);
+ Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs);
evs \<in> otway; B \<notin> bad |]
==> NC = NA & C = A"
apply (erule rev_mp, erule rev_mp)
@@ -372,14 +372,14 @@
then it originated with the Server! Quite messy proof.\<close>
lemma NB_Crypt_imp_Server_msg [rule_format]:
"[| B \<notin> bad; evs \<in> otway |]
- ==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs)
+ ==> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<forall>X'. Says B Server
- {|NA, Agent A, Agent B, X',
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+ \<lbrace>NA, Agent A, Agent B, X',
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs
--> Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|}
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
\<in> set evs)"
apply simp
apply (erule otway.induct, force,
@@ -394,15 +394,15 @@
text\<open>Guarantee for B: if it gets a message with matching NB then the Server
has sent the correct message.\<close>
theorem B_trusts_OR3:
- "[| Says B Server {|NA, Agent A, Agent B, X',
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs;
- Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
B \<notin> bad; evs \<in> otway |]
==> Says Server B
- {|NA,
- Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|}
+ \<lbrace>NA,
+ Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast intro!: NB_Crypt_imp_Server_msg)
@@ -410,11 +410,11 @@
text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma B_gets_good_key:
- "[| Says B Server {|NA, Agent A, Agent B, X',
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs;
- Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
- Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
@@ -422,11 +422,11 @@
lemma OR3_imp_OR2:
"[| Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
B \<notin> bad; evs \<in> otway |]
- ==> \<exists>X. Says B Server {|NA, Agent A, Agent B, X,
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ ==> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
@@ -438,12 +438,12 @@
We could probably prove that X has the expected form, but that is not
strictly necessary for authentication.\<close>
theorem A_auths_B:
- "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
- Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ "[| Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
+ Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
- ==> \<exists>NB X. Says B Server {|NA, Agent A, Agent B, X,
- Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ ==> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+ Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest!: A_trusts_OR4 OR3_imp_OR2)
--- a/src/HOL/Auth/OtwayRees_AN.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Mon Dec 28 23:13:33 2015 +0100
@@ -39,30 +39,30 @@
| OR1: \<comment>\<open>Alice initiates a protocol run\<close>
"evs1 \<in> otway
- ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \<in> otway"
+ ==> Says A B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> otway"
| OR2: \<comment>\<open>Bob's response to Alice's message.\<close>
"[| evs2 \<in> otway;
- Gets B {|Agent A, Agent B, Nonce NA|} \<in>set evs2 |]
- ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+ Gets B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in>set evs2 |]
+ ==> Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace>
# evs2 \<in> otway"
| OR3: \<comment>\<open>The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.\<close>
"[| evs3 \<in> otway; Key KAB \<notin> used evs3;
- Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+ Gets Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace>
\<in>set evs3 |]
==> Says Server B
- {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
- Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key KAB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key KAB\<rbrace>\<rbrace>
# evs3 \<in> otway"
| OR4: \<comment>\<open>Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
Need @{term "B \<noteq> Server"} because we allow messages to self.\<close>
"[| evs4 \<in> otway; B \<noteq> Server;
- Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \<in>set evs4;
- Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
+ Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> \<in>set evs4;
+ Gets B \<lbrace>X, Crypt(shrK B)\<lbrace>Nonce NB,Agent A,Agent B,Key K\<rbrace>\<rbrace>
\<in>set evs4 |]
==> Says B A X # evs4 \<in> otway"
@@ -70,10 +70,10 @@
identify the protocol run.\<close>
"[| evso \<in> otway;
Says Server B
- {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in>set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+ ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -85,7 +85,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
==> \<exists>evs \<in> otway.
- Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
+ Says B A (Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>)
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
@@ -104,7 +104,7 @@
text\<open>For reasoning about the encrypted portion of messages\<close>
lemma OR4_analz_knows_Spy:
- "[| Gets B {|X, Crypt(shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ "[| Gets B \<lbrace>X, Crypt(shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |]
==> X \<in> analz (knows Spy evs)"
by blast
@@ -131,8 +131,8 @@
text\<open>Describes the form of K and NA when the Server sends this message.\<close>
lemma Says_Server_message_form:
"[| Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
@@ -175,12 +175,12 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
"[| Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, K\<rbrace>\<rbrace>
\<in> set evs;
Says Server B'
- {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},
- Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}
+ \<lbrace>Crypt (shrK A') \<lbrace>NA', Agent A', Agent B', K\<rbrace>,
+ Crypt (shrK B') \<lbrace>NB', Agent A', Agent B', K\<rbrace>\<rbrace>
\<in> set evs;
evs \<in> otway |]
==> A=A' & B=B' & NA=NA' & NB=NB'"
@@ -194,10 +194,10 @@
text\<open>If the encrypted message appears then it originated with the Server!\<close>
lemma NA_Crypt_imp_Server_msg [rule_format]:
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
- ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+ ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<exists>NB. Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs)"
apply (erule otway.induct, force)
apply (simp_all add: ex_disj_distrib)
@@ -208,11 +208,11 @@
text\<open>Corollary: if A receives B's OR4 message then it originated with the
Server. Freshness may be inferred from nonce NA.\<close>
lemma A_trusts_OR4:
- "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
+ "[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs;
A \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> \<exists>NB. Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast intro!: NA_Crypt_imp_Server_msg)
@@ -223,10 +223,10 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs -->
- Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
@@ -239,10 +239,10 @@
lemma Spy_not_see_encrypted_key:
"[| Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs;
- Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (metis secrecy_lemma)
@@ -251,8 +251,8 @@
text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.\<close>
lemma A_gets_good_key:
- "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
- \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ "[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs;
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (metis A_trusts_OR4 secrecy_lemma)
@@ -264,10 +264,10 @@
text\<open>If the encrypted message appears then it originated with the Server!\<close>
lemma NB_Crypt_imp_Server_msg [rule_format]:
"[| B \<notin> bad; A \<noteq> B; evs \<in> otway |]
- ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+ ==> Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
--> (\<exists>NA. Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs)"
apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
apply blast+ \<comment>\<open>Fake, OR3\<close>
@@ -278,12 +278,12 @@
text\<open>Guarantee for B: if it gets a well-formed certificate then the Server
has sent the correct message in round 3.\<close>
lemma B_trusts_OR3:
- "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ "[| Says S B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs;
B \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> \<exists>NA. Says Server B
- {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
- Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast intro!: NB_Crypt_imp_Server_msg)
@@ -291,9 +291,9 @@
text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma B_gets_good_key:
- "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ "[| Gets B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
\<in> set evs;
- \<forall>NA. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ \<forall>NA. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)
--- a/src/HOL/Auth/OtwayRees_Bad.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Mon Dec 28 23:13:33 2015 +0100
@@ -36,17 +36,17 @@
| OR1: \<comment>\<open>Alice initiates a protocol run\<close>
"[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
- ==> Says A B {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+ ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
# evs1 \<in> otway"
| OR2: \<comment>\<open>Bob's response to Alice's message.
This variant of the protocol does NOT encrypt NB.\<close>
"[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
- Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
+ Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> \<in> set evs2 |]
==> Says B Server
- {|Nonce NA, Agent A, Agent B, X, Nonce NB,
- Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+ \<lbrace>Nonce NA, Agent A, Agent B, X, Nonce NB,
+ Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
# evs2 \<in> otway"
| OR3: \<comment>\<open>The Server receives Bob's message and checks that the three NAs
@@ -54,34 +54,34 @@
forwarding to Alice.\<close>
"[| evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server
- {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
+ \<lbrace>Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
Nonce NB,
- Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+ Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs3 |]
==> Says Server B
- {|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key KAB|},
- Crypt (shrK B) {|Nonce NB, Key KAB|}|}
+ \<lbrace>Nonce NA,
+ Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
# evs3 \<in> otway"
| OR4: \<comment>\<open>Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
Need @{term "B \<noteq> Server"} because we allow messages to self.\<close>
"[| evs4 \<in> otway; B \<noteq> Server;
- Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
- Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+ Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X', Nonce NB,
+ Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs4;
- Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
\<in> set evs4 |]
- ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
+ ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway"
| Oops: \<comment>\<open>This message models possible leaks of session keys. The nonces
identify the protocol run.\<close>
"[| evso \<in> otway;
- Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
\<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+ ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -92,7 +92,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
==> \<exists>NA. \<exists>evs \<in> otway.
- Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+ Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
@@ -112,17 +112,17 @@
subsection\<open>For reasoning about the encrypted portion of messages\<close>
lemma OR2_analz_knows_Spy:
- "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |]
+ "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway |]
==> X \<in> analz (knows Spy evs)"
by blast
lemma OR4_analz_knows_Spy:
- "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |]
==> X \<in> analz (knows Spy evs)"
by blast
lemma Oops_parts_knows_Spy:
- "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs
+ "Says Server B \<lbrace>NA, X, Crypt K' \<lbrace>NB,K\<rbrace>\<rbrace> \<in> set evs
==> K \<in> parts (knows Spy evs)"
by blast
@@ -155,7 +155,7 @@
text\<open>Describes the form of K and NA when the Server sends this message. Also
for Oops case.\<close>
lemma Says_Server_message_form:
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
apply (erule rev_mp)
@@ -196,8 +196,8 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
- Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+ "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs;
+ Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
apply (erule rev_mp)
apply (erule rev_mp)
@@ -212,9 +212,9 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
- Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
@@ -228,9 +228,9 @@
lemma Spy_not_see_encrypted_key:
"[| Says Server B
- {|NA, Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
- Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+ Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)
@@ -243,9 +243,9 @@
up. Original Otway-Rees doesn't need it.\<close>
lemma Crypt_imp_OR1 [rule_format]:
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
- ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
- Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs"
+ ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
+ Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs"
by (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
@@ -256,14 +256,14 @@
text\<open>Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.\<close>
lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
- ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
- Says A B {|NA, Agent A, Agent B,
- Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ ==> Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs) -->
+ Says A B \<lbrace>NA, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs -->
(\<exists>B NB. Says Server B
- {|NA,
- Crypt (shrK A) {|NA, Key K|},
- Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
+ \<lbrace>NA,
+ Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+ Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all)
apply blast \<comment>\<open>Fake\<close>
@@ -276,13 +276,13 @@
(*The hypotheses at this point suggest an attack in which nonce NB is used
in two different roles:
Gets Server
- {|Nonce NA, Agent Aa, Agent A,
- Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
- Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
+ \<lbrace>Nonce NA, Agent Aa, Agent A,
+ Crypt (shrK Aa) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>, Nonce NB,
+ Crypt (shrK A) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>\<rbrace>
\<in> set evs3
Says A B
- {|Nonce NB, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
+ \<lbrace>Nonce NB, Agent A, Agent B,
+ Crypt (shrK A) \<lbrace>Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
\<in> set evs3;
*)
--- a/src/HOL/Auth/Public.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Public.thy Mon Dec 28 23:13:33 2015 +0100
@@ -239,13 +239,13 @@
apply (auto dest!: parts_cut simp add: used_Nil)
done
-lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
+lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H ==> X \<in> used H & Y \<in> used H"
by (drule used_parts_subset_parts, simp, blast)
text\<open>There was a similar theorem in Event.thy, so perhaps this one can
be moved up if proved directly by induction.\<close>
lemma MPair_used [elim!]:
- "[| {|X,Y|} \<in> used H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> used H;
[| X \<in> used H; Y \<in> used H |] ==> P |]
==> P"
by (blast dest: MPair_used_D)
--- a/src/HOL/Auth/Recur.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Recur.thy Mon Dec 28 23:13:33 2015 +0100
@@ -21,18 +21,18 @@
for evs :: "event list"
where
One: "Key KAB \<notin> used evs
- ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
- {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
+ ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>,
+ \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>,
KAB) \<in> respond evs"
(*The most recent session key is passed up to the caller*)
| Cons: "[| (PA, RA, KAB) \<in> respond evs;
Key KBC \<notin> used evs; Key KBC \<notin> parts {RA};
- PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
- ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
- {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
- Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- RA|},
+ PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |]
+ ==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>,
+ \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+ RA\<rbrace>,
KBC)
\<in> respond evs"
@@ -48,8 +48,8 @@
Nil: "END \<in> responses evs"
| Cons: "[| RA \<in> responses evs; Key KAB \<notin> used evs |]
- ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- RA|} \<in> responses evs"
+ ==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+ RA\<rbrace> \<in> responses evs"
inductive_set recur :: "event list set"
@@ -65,15 +65,15 @@
(*Alice initiates a protocol run.
END is a placeholder to terminate the nesting.*)
| RA1: "[| evs1 \<in> recur; Nonce NA \<notin> used evs1 |]
- ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
+ ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>)
# evs1 \<in> recur"
(*Bob's response to Alice's message. C might be the Server.
- We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
+ We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because
it complicates proofs, so B may respond to any message at all!*)
| RA2: "[| evs2 \<in> recur; Nonce NB \<notin> used evs2;
Says A' B PA \<in> set evs2 |]
- ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
+ ==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>)
# evs2 \<in> recur"
(*The Server receives Bob's message and prepares a response.*)
@@ -84,11 +84,11 @@
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
| RA4: "[| evs4 \<in> recur;
- Says B C {|XH, Agent B, Agent C, Nonce NB,
- XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
- Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
- Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- RA|} \<in> set evs4 |]
+ Says B C \<lbrace>XH, Agent B, Agent C, Nonce NB,
+ XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4;
+ Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+ RA\<rbrace> \<in> set evs4 |]
==> Says B A RA # evs4 \<in> recur"
(*No "oops" message can easily be expressed. Each session key is
@@ -101,7 +101,7 @@
Oops: "[| evso \<in> recur; Says Server B RB \<in> set evso;
RB \<in> responses evs'; Key K \<in> parts {RB} |]
- ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
+ ==> Notes Spy \<lbrace>Key K, RB\<rbrace> # evso \<in> recur"
*)
@@ -120,8 +120,8 @@
text\<open>Simplest case: Alice goes directly to the server\<close>
lemma "Key K \<notin> used []
==> \<exists>NA. \<exists>evs \<in> recur.
- Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
- END|} \<in> set evs"
+ Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>,
+ END\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] recur.Nil [THEN recur.RA1,
THEN recur.RA3 [OF _ _ respond.One]])
@@ -133,8 +133,8 @@
lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
==> \<exists>NA. \<exists>evs \<in> recur.
- Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
- END|} \<in> set evs"
+ Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
+ END\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil
@@ -152,8 +152,8 @@
Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used [];
NA < NB; NB < NC |]
==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
- Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
- END|} \<in> set evs"
+ Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
+ END\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
@@ -189,7 +189,7 @@
lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
lemma RA4_analz_spies:
- "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
+ "Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<in> set evs ==> RA \<in> analz (spies evs)"
by blast
@@ -278,7 +278,7 @@
text\<open>Everything that's hashed is already in past traffic.\<close>
lemma Hash_imp_body:
- "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
+ "[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<in> parts (spies evs);
evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule recur.induct,
@@ -299,8 +299,8 @@
**)
lemma unique_NA:
- "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \<in> parts (spies evs);
- Hash {|Key(shrK A), Agent A, B',NA, P'|} \<in> parts (spies evs);
+ "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs);
+ Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs);
evs \<in> recur; A \<notin> bad |]
==> B=B' & P=P'"
apply (erule rev_mp, erule rev_mp)
@@ -348,8 +348,8 @@
text\<open>The last key returned by respond indeed appears in a certificate\<close>
lemma respond_certificate:
- "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
- ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
+ "(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs
+ ==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}"
apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs")
apply simp_all
done
@@ -361,8 +361,8 @@
the quantifiers appear to be necessary.*)
lemma unique_lemma [rule_format]:
"(PB,RB,KXY) \<in> respond evs ==>
- \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
- (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
+ \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} -->
+ (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} -->
(A'=A & B'=B) | (A'=B & B'=A))"
apply (erule respond.induct)
apply (simp_all add: all_conj_distrib)
@@ -370,8 +370,8 @@
done
lemma unique_session_keys:
- "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
- Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
+ "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB};
+ Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB};
(PB,RB,KXY) \<in> respond evs |]
==> (A'=A & B'=B) | (A'=B & B'=A)"
by (rule unique_lemma, auto)
@@ -384,7 +384,7 @@
lemma respond_Spy_not_see_session_key [rule_format]:
"[| (PB,RB,KAB) \<in> respond evs; evs \<in> recur |]
==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
- Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
+ Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} -->
Key K \<notin> analz (insert RB (spies evs))"
apply (erule respond.induct)
apply (frule_tac [2] respond_imp_responses)
@@ -405,7 +405,7 @@
lemma Spy_not_see_session_key:
- "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
+ "[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts (spies evs);
A \<notin> bad; A' \<notin> bad; evs \<in> recur |]
==> Key K \<notin> analz (spies evs)"
apply (erule rev_mp)
@@ -430,9 +430,9 @@
text\<open>The response never contains Hashes\<close>
lemma Hash_in_parts_respond:
- "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
+ "[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H);
(PB,RB,K) \<in> respond evs |]
- ==> Hash {|Key (shrK B), M|} \<in> parts H"
+ ==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H"
apply (erule rev_mp)
apply (erule respond_imp_responses [THEN responses.induct], auto)
done
@@ -442,9 +442,9 @@
it can say nothing about how recent A's message is. It might later be
used to prove B's presence to A at the run's conclusion.\<close>
lemma Hash_auth_sender [rule_format]:
- "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
+ "[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs);
A \<notin> bad; evs \<in> recur |]
- ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs"
+ ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs"
apply (unfold HPair_def)
apply (erule rev_mp)
apply (erule recur.induct,
--- a/src/HOL/Auth/TLS.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/TLS.thy Mon Dec 28 23:13:33 2015 +0100
@@ -20,7 +20,7 @@
The model assumes that no fraudulent certificates are present, but it does
assume that some private keys are to the spy.
-REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
+REMARK. The event "Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>" appears in ClientKeyExch,
CertVerify, ClientFinished to record that A knows M. It is a note from A to
herself. Nobody else can see it. In ClientKeyExch, the Spy can substitute
his own certificate for A's, but he cannot replace A's note by one for himself.
@@ -35,7 +35,7 @@
Proofs would be simpler if ClientKeyExch included A's name within
Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs
about that message (which B receives) and the stronger event
-Notes A {|Agent B, Nonce PMS|}.
+Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>.
*)
section\<open>The TLS Protocol: Transport Layer Security\<close>
@@ -43,7 +43,7 @@
theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
definition certificate :: "[agent,key] => msg" where
- "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
+ "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>"
text\<open>TLS apparently does not require separate keypairs for encryption and
signature. Therefore, we formalize signature as encryption using the
@@ -109,8 +109,8 @@
to available nonces\<close>
"[| evsSK \<in> tls;
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
- ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
- Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
+ ==> Notes Spy \<lbrace> Nonce (PRF(M,NA,NB)),
+ Key (sessionK((NA,NB,M),role))\<rbrace> # evsSK \<in> tls"
| ClientHello:
\<comment>\<open>(7.4.1.2)
@@ -121,7 +121,7 @@
May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is
28 bytes while MASTER SECRET is 48 bytes\<close>
"[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |]
- ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
+ ==> Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
# evsCH \<in> tls"
| ServerHello:
@@ -130,9 +130,9 @@
SERVER CERTIFICATE (7.4.2) is always present.
\<open>CERTIFICATE_REQUEST\<close> (7.4.4) is implied.\<close>
"[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF;
- Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
+ Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
\<in> set evsSH |]
- ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls"
+ ==> Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> # evsSH \<in> tls"
| Certificate:
\<comment>\<open>SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.\<close>
@@ -150,7 +150,7 @@
"[| evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF;
Says B' A (certificate B KB) \<in> set evsCX |]
==> Says A B (Crypt KB (Nonce PMS))
- # Notes A {|Agent B, Nonce PMS|}
+ # Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>
# evsCX \<in> tls"
| CertVerify:
@@ -160,9 +160,9 @@
Checking the signature, which is the only use of A's certificate,
assures B of A's presence\<close>
"[| evsCV \<in> tls;
- Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV;
- Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |]
- ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
+ Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCV;
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCV |]
+ ==> Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>))
# evsCV \<in> tls"
\<comment>\<open>Finally come the FINISHED messages (7.4.8), confirming PA and PB
@@ -170,37 +170,37 @@
Either party may send its message first.\<close>
| ClientFinished:
- \<comment>\<open>The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
+ \<comment>\<open>The occurrence of Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> stops the
rule's applying when the Spy has satisfied the "Says A B" by
repaying messages sent by the true client; in that case, the
Spy does not know PMS and could not send ClientFinished. One
could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
expect the spy to be well-behaved.\<close>
"[| evsCF \<in> tls;
- Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
+ Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
\<in> set evsCF;
- Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCF;
- Notes A {|Agent B, Nonce PMS|} \<in> set evsCF;
+ Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCF;
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCF;
M = PRF(PMS,NA,NB) |]
==> Says A B (Crypt (clientK(NA,NB,M))
- (Hash{|Number SID, Nonce M,
+ (Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|}))
+ Nonce NB, Number PB, Agent B\<rbrace>))
# evsCF \<in> tls"
| ServerFinished:
\<comment>\<open>Keeping A' and A'' distinct means B cannot even check that the
two messages originate from the same source.\<close>
"[| evsSF \<in> tls;
- Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
+ Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
\<in> set evsSF;
- Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSF;
+ Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSF;
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF;
M = PRF(PMS,NA,NB) |]
==> Says B A (Crypt (serverK(NA,NB,M))
- (Hash{|Number SID, Nonce M,
+ (Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|}))
+ Nonce NB, Number PB, Agent B\<rbrace>))
# evsSF \<in> tls"
| ClientAccepts:
@@ -209,15 +209,15 @@
needed to resume this session. The "Notes A ..." premise is
used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close>
"[| evsCA \<in> tls;
- Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCA;
M = PRF(PMS,NA,NB);
- X = Hash{|Number SID, Nonce M,
+ X = Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|};
+ Nonce NB, Number PB, Agent B\<rbrace>;
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA;
Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |]
==>
- Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls"
+ Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsCA \<in> tls"
| ServerAccepts:
\<comment>\<open>Having transmitted ServerFinished and received an identical
@@ -228,38 +228,38 @@
A \<noteq> B;
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
M = PRF(PMS,NA,NB);
- X = Hash{|Number SID, Nonce M,
+ X = Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|};
+ Nonce NB, Number PB, Agent B\<rbrace>;
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA;
Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |]
==>
- Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls"
+ Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsSA \<in> tls"
| ClientResume:
\<comment>\<open>If A recalls the \<open>SESSION_ID\<close>, then she sends a FINISHED
message using the new nonces and stored MASTER SECRET.\<close>
"[| evsCR \<in> tls;
- Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
- Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
- Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsCR |]
+ Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>: set evsCR;
+ Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCR;
+ Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsCR |]
==> Says A B (Crypt (clientK(NA,NB,M))
- (Hash{|Number SID, Nonce M,
+ (Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|}))
+ Nonce NB, Number PB, Agent B\<rbrace>))
# evsCR \<in> tls"
| ServerResume:
\<comment>\<open>Resumption (7.3): If B finds the \<open>SESSION_ID\<close> then he can
send a FINISHED message using the recovered MASTER SECRET\<close>
"[| evsSR \<in> tls;
- Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
- Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
- Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsSR |]
+ Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>: set evsSR;
+ Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSR;
+ Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsSR |]
==> Says B A (Crypt (serverK(NA,NB,M))
- (Hash{|Number SID, Nonce M,
+ (Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|})) # evsSR
+ Nonce NB, Number PB, Agent B\<rbrace>)) # evsSR
\<in> tls"
| Oops:
@@ -333,7 +333,7 @@
text\<open>Possibility property ending with ClientAccepts.\<close>
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID M. \<exists>evs \<in> tls.
- Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
+ Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
[THEN tls.ClientHello, THEN tls.ServerHello,
@@ -346,7 +346,7 @@
text\<open>And one for ServerAccepts. Either FINISHED message may come first.\<close>
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
- Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
+ Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
[THEN tls.ClientHello, THEN tls.ServerHello,
@@ -359,7 +359,7 @@
text\<open>Another one, for CertVerify (which is optional)\<close>
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
==> \<exists>NB PMS. \<exists>evs \<in> tls.
- Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
+ Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>))
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
@@ -372,14 +372,14 @@
text\<open>Another one, for session resumption (both ServerResume and ClientResume).
NO tls.Nil here: we refer to a previous session, not the empty trace.\<close>
lemma "[| evs0 \<in> tls;
- Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
- Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
+ Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
+ Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
\<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;
A \<noteq> B |]
==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls.
- X = Hash{|Number SID, Nonce M,
+ X = Hash\<lbrace>Number SID, Nonce M,
Nonce NA, Number PA, Agent A,
- Nonce NB, Number PB, Agent B|} &
+ Nonce NB, Number PB, Agent B\<rbrace> &
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs &
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs"
apply (intro exI bexI)
@@ -425,7 +425,7 @@
subsubsection\<open>Properties of items found in Notes\<close>
lemma Notes_Crypt_parts_spies:
- "[| Notes A {|Agent B, X|} \<in> set evs; evs \<in> tls |]
+ "[| Notes A \<lbrace>Agent B, X\<rbrace> \<in> set evs; evs \<in> tls |]
==> Crypt (pubK B) X \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct,
@@ -435,7 +435,7 @@
text\<open>C may be either A or B\<close>
lemma Notes_master_imp_Crypt_PMS:
- "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
+ "[| Notes C \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
evs \<in> tls |]
==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
apply (erule rev_mp)
@@ -448,9 +448,9 @@
text\<open>Compared with the theorem above, both premise and conclusion are stronger\<close>
lemma Notes_master_imp_Notes_PMS:
- "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
+ "[| Notes A \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
evs \<in> tls |]
- ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+ ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
txt\<open>ServerAccepts\<close>
@@ -463,7 +463,7 @@
text\<open>B can check A's signature if he has received A's certificate.\<close>
lemma TrustCertVerify_lemma:
"[| X \<in> parts (spies evs);
- X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
+ X = Crypt (priK A) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
evs \<in> tls; A \<notin> bad |]
==> Says A B X \<in> set evs"
apply (erule rev_mp, erule ssubst)
@@ -473,7 +473,7 @@
text\<open>Final version: B checks X using the distributed KA instead of priK A\<close>
lemma TrustCertVerify:
"[| X \<in> parts (spies evs);
- X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
+ X = Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
certificate A KA \<in> parts (spies evs);
evs \<in> tls; A \<notin> bad |]
==> Says A B X \<in> set evs"
@@ -482,25 +482,25 @@
text\<open>If CertVerify is present then A has chosen PMS.\<close>
lemma UseCertVerify_lemma:
- "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
+ "[| Crypt (priK A) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) \<in> parts (spies evs);
evs \<in> tls; A \<notin> bad |]
- ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+ ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all, blast)
done
text\<open>Final version using the distributed KA instead of priK A\<close>
lemma UseCertVerify:
- "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
+ "[| Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>)
\<in> parts (spies evs);
certificate A KA \<in> parts (spies evs);
evs \<in> tls; A \<notin> bad |]
- ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+ ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
by (blast dest!: certificate_valid intro!: UseCertVerify_lemma)
lemma no_Notes_A_PRF [simp]:
- "evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
+ "evs \<in> tls ==> Notes A \<lbrace>Agent B, Nonce (PRF x)\<rbrace> \<notin> set evs"
apply (erule tls.induct, force, simp_all)
txt\<open>ClientKeyExch: PMS is assumed to differ from any PRF.\<close>
apply blast
@@ -538,15 +538,15 @@
(** It is frustrating that we need two versions of the unicity results.
- But Notes A {|Agent B, Nonce PMS|} determines both A and B. Sometimes
+ But Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> determines both A and B. Sometimes
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which
determines B alone, and only if PMS is secret.
**)
text\<open>In A's internal Note, PMS determines A and B.\<close>
lemma Notes_unique_PMS:
- "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
- Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
+ "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
+ Notes A' \<lbrace>Agent B', Nonce PMS\<rbrace> \<in> set evs;
evs \<in> tls |]
==> A=A' & B=B'"
apply (erule rev_mp, erule rev_mp)
@@ -674,7 +674,7 @@
text\<open>If A sends ClientKeyExch to an honest B, then the PMS will stay secret.\<close>
lemma Spy_not_see_PMS:
- "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce PMS \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -696,7 +696,7 @@
text\<open>If A sends ClientKeyExch to an honest B, then the MASTER SECRET
will stay secret.\<close>
lemma Spy_not_see_MS:
- "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -720,7 +720,7 @@
would send a message using a clientK generated from that PMS.\<close>
lemma Says_clientK_unique:
"[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
- Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
evs \<in> tls; A' \<noteq> Spy |]
==> A = A'"
apply (erule rev_mp, erule rev_mp)
@@ -737,7 +737,7 @@
text\<open>If A created PMS and has not leaked her clientK to the Spy,
then it is completely secure: not even in parts!\<close>
lemma clientK_not_spied:
- "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
A \<notin> bad; B \<notin> bad;
evs \<in> tls |]
@@ -762,7 +762,7 @@
send a message using a serverK generated from that PMS.\<close>
lemma Says_serverK_unique:
"[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
- Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad; B' \<noteq> Spy |]
==> B = B'"
apply (erule rev_mp, erule rev_mp)
@@ -779,7 +779,7 @@
text\<open>If A created PMS for B, and B has not leaked his serverK to the Spy,
then it is completely secure: not even in parts!\<close>
lemma serverK_not_spied:
- "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+ "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> tls |]
==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
@@ -804,13 +804,13 @@
text\<open>The mention of her name (A) in X assures A that B knows who she is.\<close>
lemma TrustServerFinished [rule_format]:
"[| X = Crypt (serverK(Na,Nb,M))
- (Hash{|Number SID, Nonce M,
+ (Hash\<lbrace>Number SID, Nonce M,
Nonce Na, Number PA, Agent A,
- Nonce Nb, Number PB, Agent B|});
+ Nonce Nb, Number PB, Agent B\<rbrace>);
M = PRF(PMS,NA,NB);
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
- Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
X \<in> parts (spies evs) --> Says B A X \<in> set evs"
apply (erule ssubst)+
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -829,7 +829,7 @@
lemma TrustServerMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
- Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs) -->
(\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)"
apply (erule ssubst)
@@ -855,7 +855,7 @@
lemma TrustClientMsg [rule_format]:
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs -->
- Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+ Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) -->
Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
apply (erule ssubst)
@@ -878,7 +878,7 @@
Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs;
certificate A KA \<in> parts (spies evs);
- Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))
+ Says A'' B (Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>))
\<in> set evs;
evs \<in> tls; A \<notin> bad; B \<notin> bad |]
==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
--- a/src/HOL/Auth/WooLam.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/WooLam.thy Mon Dec 28 23:13:33 2015 +0100
@@ -52,13 +52,13 @@
| WL4: "[| evs4 \<in> woolam;
Says A' B X \<in> set evs4;
Says A'' B (Agent A) \<in> set evs4 |]
- ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
+ ==> Says B Server \<lbrace>Agent A, Agent B, X\<rbrace> # evs4 \<in> woolam"
(*Server decrypts Alice's response for Bob.*)
| WL5: "[| evs5 \<in> woolam;
- Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
+ Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
\<in> set evs5 |]
- ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
+ ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>)
# evs5 \<in> woolam"
@@ -70,7 +70,7 @@
(*A "possibility property": there are traces that reach the end*)
lemma "\<exists>NB. \<exists>evs \<in> woolam.
- Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \<in> set evs"
+ Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] woolam.Nil
[THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
@@ -113,7 +113,7 @@
Alice, then she originated that certificate. But we DO NOT know that B
ever saw it: the Spy may have rerouted the message to the Server.*)
lemma Server_trusts_WL4 [dest]:
- "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
+ "[| Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
\<in> set evs;
A \<notin> bad; evs \<in> woolam |]
==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
@@ -124,17 +124,17 @@
(*Server sent WL5 only if it received the right sort of message*)
lemma Server_sent_WL5 [dest]:
- "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
+ "[| Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs;
evs \<in> woolam |]
- ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
+ ==> \<exists>B'. Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) NB\<rbrace>
\<in> set evs"
by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(*If the encrypted message appears then it originated with the Server!*)
lemma NB_Crypt_imp_Server_msg [rule_format]:
- "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
+ "[| Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace> \<in> parts (spies evs);
B \<notin> bad; evs \<in> woolam |]
- ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
+ ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs"
by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
@@ -142,7 +142,7 @@
But A may have sent the nonce to some other agent and it could have reached
the Server via the Spy.*)
lemma B_trusts_WL5:
- "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
+ "[| Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>): set evs;
A \<notin> bad; B \<notin> bad; evs \<in> woolam |]
==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
by (blast dest!: NB_Crypt_imp_Server_msg)
--- a/src/HOL/Auth/Yahalom.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom.thy Mon Dec 28 23:13:33 2015 +0100
@@ -32,24 +32,24 @@
(*Alice initiates a protocol run*)
| YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+ ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
| YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+ Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
==> Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
# evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
| YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys;
Gets Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
\<in> set evs3 |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key KAB|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
# evs3 \<in> yahalom"
| YM4:
@@ -58,25 +58,25 @@
@{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>.
Alice can check that K is symmetric by its length.\<close>
"[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys;
- Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
+ Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+ Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+ ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
| Oops: "[| evso \<in> yahalom;
- Says Server A {|Crypt (shrK A)
- {|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} \<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
+ Says Server A \<lbrace>Crypt (shrK A)
+ \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+ X\<rbrace> \<in> set evso |]
+ ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
definition KeyWithNonce :: "[key, nat, event list] => bool" where
"KeyWithNonce K NB evs ==
\<exists>A B na X.
- Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
+ Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs"
@@ -88,7 +88,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[| A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] |]
==> \<exists>X NB. \<exists>evs \<in> yahalom.
- Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
@@ -116,7 +116,7 @@
text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
lemma YM4_analz_knows_Spy:
- "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
by blast
@@ -125,7 +125,7 @@
text\<open>For Oops\<close>
lemma YM4_Key_parts_knows_Spy:
- "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
+ "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs
==> K \<in> parts (knows Spy evs)"
by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj)
@@ -170,7 +170,7 @@
text\<open>Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.\<close>
lemma Says_Server_not_range [simp]:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
+ "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace>
\<in> set evs; evs \<in> yahalom |]
==> K \<notin> range shrK"
by (erule rev_mp, erule yahalom.induct, simp_all)
@@ -210,9 +210,9 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
"[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
Says Server A'
- {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+ \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
evs \<in> yahalom |]
==> A=A' & B=B' & na=na' & nb=nb'"
apply (erule rev_mp, erule rev_mp)
@@ -226,10 +226,10 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs -->
- Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force,
drule_tac [6] YM4_analz_knows_Spy)
@@ -240,10 +240,10 @@
text\<open>Final version\<close>
lemma Spy_not_see_encrypted_key:
"[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs;
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: secrecy_lemma)
@@ -253,11 +253,11 @@
text\<open>If the encrypted message appears then it originated with the Server\<close>
lemma A_trusts_YM3:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -269,8 +269,8 @@
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma A_gets_good_key:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (metis A_trusts_YM3 secrecy_lemma)
@@ -281,12 +281,12 @@
text\<open>B knows, by the first part of A's message, that the Server distributed
the key for A and B. But this part says nothing about nonces.\<close>
lemma B_trusts_YM4_shrK:
- "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
==> \<exists>NA NB. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K,
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+ Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -305,8 +305,8 @@
"[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
==> \<exists>A B NA. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
@@ -329,14 +329,14 @@
lemma KeyWithNonceI:
"Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs ==> KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast)
lemma KeyWithNonce_Says [simp]:
"KeyWithNonce K NB (Says S A X # evs) =
(Server = S &
- (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
+ (\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>)
| KeyWithNonce K NB evs)"
by (simp add: KeyWithNonce_def, blast)
@@ -358,7 +358,7 @@
text\<open>The Server message associates K with NB' and therefore not with any
other nonce NB.\<close>
lemma Says_Server_KeyWithNonce:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
+ "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace>
\<in> set evs;
NB \<noteq> NB'; evs \<in> yahalom |]
==> ~ KeyWithNonce K NB evs"
@@ -417,7 +417,7 @@
for the induction to carry through.\<close>
lemma single_Nonce_secrecy:
"[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace>
\<in> set evs;
NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |]
==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
@@ -430,8 +430,8 @@
subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close>
lemma unique_NB:
- "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
- Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
+ Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs);
evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |]
==> NA' = NA & A' = A & B' = B"
apply (erule rev_mp, erule rev_mp)
@@ -445,9 +445,9 @@
text\<open>Variant useful for proving secrecy of NB. Because nb is assumed to be
secret, we no longer must assume B, B' not bad.\<close>
lemma Says_unique_NB:
- "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ "[| Says C S \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
\<in> set evs;
- Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
+ Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace>
\<in> set evs;
nb \<notin> analz (knows Spy evs); evs \<in> yahalom |]
==> NA' = NA & A' = A & B' = B"
@@ -458,9 +458,9 @@
subsubsection\<open>A nonce value is never used both as NA and as NB\<close>
lemma no_nonce_YM1_YM2:
- "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
+ "[|Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs);
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
- ==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
+ ==> Crypt (shrK B) \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
@@ -471,18 +471,18 @@
text\<open>The Server sends YM3 only in response to YM2.\<close>
lemma Says_Server_imp_YM2:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
+ "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
evs \<in> yahalom |]
- ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
+ ==> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace>
\<in> set evs"
by (erule rev_mp, erule yahalom.induct, auto)
text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close>
lemma Spy_not_see_NB :
"[| Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
\<in> set evs;
- (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+ (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Nonce NB \<notin> analz (knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
@@ -521,17 +521,17 @@
If this run is broken and the spy substitutes a certificate containing an
old key, B has no means of telling.\<close>
lemma B_trusts_YM4:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
\<in> set evs;
- \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K,
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+ Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest: Spy_not_see_NB Says_unique_NB
Says_Server_imp_YM2 B_trusts_YM4_newK)
@@ -541,12 +541,12 @@
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma B_gets_good_key:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
\<in> set evs;
- \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
@@ -556,10 +556,10 @@
text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
lemma B_Said_YM2 [rule_format]:
- "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
+ "[|Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
evs \<in> yahalom|]
==> B \<notin> bad -->
- Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp, erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
@@ -569,10 +569,10 @@
text\<open>If the server sends YM3 then B sent YM2\<close>
lemma YM3_auth_B_to_A_lemma:
- "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ "[|Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
\<in> set evs; evs \<in> yahalom|]
==> B \<notin> bad -->
- Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp, erule yahalom.induct, simp_all)
txt\<open>YM3, YM4\<close>
@@ -581,10 +581,10 @@
text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
lemma YM3_auth_B_to_A:
- "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ "[| Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ ==> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
\<in> set evs"
by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
not_parts_not_analz)
@@ -600,9 +600,9 @@
"evs \<in> yahalom
==> Key K \<notin> analz (knows Spy evs) -->
Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
- Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) -->
B \<notin> bad -->
- (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+ (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
@@ -624,13 +624,13 @@
Moreover, A associates K with NB (thus is talking about the same run).
Other premises guarantee secrecy of K.\<close>
lemma YM4_imp_A_Said_YM3 [rule_format]:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
\<in> set evs;
- (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+ (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
end
--- a/src/HOL/Auth/Yahalom2.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Mon Dec 28 23:13:33 2015 +0100
@@ -36,44 +36,44 @@
(*Alice initiates a protocol run*)
| YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+ ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
| YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+ Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
==> Says B Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
# evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a certificate for forwarding to Bob.
Both agents are quoted in the 2nd certificate to prevent attacks!*)
| YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
- Gets Server {|Agent B, Nonce NB,
- Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ Gets Server \<lbrace>Agent B, Nonce NB,
+ Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs3 |]
==> Says Server A
- {|Nonce NB,
- Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
- Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
+ \<lbrace>Nonce NB,
+ Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key KAB, Nonce NB\<rbrace>\<rbrace>
# evs3 \<in> yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
| YM4: "[| evs4 \<in> yahalom;
- Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} \<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+ Gets A \<lbrace>Nonce NB, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+ X\<rbrace> \<in> set evs4;
+ Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+ ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
| Oops: "[| evso \<in> yahalom;
- Says Server A {|Nonce NB,
- Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} \<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
+ Says Server A \<lbrace>Nonce NB,
+ Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+ X\<rbrace> \<in> set evso |]
+ ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -84,7 +84,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "Key K \<notin> used []
==> \<exists>X NB. \<exists>evs \<in> yahalom.
- Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
@@ -111,7 +111,7 @@
text\<open>Result for reasoning about the encrypted portion of messages.
Lets us treat YM4 using a similar argument as for the Fake case.\<close>
lemma YM4_analz_knows_Spy:
- "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ "[| Gets A \<lbrace>NB, Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
by blast
@@ -157,7 +157,7 @@
text\<open>Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.\<close>
lemma Says_Server_message_form:
- "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
+ "[| Says Server A \<lbrace>nb', Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace>
\<in> set evs; evs \<in> yahalom |]
==> K \<notin> range shrK"
by (erule rev_mp, erule yahalom.induct, simp_all)
@@ -194,9 +194,9 @@
text\<open>The Key K uniquely identifies the Server's message\<close>
lemma unique_session_keys:
"[| Says Server A
- {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
+ \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> \<in> set evs;
Says Server A'
- {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
+ \<lbrace>nb', Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace>, X'\<rbrace> \<in> set evs;
evs \<in> yahalom |]
==> A=A' & B=B' & na=na' & nb=nb'"
apply (erule rev_mp, erule rev_mp)
@@ -211,10 +211,10 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
\<in> set evs -->
- Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
drule_tac [6] YM4_analz_knows_Spy)
@@ -226,10 +226,10 @@
text\<open>Final version\<close>
lemma Spy_not_see_encrypted_key:
"[| Says Server A
- {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
\<in> set evs;
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: secrecy_lemma Says_Server_message_form)
@@ -245,10 +245,10 @@
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
lemma Spy_not_know_encrypted_key:
"[| Says Server A
- {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
\<in> set evs;
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> knows Spy evs"
by (blast dest: Spy_not_see_encrypted_key)
@@ -259,11 +259,11 @@
text\<open>If the encrypted message appears then it originated with the Server.
May now apply \<open>Spy_not_see_encrypted_key\<close>, subject to its conditions.\<close>
lemma A_trusts_YM3:
- "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> yahalom |]
==> \<exists>nb. Says Server A
- {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -275,8 +275,8 @@
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
theorem A_gets_good_key:
- "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
- \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs);
+ \<forall>nb. Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
@@ -287,13 +287,13 @@
text\<open>B knows, by the first part of A's message, that the Server distributed
the key for A and B, and has associated it with NB.\<close>
lemma B_trusts_YM4_shrK:
- "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+ "[| Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
\<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
==> \<exists>NA. Says Server A
- {|Nonce NB,
- Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+ \<lbrace>Nonce NB,
+ Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -309,13 +309,13 @@
text\<open>What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
because we do not have to show that NB is secret.\<close>
lemma B_trusts_YM4:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>NA. Says Server A
- {|Nonce NB,
- Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+ \<lbrace>Nonce NB,
+ Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest!: B_trusts_YM4_shrK)
@@ -323,9 +323,9 @@
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
theorem B_gets_good_key:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs;
- \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
+ \<forall>na. Notes Spy \<lbrace>na, Nonce NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
@@ -335,10 +335,10 @@
text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
lemma B_Said_YM2:
- "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace> \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
- Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ ==> \<exists>NB. Says B Server \<lbrace>Agent B, Nonce NB,
+ Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -350,11 +350,11 @@
text\<open>If the server sends YM3 then B sent YM2, perhaps with a different NB\<close>
lemma YM3_auth_B_to_A_lemma:
- "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+ "[| Says Server A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace>
\<in> set evs;
B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>nb'. Says B Server {|Agent B, nb',
- Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ ==> \<exists>nb'. Says B Server \<lbrace>Agent B, nb',
+ Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, simp_all)
@@ -364,11 +364,11 @@
text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
theorem YM3_auth_B_to_A:
- "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+ "[| Gets A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>nb'. Says B Server
- {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, nb', Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
@@ -385,8 +385,8 @@
text\<open>This lemma allows a use of \<open>unique_session_keys\<close> in the next proof,
which otherwise is extremely slow.\<close>
lemma secure_unique_session_keys:
- "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
- Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> analz (spies evs);
+ Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace> \<in> analz (spies evs);
Key K \<notin> analz (knows Spy evs); evs \<in> yahalom |]
==> A=A' & B=B'"
by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
@@ -397,10 +397,10 @@
==> Key K \<notin> analz (knows Spy evs) -->
K \<in> symKeys -->
Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
- Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
\<in> parts (knows Spy evs) -->
B \<notin> bad -->
- (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+ (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
@@ -419,11 +419,11 @@
Moreover, A associates K with NB (thus is talking about the same run).
Other premises guarantee secrecy of K.\<close>
theorem YM4_imp_A_Said_YM3 [rule_format]:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
- Crypt K (Nonce NB)|} \<in> set evs;
- (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
+ (\<forall>NA. Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> \<notin> set evs);
K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
by (blast intro: Auth_A_to_B_lemma
dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
--- a/src/HOL/Auth/Yahalom_Bad.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.thy Mon Dec 28 23:13:33 2015 +0100
@@ -31,34 +31,34 @@
(*Alice initiates a protocol run*)
| YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+ ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
| YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+ Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
==> Says B Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
# evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
| YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys;
Gets Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs3 |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key KAB|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
# evs3 \<in> yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
A \<noteq> Server is needed to prove Says_Server_not_range.*)
| YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys;
- Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
+ Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+ Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+ ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -70,7 +70,7 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
==> \<exists>X NB. \<exists>evs \<in> yahalom.
- Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
@@ -98,7 +98,7 @@
text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
lemma YM4_analz_knows_Spy:
- "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
by blast
@@ -168,9 +168,9 @@
text\<open>The Key K uniquely identifies the Server's message.\<close>
lemma unique_session_keys:
"[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
Says Server A'
- {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+ \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
evs \<in> yahalom |]
==> A=A' & B=B' & na=na' & nb=nb'"
apply (erule rev_mp, erule rev_mp)
@@ -184,8 +184,8 @@
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
@@ -196,8 +196,8 @@
text\<open>Final version\<close>
lemma Spy_not_see_encrypted_key:
"[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
@@ -208,11 +208,11 @@
text\<open>If the encrypted message appears then it originated with the Server\<close>
lemma A_trusts_YM3:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> yahalom |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -224,7 +224,7 @@
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma A_gets_good_key:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
@@ -234,11 +234,11 @@
text\<open>B knows, by the first part of A's message, that the Server distributed
the key for A and B. But this part says nothing about nonces.\<close>
lemma B_trusts_YM4_shrK:
- "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+ "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
==> \<exists>NA NB. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -262,9 +262,9 @@
"[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|]
==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
(\<exists>A B NA. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K,
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+ Nonce NA, Nonce NB\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs)"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
@@ -285,15 +285,15 @@
text\<open>B's session key guarantee from YM4. The two certificates contribute to a
single conclusion about the Server's message.\<close>
lemma B_trusts_YM4:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>na nb. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
\<in> set evs"
by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key
unique_session_keys)
@@ -302,10 +302,10 @@
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with
\<open>Spy_not_see_encrypted_key\<close>\<close>
lemma B_gets_good_key:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
@@ -325,9 +325,9 @@
"evs \<in> yahalom
==> Key K \<notin> analz (knows Spy evs) -->
Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
- Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+ Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) -->
B \<notin> bad -->
- (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+ (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
@@ -349,13 +349,13 @@
Moreover, A associates K with NB (thus is talking about the same run).
Other premises guarantee secrecy of K.\<close>
lemma YM4_imp_A_Said_YM3 [rule_format]:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
+ "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+ Crypt K (Nonce NB)\<rbrace> \<in> set evs;
Says B Server
- {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+ ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
by (blast intro!: A_Said_YM3_lemma
dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
--- a/src/HOL/Auth/ZhouGollmann.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/ZhouGollmann.thy Mon Dec 28 23:13:33 2015 +0100
@@ -43,24 +43,24 @@
rather than to keep M secret.*)
| ZG1: "[| evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m);
K \<in> symKeys;
- NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
- ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
+ NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>|]
+ ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # evs1 \<in> zg"
(*B must check that NRO is A's signature to learn the sender's name*)
| ZG2: "[| evs2 \<in> zg;
- Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
- NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
- ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2 \<in> zg"
+ Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs2;
+ NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>|]
+ ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # evs2 \<in> zg"
(*A must check that NRR is B's signature to learn the sender's name;
without spy, the matching label would be enough*)
| ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
- Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
- Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
- ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+ Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs3;
+ Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs3;
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>|]
+ ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
# evs3 \<in> zg"
(*TTP checks that sub_K is A's signature to learn who issued K, then
@@ -70,14 +70,14 @@
also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
@{term "K \<noteq> priK TTP"}. *)
| ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
- Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+ Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
\<in> set evs4;
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
- con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
- Nonce L, Key K|}|]
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
+ con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
+ Nonce L, Key K\<rbrace>|]
==> Says TTP Spy con_K
#
- Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
# evs4 \<in> zg"
@@ -92,8 +92,8 @@
text\<open>A "possibility property": there are traces that reach the end\<close>
lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
\<exists>L. \<exists>evs \<in> zg.
- Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
- Crypt (priK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|} |}
+ Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K,
+ Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace>
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] zg.Nil
@@ -128,18 +128,18 @@
done
lemma Notes_TTP_imp_Gets:
- "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
+ "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<in> set evs;
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
evs \<in> zg|]
- ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+ ==> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
done
text\<open>For reasoning about C, which is encrypted in message ZG2\<close>
lemma ZG2_msg_in_parts_spies:
- "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
+ "[|Gets B \<lbrace>F, B', L, C, X\<rbrace> \<in> set evs; evs \<in> zg|]
==> C \<in> parts (spies evs)"
by (blast dest: Gets_imp_Says)
@@ -165,10 +165,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma NRO_validity_good:
- "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
NRO \<in> parts (spies evs);
A \<notin> bad; evs \<in> zg |]
- ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+ ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
@@ -176,7 +176,7 @@
done
lemma NRO_sender:
- "[|Says A' B {|n, b, l, C, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
+ "[|Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|]
==> A' \<in> {A,Spy}"
apply (erule rev_mp)
apply (erule zg.induct, simp_all)
@@ -184,10 +184,10 @@
text\<open>Holds also for @{term "A = Spy"}!\<close>
theorem NRO_validity:
- "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
- NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ "[|Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs;
+ NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
A \<notin> broken; evs \<in> zg |]
- ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+ ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
apply (drule Gets_imp_Says, assumption)
apply clarify
apply (frule NRO_sender, auto)
@@ -205,10 +205,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma NRR_validity_good:
- "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ "[|NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
NRR \<in> parts (spies evs);
B \<notin> bad; evs \<in> zg |]
- ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+ ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
@@ -216,7 +216,7 @@
done
lemma NRR_sender:
- "[|Says B' A {|n, a, l, Crypt (priK B) X|} \<in> set evs; evs \<in> zg|]
+ "[|Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<in> set evs; evs \<in> zg|]
==> B' \<in> {B,Spy}"
apply (erule rev_mp)
apply (erule zg.induct, simp_all)
@@ -224,10 +224,10 @@
text\<open>Holds also for @{term "B = Spy"}!\<close>
theorem NRR_validity:
- "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+ "[|Says B' A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs;
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
B \<notin> broken; evs \<in> zg|]
- ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+ ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
apply clarify
apply (frule NRR_sender, auto)
txt\<open>We are left with the case where @{term "B' = Spy"} and @{term "B' \<noteq> B"},
@@ -243,10 +243,10 @@
text\<open>Strong conclusion for a good agent\<close>
lemma sub_K_validity_good:
- "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ "[|sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
sub_K \<in> parts (spies evs);
A \<notin> bad; evs \<in> zg |]
- ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+ ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
@@ -256,7 +256,7 @@
done
lemma sub_K_sender:
- "[|Says A' TTP {|n, b, l, k, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
+ "[|Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|]
==> A' \<in> {A,Spy}"
apply (erule rev_mp)
apply (erule zg.induct, simp_all)
@@ -264,10 +264,10 @@
text\<open>Holds also for @{term "A = Spy"}!\<close>
theorem sub_K_validity:
- "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ "[|Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs;
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg |]
- ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+ ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
apply (drule Gets_imp_Says, assumption)
apply clarify
apply (frule sub_K_sender, auto)
@@ -288,9 +288,9 @@
lemma con_K_validity:
"[|con_K \<in> used evs;
con_K = Crypt (priK TTP)
- {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+ \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
evs \<in> zg |]
- ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ ==> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<in> set evs"
apply clarify
apply (erule rev_mp)
@@ -306,11 +306,11 @@
@{term sub_K}. We assume that @{term A} is not broken. Importantly, nothing
needs to be assumed about the form of @{term con_K}!\<close>
lemma Notes_TTP_imp_Says_A:
- "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+ "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
\<in> set evs;
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg|]
- ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+ ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
@@ -324,11 +324,11 @@
assume that @{term A} is not broken.\<close>
theorem B_sub_K_validity:
"[|con_K \<in> used evs;
- con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
- Nonce L, Key K|};
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
+ Nonce L, Key K\<rbrace>;
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> broken; evs \<in> zg|]
- ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+ ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
@@ -340,9 +340,9 @@
text\<open>Strange: unicity of the label protects @{term A}?\<close>
lemma A_unicity:
- "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+ "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
NRO \<in> parts (spies evs);
- Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
+ Says A B \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M', NRO'\<rbrace>
\<in> set evs;
A \<notin> bad; evs \<in> zg |]
==> M'=M"
@@ -359,13 +359,13 @@
text\<open>Fairness lemma: if @{term sub_K} exists, then @{term A} holds
NRR. Relies on unicity of labels.\<close>
lemma sub_K_implies_NRR:
- "[| NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+ "[| NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
sub_K \<in> parts (spies evs);
NRO \<in> parts (spies evs);
- sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+ sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
A \<notin> bad; evs \<in> zg |]
- ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+ ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
apply clarify
apply hypsubst_thin
apply (erule rev_mp)
@@ -382,7 +382,7 @@
lemma Crypt_used_imp_L_used:
- "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
+ "[| Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<in> used evs; evs \<in> zg |]
==> L \<in> used evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
@@ -400,11 +400,11 @@
"[|con_K \<in> used evs;
NRO \<in> parts (spies evs);
con_K = Crypt (priK TTP)
- {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
- NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+ \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
+ NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
A \<notin> bad; evs \<in> zg |]
- ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+ ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule rev_mp)
@@ -427,10 +427,10 @@
A}.\<close>
theorem B_fairness_NRR:
"[|NRR \<in> used evs;
- NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
- NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+ NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
+ NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
B \<notin> bad; evs \<in> zg |]
- ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+ ==> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Dec 28 23:13:33 2015 +0100
@@ -33,7 +33,7 @@
NS1 :: "(state*state) set"
where "NS1 = {(s1,s').
\<exists>A1 B NA.
- s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
+ s' = Says A1 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A1\<rbrace>) # s1
& Nonce NA \<notin> used s1}"
(*Bob responds to Alice's message with a further nonce*)
@@ -41,8 +41,8 @@
NS2 :: "(state*state) set"
where "NS2 = {(s2,s').
\<exists>A' A2 B NA NB.
- s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
- & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
+ s' = Says B A2 (Crypt (pubK A2) \<lbrace>Nonce NA, Nonce NB\<rbrace>) # s2
+ & Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A2\<rbrace>) \<in> set s2
& Nonce NB \<notin> used s2}"
(*Alice proves her existence by sending NB back to Bob.*)
@@ -51,8 +51,8 @@
where "NS3 = {(s3,s').
\<exists>A3 B' B NA NB.
s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
- & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
- & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}"
+ & Says A3 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A3\<rbrace>) \<in> set s3
+ & Says B' A3 (Crypt (pubK A3) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s3}"
definition Nprg :: "state program" where
@@ -151,8 +151,8 @@
nonce is secret. (Honest users generate fresh nonces.)*}
lemma no_nonce_NS1_NS2:
"Nprg
- \<in> Always {s. Crypt (pubK C) {|NA', Nonce NA|} \<in> parts (spies s) -->
- Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s) -->
+ \<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) -->
+ Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) -->
Nonce NA \<in> analz (spies s)}"
apply ns_induct
apply (blast intro: analz_insertI)+
@@ -167,8 +167,8 @@
lemma unique_NA_lemma:
"Nprg
\<in> Always {s. Nonce NA \<notin> analz (spies s) -->
- Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s) -->
- Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s) -->
+ Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s) -->
+ Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s) -->
A=A' & B=B'}"
apply ns_induct
apply auto
@@ -177,8 +177,8 @@
text{*Unicity for NS1: nonce NA identifies agents A and B*}
lemma unique_NA:
- "[| Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s);
- Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s);
+ "[| Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s);
+ Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s);
Nonce NA \<notin> analz (spies s);
s \<in> reachable Nprg |]
==> A=A' & B=B'"
@@ -189,7 +189,7 @@
lemma Spy_not_see_NA:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
- {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s
+ {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s
--> Nonce NA \<notin> analz (spies s)}"
apply ns_induct
txt{*NS3*}
@@ -208,9 +208,9 @@
lemma A_trusts_NS2:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
- {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s &
- Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts (knows Spy s)
- --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}) \<in> set s}"
+ {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s &
+ Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (knows Spy s)
+ --> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s}"
(*insert an invariant for use in some of the subgoals*)
apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct)
apply (auto dest: unique_NA)
@@ -221,8 +221,8 @@
lemma B_trusts_NS1:
"Nprg \<in> Always
{s. Nonce NA \<notin> analz (spies s) -->
- Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s)
- --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) \<in> set s}"
+ Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s)
+ --> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s}"
apply ns_induct
apply blast
done
@@ -235,8 +235,8 @@
lemma unique_NB_lemma:
"Nprg
\<in> Always {s. Nonce NB \<notin> analz (spies s) -->
- Crypt (pubK A) {|Nonce NA, Nonce NB|} \<in> parts (spies s) -->
- Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s) -->
+ Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies s) -->
+ Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s) -->
A=A' & NA=NA'}"
apply ns_induct
apply auto
@@ -244,8 +244,8 @@
done
lemma unique_NB:
- "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts(spies s);
- Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s);
+ "[| Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies s);
+ Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s);
Nonce NB \<notin> analz (spies s);
s \<in> reachable Nprg |]
==> A=A' & NA=NA'"
@@ -257,7 +257,7 @@
lemma Spy_not_see_NB:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
- {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s &
+ {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s &
(ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s)
--> Nonce NB \<notin> analz (spies s)}"
apply ns_induct
@@ -280,7 +280,7 @@
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
{s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) &
- Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+ Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
--> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}"
(*insert an invariant for use in some of the subgoals*)
apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
@@ -294,7 +294,7 @@
text{*Can we strengthen the secrecy theorem? NO*}
lemma "[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
- {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+ {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
--> Nonce NB \<notin> analz (spies s)}"
apply ns_induct
apply auto
@@ -317,13 +317,13 @@
[| A \<notin> bad; B \<notin> bad |]
==> Nprg
\<in> Always
- {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s -->
+ {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s -->
Nonce NB \<notin> analz (knows Spy s)}
1. !!s B' C.
[| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg
- Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) \<in> set s;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
- C \<in> bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
+ Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s;
+ Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s;
+ C \<in> bad; Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s;
Nonce NB \<notin> analz (knows Spy s) |]
==> False
*)