--- 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