--- a/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 08 15:17:11 1998 +0200
@@ -24,8 +24,7 @@
(*A "possibility property": there are traces that reach the end.*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX Timestamp K. EX evs: kerberos_ban. \
+Goal "EX Timestamp K. EX evs: kerberos_ban. \
\ Says B A (Crypt K (Number Timestamp)) \
\ : set evs";
by (cut_facts_tac [SesKeyLife_LB] 1);
@@ -41,15 +40,6 @@
(**** Inductive proofs about kerberos_ban ****)
-(*Nobody sends themselves messages*)
-Goal "evs : kerberos_ban ==> ALL X. Says A A X ~: set evs";
-by (etac kerberos_ban.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
\ ==> X : parts (spies evs)";
--- a/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 08 15:17:11 1998 +0200
@@ -48,18 +48,16 @@
Nil "[]: kerberos_ban"
-
- Fake "[| evs: kerberos_ban; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: kerberos_ban; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : kerberos_ban"
- Kb1 "[| evs1: kerberos_ban; A ~= Server |]
+ Kb1 "[| evs1: kerberos_ban |]
==> Says A Server {|Agent A, Agent B|} # evs1
: kerberos_ban"
- Kb2 "[| evs2: kerberos_ban; A ~= B; A ~= Server; Key KAB ~: used evs2;
+ Kb2 "[| evs2: kerberos_ban; Key KAB ~: used evs2;
Says A' Server {|Agent A, Agent B|} : set evs2 |]
==> Says Server A
(Crypt (shrK A)
@@ -68,7 +66,7 @@
# evs2 : kerberos_ban"
- Kb3 "[| evs3: kerberos_ban; A ~= B;
+ Kb3 "[| evs3: kerberos_ban;
Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
: set evs3;
Says A Server {|Agent A, Agent B|} : set evs3;
@@ -77,21 +75,19 @@
# evs3 : kerberos_ban"
- Kb4 "[| evs4: kerberos_ban; A ~= B;
+ Kb4 "[| evs4: kerberos_ban;
Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
(Crypt K {|Agent A, Number Ta|}) |}: set evs4;
- ~ Expired Ts evs4;
- RecentAuth Ta evs4|]
+ ~ Expired Ts evs4; RecentAuth Ta evs4 |]
==> Says B A (Crypt K (Number Ta)) # evs4
: kerberos_ban"
-
-(*The session key has EXPIRED when it gets lost *)
- Oops "[| evso: kerberos_ban; A ~= Spy;
+ (*Old session keys may become compromised*)
+ Oops "[| evso: kerberos_ban;
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
: set evso;
Expired Ts evso |]
- ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
+ ==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban"
end
--- a/src/HOL/Auth/NS_Public.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML Tue Sep 08 15:17:11 1998 +0200
@@ -14,8 +14,8 @@
AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
-Goal "A ~= B ==> EX NB. EX evs: ns_public. \
-\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
+Goal
+ "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by possibility_tac;
@@ -24,15 +24,6 @@
(**** Inductive proofs about ns_public ****)
-(*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
-by (etac ns_public.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(*Induction for regularity theorems. If induction formula has the form
X ~: analz (spies evs) --> ... then it shortens the proof by discarding
needless information about analz (insert X (spies evs)) *)
--- a/src/HOL/Auth/NS_Public.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public.thy Tue Sep 08 15:17:11 1998 +0200
@@ -19,17 +19,16 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_public; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: ns_public; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs1: ns_public; A ~= B; Nonce NA ~: used evs1 |]
+ NS1 "[| evs1: ns_public; Nonce NA ~: used evs1 |]
==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
# evs1 : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs2: ns_public; A ~= B; Nonce NB ~: used evs2;
+ NS2 "[| evs2: ns_public; Nonce NB ~: used evs2;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
# evs2 : ns_public"
--- a/src/HOL/Auth/NS_Public_Bad.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Tue Sep 08 15:17:11 1998 +0200
@@ -18,8 +18,8 @@
AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
-Goal "A ~= B ==> EX NB. EX evs: ns_public. \
-\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
+Goal
+ "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by possibility_tac;
@@ -28,15 +28,6 @@
(**** Inductive proofs about ns_public ****)
-(*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
-by (etac ns_public.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(*Induction for regularity theorems. If induction formula has the form
X ~: analz (spies evs) --> ... then it shortens the proof by discarding
needless information about analz (insert X (spies evs)) *)
--- a/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 08 15:17:11 1998 +0200
@@ -23,17 +23,16 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_public; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: ns_public; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs1: ns_public; A ~= B; Nonce NA ~: used evs1 |]
+ NS1 "[| evs1: ns_public; Nonce NA ~: used evs1 |]
==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
# evs1 : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs2: ns_public; A ~= B; Nonce NB ~: used evs2;
+ NS2 "[| evs2: ns_public; Nonce NB ~: used evs2;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
# evs2 : ns_public"
--- a/src/HOL/Auth/NS_Shared.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Tue Sep 08 15:17:11 1998 +0200
@@ -16,7 +16,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= Server |] \
\ ==> EX N K. EX evs: ns_shared. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -35,14 +35,6 @@
(**** Inductive proofs about ns_shared ****)
-(*Nobody sends themselves messages*)
-Goal "evs : ns_shared ==> ALL X. Says A A X ~: set evs";
-by (etac ns_shared.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
(*For reasoning about the encrypted portion of message NS3*)
Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \
\ ==> X : parts (spies evs)";
--- a/src/HOL/Auth/NS_Shared.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 08 15:17:11 1998 +0200
@@ -21,12 +21,11 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_shared; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: ns_shared; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs1: ns_shared; A ~= Server; Nonce NA ~: used evs1 |]
+ NS1 "[| evs1: ns_shared; Nonce NA ~: used evs1 |]
==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
: ns_shared"
@@ -34,7 +33,7 @@
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2 "[| evs2: ns_shared; A ~= B; A ~= Server; Key KAB ~: used evs2;
+ NS2 "[| evs2: ns_shared; Key KAB ~: used evs2;
Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says Server A
(Crypt (shrK A)
@@ -43,8 +42,8 @@
# evs2 : ns_shared"
(*We can't assume S=Server. Agent A "remembers" her nonce.
- Can inductively show A ~= Server*)
- NS3 "[| evs3: ns_shared; A ~= B;
+ Need A ~= Server because we allow messages to self.*)
+ NS3 "[| evs3: ns_shared; A ~= Server;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evs3;
Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
@@ -52,7 +51,7 @@
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4 "[| evs4: ns_shared; A ~= B; Nonce NB ~: used evs4;
+ NS4 "[| evs4: ns_shared; Nonce NB ~: used evs4;
Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
==> Says B A (Crypt K (Nonce NB)) # evs4
: ns_shared"
@@ -62,7 +61,7 @@
We do NOT send NB-1 or similar as the Spy cannot spoof such things.
Letting the Spy add or subtract 1 lets him send ALL nonces.
Instead we distinguish the messages by sending the nonce twice.*)
- NS5 "[| evs5: ns_shared; A ~= B;
+ NS5 "[| evs5: ns_shared;
Says B' A (Crypt K (Nonce NB)) : set evs5;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evs5 |]
--- a/src/HOL/Auth/OtwayRees.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Tue Sep 08 15:17:11 1998 +0200
@@ -18,7 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
@@ -30,15 +30,6 @@
(**** Inductive proofs about otway ****)
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(** For reasoning about the encrypted portion of messages **)
Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
--- a/src/HOL/Auth/OtwayRees.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Tue Sep 08 15:17:11 1998 +0200
@@ -20,15 +20,16 @@
(*Initial trace is empty*)
Nil "[]: otway"
+ (** These rules allow agents to send messages to themselves **)
+
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1: otway; A ~= B; B ~= Server; Nonce NA ~: used evs1 |]
+ OR1 "[| evs1: otway; Nonce NA ~: used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 : otway"
@@ -36,7 +37,7 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
- OR2 "[| evs2: otway; B ~= Server; Nonce NB ~: used evs2;
+ OR2 "[| evs2: otway; Nonce NB ~: used evs2;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
@@ -47,7 +48,7 @@
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs3: otway; B ~= Server; Key KAB ~: used evs3;
+ OR3 "[| evs3: otway; Key KAB ~: used evs3;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -60,8 +61,9 @@
# evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.*)
- OR4 "[| evs4: otway; A ~= B;
+ those in the message he previously sent the Server.
+ Need B ~= Server because we allow messages to self.*)
+ OR4 "[| evs4: otway; B ~= Server;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 08 15:17:11 1998 +0200
@@ -18,10 +18,10 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway. \
-\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
-\ : set evs";
+Goal "[| B ~= Server |] \
+\ ==> EX K. EX NA. EX evs: otway. \
+\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by possibility_tac;
@@ -30,15 +30,6 @@
(**** Inductive proofs about otway ****)
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(** For reasoning about the encrypted portion of messages **)
Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
@@ -196,12 +187,12 @@
(**** Authenticity properties relating to NA ****)
(*If the encrypted message appears then it originated with the Server!*)
-Goal "[| A ~: bad; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
-\ --> (EX NB. Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs)";
+Goal "[| A ~: bad; A ~= B; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
+\ --> (EX NB. Says Server B \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+\ : set evs)";
by (parts_induct_tac 1);
by (Blast_tac 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
@@ -214,7 +205,7 @@
Freshness may be inferred from nonce NA.*)
Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
-\ A ~: bad; evs : otway |] \
+\ A ~: bad; A ~= B; evs : otway |] \
\ ==> EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -266,8 +257,8 @@
what it is.*)
Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
-\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
+\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; A ~= B; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
qed "A_gets_good_key";
@@ -276,7 +267,7 @@
(**** Authenticity properties relating to NB ****)
(*If the encrypted message appears then it originated with the Server!*)
-Goal "[| B ~: bad; evs : otway |] \
+Goal "[| B ~: bad; A ~= B; evs : otway |] \
\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
\ --> (EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
@@ -294,7 +285,7 @@
has sent the correct message in round 3.*)
Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
-\ B ~: bad; evs : otway |] \
+\ B ~: bad; A ~= B; evs : otway |] \
\ ==> EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -305,9 +296,9 @@
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs; \
-\ ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
+\ : set evs; \
+\ ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; A ~= B; evs : otway |] \
\ ==> Key K ~: analz (spies evs)";
by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
qed "B_gets_good_key";
--- a/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 08 15:17:11 1998 +0200
@@ -28,24 +28,23 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1: otway; A ~= B; B ~= Server |]
+ OR1 "[| evs1: otway |]
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- OR2 "[| evs2: otway; B ~= Server;
+ OR2 "[| evs2: otway;
Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
# evs2 : otway"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
- OR3 "[| evs3: otway; B ~= Server; A ~= B; Key KAB ~: used evs3;
+ OR3 "[| evs3: otway; Key KAB ~: used evs3;
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set evs3 |]
==> Says Server B
@@ -54,8 +53,9 @@
# evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.*)
- OR4 "[| evs4: otway; A ~= B;
+ those in the message he previously sent the Server.
+ Need B ~= Server because we allow messages to self.*)
+ OR4 "[| evs4: otway; B ~= Server;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set evs4 |]
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 08 15:17:11 1998 +0200
@@ -21,10 +21,10 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway. \
-\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\ : set evs";
+Goal "[| A ~= B; B ~= Server |] \
+\ ==> EX K. EX NA. EX evs: otway. \
+\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by possibility_tac;
@@ -33,14 +33,6 @@
(**** Inductive proofs about otway ****)
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
(** For reasoning about the encrypted portion of messages **)
@@ -232,9 +224,8 @@
(*** Attempting to prove stronger properties ***)
(*Only OR1 can have caused such a part of a message to appear.
- I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
- Perhaps it's because OR2 has two similar-looking encrypted messages in
- this version.*)
+ The premise A ~= B prevents OR2's similar-looking cryptogram from being
+ picked up. Original Otway-Rees doesn't need it.*)
Goal "[| A ~: bad; A ~= B; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
--- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 08 15:17:11 1998 +0200
@@ -22,11 +22,11 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Spy; X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1: otway; A ~= B; B ~= Server; Nonce NA ~: used evs1 |]
+ OR1 "[| evs1: otway; Nonce NA ~: used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 : otway"
@@ -34,7 +34,7 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
We modify the published protocol by NOT encrypting NB.*)
- OR2 "[| evs2: otway; B ~= Server; Nonce NB ~: used evs2;
+ OR2 "[| evs2: otway; Nonce NB ~: used evs2;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
@@ -44,7 +44,7 @@
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs3: otway; B ~= Server; Key KAB ~: used evs3;
+ OR3 "[| evs3: otway; Key KAB ~: used evs3;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -58,8 +58,9 @@
# evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.*)
- OR4 "[| evs4: otway; A ~= B;
+ those in the message he previously sent the Server.
+ Need B ~= Server because we allow messages to self.*)
+ OR4 "[| evs4: otway; A ~= B; B ~= Server;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
: set evs4;
--- a/src/HOL/Auth/Recur.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Tue Sep 08 15:17:11 1998 +0200
@@ -8,7 +8,6 @@
Pretty.setdepth 30;
-
AddEs spies_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
@@ -21,27 +20,24 @@
(*Simplest case: Alice goes directly to the server*)
-Goal "A ~= Server \
-\ ==> EX K NA. EX evs: recur. \
-\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\ Agent Server|} : set evs";
+Goal "EX K NA. EX evs: recur. \
+\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
+\ END|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.RA1 RS
- (respond.One RSN (4,recur.RA3))) 2);
+by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2);
by possibility_tac;
result();
(*Case two: Alice, Bob and the server*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur. \
-\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} : set evs";
+Goal "EX K. EX NA. EX evs: recur. \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ END|} : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
- (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
+ (respond.One RS respond.Cons RSN (3,recur.RA3)) RS
recur.RA4) 2);
by basic_possibility_tac;
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
@@ -50,17 +46,16 @@
(*Case three: Alice, Bob, Charlie and the server
TOO SLOW to run every time!
-Goal "[| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur. \
-\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} : set evs";
+Goal "EX K. EX NA. EX evs: recur. \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ END|} : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
(respond.One RS respond.Cons RS respond.Cons RSN
- (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-(*SLOW: 70 seconds*)
+ (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+(*SLOW: 33 seconds*)
by basic_possibility_tac;
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
ORELSE
@@ -70,15 +65,6 @@
(**** Inductive proofs about recur ****)
-(*Nobody sends themselves messages*)
-Goal "evs : recur ==> ALL X. Says A A X ~: set evs";
-by (etac recur.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
by (etac respond.induct 1);
@@ -253,7 +239,7 @@
by (etac responses.induct 2);
by (ALLGOALS Asm_simp_tac);
(*Fake*)
-by (Fake_parts_insert_tac 1);
+by (blast_tac (claset() addIs [parts_insertI]) 1);
qed "Hash_imp_body";
@@ -323,17 +309,6 @@
(2, resp_analz_insert_lemma) RSN(2, rev_mp));
-(*The Server does not send such messages. This theorem lets us avoid
- assuming B~=Server in RA4.*)
-Goal "evs : recur \
-\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
-by (etac recur.induct 1);
-by (etac (respond.induct) 5);
-by Auto_tac;
-qed_spec_mp "Says_Server_not";
-AddSEs [Says_Server_not RSN (2,rev_notE)];
-
-
(*The last key returned by respond indeed appears in a certificate*)
Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
--- a/src/HOL/Auth/Recur.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Recur.thy Tue Sep 08 15:17:11 1998 +0200
@@ -8,6 +8,10 @@
Recur = Shared +
+(*End marker for message bundles*)
+syntax END :: msg
+translations "END" == "Number 0"
+
(*Two session keys are distributed to each agent except for the initiator,
who receives one.
Perhaps the two session keys could be bundled into a single message.
@@ -15,17 +19,15 @@
consts respond :: "event list => (msg*msg*key)set"
inductive "respond evs" (*Server's response to the nested message*)
intrs
- (*The message "Agent Server" marks the end of a list.*)
- One "[| A ~= Server; Key KAB ~: used evs |]
- ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|},
- {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
+ One "[| Key KAB ~: used evs |]
+ ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
+ {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
KAB) : respond evs"
(*The most recent session key is passed up to the caller*)
Cons "[| (PA, RA, KAB) : respond evs;
Key KBC ~: used evs; Key KBC ~: parts {RA};
- PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
- B ~= Server |]
+ 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|},
@@ -41,7 +43,7 @@
inductive "responses evs"
intrs
(*Server terminates lists*)
- Nil "Agent Server : responses evs"
+ Nil "END : responses evs"
Cons "[| RA : responses evs; Key KAB ~: used evs |]
==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
@@ -56,35 +58,31 @@
(*The spy MAY say anything he CAN say. Common to
all similar protocols.*)
- Fake "[| evs: recur; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: recur; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : recur"
(*Alice initiates a protocol run.
- "Agent Server" is just a placeholder, to terminate the nesting.*)
- RA1 "[| evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 |]
- ==> Says A B
- (Hash[Key(shrK A)]
- {|Agent A, Agent B, Nonce NA, Agent Server|})
+ END is a placeholder to terminate the nesting.*)
+ RA1 "[| evs1: recur; Nonce NA ~: used evs1 |]
+ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
# evs1 : 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
it complicates proofs, so B may respond to any message at all!*)
- RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2;
+ RA2 "[| evs2: recur; Nonce NB ~: used evs2;
Says A' B PA : set evs2 |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs2 : recur"
(*The Server receives Bob's message and prepares a response.*)
- RA3 "[| evs3: recur; B ~= Server;
- Says B' Server PB : set evs3;
+ RA3 "[| evs3: recur; Says B' Server PB : set evs3;
(PB,RB,K) : respond evs3 |]
==> Says Server B RB # evs3 : recur"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
- RA4 "[| evs4: recur; A ~= B;
+ RA4 "[| evs4: recur;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
--- a/src/HOL/Auth/TLS.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 08 15:17:11 1998 +0200
@@ -82,8 +82,7 @@
"[]: tls"
Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
- "[| evs: tls; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ "[| evs: tls; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : tls"
SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
@@ -100,7 +99,7 @@
UNIX TIME is omitted because the protocol doesn't use it.
May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
while MASTER SECRET is 48 bytes*)
- "[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |]
+ "[| evsCH: tls; Nonce NA ~: used evsCH; NA ~: range PRF |]
==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
# evsCH : tls"
@@ -109,14 +108,14 @@
PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
SERVER CERTIFICATE (7.4.2) is always present.
CERTIFICATE_REQUEST (7.4.4) is implied.*)
- "[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF;
+ "[| evsSH: tls; Nonce NB ~: used evsSH; NB ~: range PRF;
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSH |]
==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH : tls"
Certificate
(*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
- "[| evsC: tls; A ~= B |]
+ "[| evsC: tls |]
==> Says B A (certificate B (pubK B)) # evsC : tls"
ClientKeyExch
@@ -128,7 +127,7 @@
both items have the same length, 48 bytes).
The Note event records in the trace that she knows PMS
(see REMARK at top). *)
- "[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF;
+ "[| evsCX: tls; Nonce PMS ~: used evsCX; PMS ~: range PRF;
Says B' A (certificate B KB) : set evsCX |]
==> Says A B (Crypt KB (Nonce PMS))
# Notes A {|Agent B, Nonce PMS|}
@@ -140,7 +139,7 @@
It adds the pre-master-secret, which is also essential!
Checking the signature, which is the only use of A's certificate,
assures B of A's presence*)
- "[| evsCV: tls; A ~= B;
+ "[| evsCV: tls;
Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
Notes A {|Agent B, Nonce PMS|} : set evsCV |]
==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
@@ -206,6 +205,7 @@
needed to resume this session. The "Says A'' B ..." premise is
used to prove Notes_master_imp_Crypt_PMS.*)
"[| evsSA: tls;
+ A ~= B;
Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
M = PRF(PMS,NA,NB);
X = Hash{|Number SID, Nonce M,
@@ -245,8 +245,9 @@
Oops
(*The most plausible compromise is of an old session key. Losing
the MASTER SECRET or PREMASTER SECRET is more serious but
- rather unlikely.*)
- "[| evso: tls; A ~= Spy;
+ rather unlikely. The assumption A ~= Spy is essential: otherwise
+ the Spy could learn session keys merely by replaying messages!*)
+ "[| evso: tls; A ~= Spy;
Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso : tls"
--- a/src/HOL/Auth/WooLam.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/WooLam.ML Tue Sep 08 15:17:11 1998 +0200
@@ -16,8 +16,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX NB. EX evs: woolam. \
+Goal "EX NB. EX evs: woolam. \
\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
@@ -28,15 +27,6 @@
(**** Inductive proofs about woolam ****)
-(*Nobody sends themselves messages*)
-Goal "evs : woolam ==> ALL X. Says A A X ~: set evs";
-by (etac woolam.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(** For reasoning about the encrypted portion of messages **)
Goal "Says A' B X : set evs ==> X : analz (spies evs)";
--- a/src/HOL/Auth/WooLam.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/WooLam.thy Tue Sep 08 15:17:11 1998 +0200
@@ -22,20 +22,20 @@
(*Initial trace is empty*)
Nil "[]: woolam"
+ (** These rules allow agents to send messages to themselves **)
+
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: woolam; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: woolam; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : woolam"
(*Alice initiates a protocol run*)
- WL1 "[| evs1: woolam; A ~= B |]
+ WL1 "[| evs1: woolam |]
==> Says A B (Agent A) # evs1 : woolam"
(*Bob responds to Alice's message with a challenge.*)
- WL2 "[| evs2: woolam; A ~= B;
- Says A' B (Agent A) : set evs2 |]
+ WL2 "[| evs2: woolam; Says A' B (Agent A) : set evs2 |]
==> Says B A (Nonce NB) # evs2 : woolam"
(*Alice responds to Bob's challenge by encrypting NB with her key.
@@ -50,13 +50,13 @@
the messages are shown in chronological order, for clarity.
But here, exchanging the two events would cause the lemma
WL4_analz_spies to pick up the wrong assumption!*)
- WL4 "[| evs4: woolam; B ~= Server;
+ WL4 "[| evs4: woolam;
Says A' B X : set evs4;
Says A'' B (Agent A) : set evs4 |]
==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
(*Server decrypts Alice's response for Bob.*)
- WL5 "[| evs5: woolam; B ~= Server;
+ WL5 "[| evs5: woolam;
Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
: set evs5 |]
==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
--- a/src/HOL/Auth/Yahalom.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML Tue Sep 08 15:17:11 1998 +0200
@@ -14,7 +14,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "A ~= Server \
\ ==> EX X NB K. EX evs: yahalom. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -26,14 +26,6 @@
(**** Inductive proofs about yahalom ****)
-(*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
(** For reasoning about the encrypted portion of messages **)
@@ -109,8 +101,7 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set evs; \
-\ evs : yahalom |] \
+\ : set evs; evs : yahalom |] \
\ ==> K ~: range shrK";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
--- a/src/HOL/Auth/Yahalom.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom.thy Tue Sep 08 15:17:11 1998 +0200
@@ -21,17 +21,16 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: yahalom; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: yahalom; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs1: yahalom; A ~= B; Nonce NA ~: used evs1 |]
+ YM1 "[| evs1: yahalom; Nonce NA ~: used evs1 |]
==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs2: yahalom; B ~= Server; Nonce NB ~: used evs2;
+ YM2 "[| evs2: yahalom; Nonce NB ~: used evs2;
Says A' B {|Agent A, Nonce NA|} : set evs2 |]
==> Says B Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
@@ -39,7 +38,7 @@
(*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: yahalom; A ~= Server; Key KAB ~: used evs3;
+ YM3 "[| evs3: yahalom; Key KAB ~: used evs3;
Says B' Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
: set evs3 |]
@@ -50,8 +49,8 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
- A ~= Server is needed to prove Says_Server_message_form.*)
- YM4 "[| evs4: yahalom; A ~= Server;
+ A ~= Server is needed to prove Says_Server_not_range.*)
+ YM4 "[| evs4: yahalom; A ~= Server;
Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evs4;
Says A B {|Agent A, Nonce NA|} : set evs4 |]
--- a/src/HOL/Auth/Yahalom2.ML Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Tue Sep 08 15:17:11 1998 +0200
@@ -18,8 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX X NB K. EX evs: yahalom. \
+Goal "EX X NB K. EX evs: yahalom. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
@@ -30,15 +29,6 @@
(**** Inductive proofs about yahalom ****)
-(*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs [not_Says_to_self RSN (2, rev_notE)];
-
-
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
@@ -114,7 +104,7 @@
Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
\ : set evs; \
\ evs : yahalom |] \
-\ ==> K ~: range shrK & A ~= B";
+\ ==> K ~: range shrK";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
@@ -191,8 +181,7 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-Goal "[| A ~: bad; B ~: bad; A ~= B; \
-\ evs : yahalom |] \
+Goal "[| A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
--- a/src/HOL/Auth/Yahalom2.thy Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Tue Sep 08 15:17:11 1998 +0200
@@ -24,17 +24,16 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: yahalom; B ~= Spy;
- X: synth (analz (spies evs)) |]
+ Fake "[| evs: yahalom; X: synth (analz (spies evs)) |]
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs1: yahalom; A ~= B; Nonce NA ~: used evs1 |]
+ YM1 "[| evs1: yahalom; Nonce NA ~: used evs1 |]
==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs2: yahalom; B ~= Server; Nonce NB ~: used evs2;
+ YM2 "[| evs2: yahalom; Nonce NB ~: used evs2;
Says A' B {|Agent A, Nonce NA|} : set evs2 |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
@@ -43,7 +42,7 @@
(*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: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs3;
+ YM3 "[| evs3: yahalom; Key KAB ~: used evs3;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
: set evs3 |]
@@ -55,7 +54,7 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs4: yahalom; A ~= Server;
+ YM4 "[| evs4: yahalom;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evs4;
Says A B {|Agent A, Nonce NA|} : set evs4 |]