Added some more explicit guarantees of key secrecy for agents
Deleted spurious A~=Spy assumptions
--- a/src/HOL/Auth/OtwayRees.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Thu Feb 05 10:38:34 1998 +0100
@@ -259,7 +259,7 @@
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
goal thy
- "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \
+ "!!evs. [| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
@@ -291,10 +291,10 @@
bad form of this protocol, even though we can prove
Spy_not_see_encrypted_key*)
goal thy
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
-\ Says A B {|NA, Agent A, Agent B, \
+ "!!evs. [| Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\ A ~: bad; A ~= Spy; evs : otway |] \
+\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ A ~: bad; evs : otway |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
@@ -343,6 +343,19 @@
qed "Spy_not_see_encrypted_key";
+(*A's guarantee. The Oops premise quantifies over NB because A cannot know
+ what it is.*)
+goal thy
+ "!!evs. [| Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; 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";
+
+
(**** Authenticity properties relating to NB ****)
(*Only OR2 can have caused such a part of a message to appear. We do not
@@ -363,8 +376,8 @@
(** The Nonce NB uniquely identifies B's message. **)
goal thy
- "!!evs. [| evs : otway; B ~: bad |] \
-\ ==> EX NA' A'. ALL NA A. \
+ "!!evs. [| evs : otway; B ~: bad |] \
+\ ==> EX NA' A'. ALL NA A. \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
\ --> NA = NA' & A = A'";
by (parts_induct_tac 1);
@@ -387,8 +400,8 @@
(*If the encrypted message appears, and B has used Nonce NB,
then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: bad; B ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \
+ "!!evs. [| B ~: bad; evs : otway |] \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -418,11 +431,11 @@
(*Guarantee for B: if it gets a message with matching NB then the Server
has sent the correct message.*)
goal thy
- "!!evs. [| B ~: bad; B ~= Spy; evs : otway; \
-\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Server {|NA, Agent A, Agent B, X', \
+ "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ : set evs |] \
+\ : set evs; \
+\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
@@ -432,11 +445,21 @@
qed "B_trusts_OR3";
-B_trusts_OR3 RS Spy_not_see_encrypted_key;
+(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| Says B Server {|NA, Agent A, Agent B, X', \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
+\ : set evs; \
+\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : otway |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
+qed "B_gets_good_key";
goal thy
- "!!evs. [| B ~: bad; evs : otway |] \
+ "!!evs. [| B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
@@ -454,11 +477,11 @@
We could probably prove that X has the expected form, but that is not
strictly necessary for authentication.*)
goal thy
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\ A ~: bad; A ~= Spy; B ~: bad; evs : otway |] \
-\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\ A ~: bad; B ~: bad; evs : otway |] \
+\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
\ : set evs";
by (blast_tac (claset() addSDs [A_trusts_OR4]
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Feb 05 10:38:34 1998 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/Auth/OtwayRees
+(* Title: HOL/Auth/OtwayRees_AN
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Inductive relation "otway" for the Otway-Rees protocol.
-Simplified version with minimal encryption but explicit messages
+Abadi-Needham version: minimal encryption, explicit messages
From page 11 of
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
@@ -147,8 +147,8 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+ "!!evs. evs : otway ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
@@ -162,7 +162,7 @@
goal thy
- "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
+ "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
@@ -280,6 +280,18 @@
qed "Spy_not_see_encrypted_key";
+(*A's guarantee. The Oops premise quantifies over NB because A cannot know
+ what it is.*)
+goal thy
+ "!!evs. [| 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 |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
+qed "A_gets_good_key";
+
+
(**** Authenticity properties relating to NB ****)
(*If the encrypted message appears then it originated with the Server!*)
@@ -301,12 +313,23 @@
(*Guarantee for B: if it gets a well-formed certificate then the Server
has sent the correct message in round 3.*)
goal thy
- "!!evs. [| B ~: bad; evs : otway; \
-\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs |] \
+ "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+\ : set evs; \
+\ B ~: bad; 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|}|} \
\ : set evs";
by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
qed "B_trusts_OR3";
+
+
+(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| 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 |] \
+\ ==> 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_Bad.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Feb 05 10:38:34 1998 +0100
@@ -266,8 +266,8 @@
(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
goal thy
- "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
+ "!!evs. [| A ~: bad; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
--- a/src/HOL/Auth/Recur.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/Recur.ML Thu Feb 05 10:38:34 1998 +0100
@@ -22,7 +22,7 @@
(*Simplest case: Alice goes directly to the server*)
goal thy
"!!A. A ~= Server \
-\ ==> EX K NA. EX evs: recur. \
+\ ==> EX K NA. EX evs: recur. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
\ Agent Server|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -35,7 +35,7 @@
(*Case two: Alice, Bob and the server*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur. \
+\ ==> EX K. EX NA. EX evs: recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
@@ -54,7 +54,7 @@
TOO SLOW to run every time!
goal thy
"!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
-\ ==> EX K. EX NA. EX evs: recur. \
+\ ==> EX K. EX NA. EX evs: recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
@@ -223,8 +223,8 @@
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
goal thy
- "!!evs. evs : recur ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+ "!!evs. evs : recur ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac recur.induct 1);
@@ -251,7 +251,7 @@
(2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
goal thy
- "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
+ "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
@@ -260,7 +260,7 @@
(*Everything that's hashed is already in past traffic. *)
goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] \
+\ evs : recur; A ~: bad |] \
\ ==> X : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -296,9 +296,9 @@
val lemma = result();
goalw thy [HPair_def]
- "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(spies evs); \
-\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
-\ evs : recur; A ~: bad |] \
+ "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \
+\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
+\ evs : recur; A ~: bad |] \
\ ==> B=B' & P=P'";
by (REPEAT (eresolve_tac partsEs 1));
by (prove_unique_tac lemma 1);
@@ -357,7 +357,7 @@
(*The last key returned by respond indeed appears in a certificate*)
goal thy
"!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
-\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
+\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
by (etac respond.elim 1);
by (ALLGOALS Asm_full_simp_tac);
qed "respond_certificate";
@@ -376,8 +376,8 @@
by (expand_case_tac "K = KBC" 1);
by (dtac respond_Key_in_parts 1);
by (blast_tac (claset() addSIs [exI]
- addSEs partsEs
- addDs [Key_in_parts_respond]) 1);
+ addSEs partsEs
+ addDs [Key_in_parts_respond]) 1);
by (expand_case_tac "K = KAB" 1);
by (REPEAT (ares_tac [exI] 2));
by (ex_strip_tac 1);
@@ -400,7 +400,7 @@
goal thy
"!!evs. [| (PB,RB,KAB) : respond evs; evs : recur |] \
-\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
+\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
\ Key K ~: analz (insert RB (spies evs))";
by (etac respond.induct 1);
@@ -495,8 +495,8 @@
(*Certificates can only originate with the Server.*)
goal thy
"!!evs. [| Crypt (shrK A) Y : parts (spies evs); \
-\ A ~: bad; A ~= Spy; evs : recur |] \
-\ ==> EX C RC. Says Server C RC : set evs & \
+\ A ~: bad; evs : recur |] \
+\ ==> EX C RC. Says Server C RC : set evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
by (parts_induct_tac 1);
--- a/src/HOL/Auth/Yahalom.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/Yahalom.ML Thu Feb 05 10:38:34 1998 +0100
@@ -255,6 +255,14 @@
by (Fake_parts_insert_tac 1);
qed "A_trusts_YM3";
+(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
+\ Notes Spy {|na, nb, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
+qed "A_gets_good_key";
(** Security Guarantees for B upon receiving YM4 **)
@@ -541,11 +549,11 @@
If this run is broken and the spy substitutes a certificate containing an
old key, B has no means of telling.*)
goal thy
- "!!evs. [| Says B Server \
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set evs; \
-\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set evs; \
\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> Says Server A \
@@ -564,6 +572,19 @@
qed "B_trusts_YM4";
+(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ Says B Server \
+\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
+\ : set evs; \
+\ ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
+qed "B_gets_good_key";
+
(*** Authenticating B to A ***)
@@ -638,15 +659,15 @@
Moreover, A associates K with NB (thus is talking about the same run).
Other premises guarantee secrecy of K.*)
goal thy
- "!!evs. [| Says B Server \
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set evs; \
-\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set evs; \
\ (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \
\ A ~: bad; B ~: bad; evs : yahalom |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
-by (dtac B_trusts_YM4 1);
+by (forward_tac [B_trusts_YM4] 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
by (rtac lemma 1);
--- a/src/HOL/Auth/Yahalom2.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Thu Feb 05 10:38:34 1998 +0100
@@ -261,6 +261,15 @@
by (Blast_tac 1);
qed "A_trusts_YM3";
+(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \
+\ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
+qed "A_gets_good_key";
+
(** Security Guarantee for B upon receiving YM4 **)
@@ -301,6 +310,17 @@
qed "B_trusts_YM4";
+(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+goal thy
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
+\ : set evs; \
+\ ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] \
+\ ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
+qed "B_gets_good_key";
+
+
(*** Authenticating B to A ***)
@@ -318,6 +338,7 @@
by (Blast_tac 1);
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
+
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
goal thy
"!!evs. evs : yahalom \