# HG changeset patch # User paulson # Date 886671514 -3600 # Node ID 649bf14debe7f642b455522223cfae1e48b82b67 # Parent a0bdee64194c85b5654cfc996ba8731757f3b9e1 Added some more explicit guarantees of key secrecy for agents Deleted spurious A~=Spy assumptions diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/OtwayRees.ML --- 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] diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/OtwayRees_AN.ML --- 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"; diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/OtwayRees_Bad.ML --- 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 --> \ diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/Recur.ML --- 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); diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/Yahalom.ML --- 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); diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/Yahalom2.ML --- 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 \