# HG changeset patch # User paulson # Date 1475251970 -3600 # Node ID 6728b5007ad026a5d48747a3157b898b029d3e7a # Parent 721810140424bfe6c251612650eca6a86d012c0b Trying out "subgoal", and no more [| |] diff -r 721810140424 -r 6728b5007ad0 src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Fri Sep 30 15:51:43 2016 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Fri Sep 30 17:12:50 2016 +0100 @@ -21,62 +21,62 @@ (*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: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] - ==> Says Spy B X # evsf \ otway" + | Fake: "\evsf \ otway; X \ synth (analz (knows Spy evsf)) \ + \ Says Spy B X # evsf \ otway" (*A message that has been sent can be received by the intended recipient.*) - | Reception: "[| evsr \ otway; Says A B X \set evsr |] - ==> Gets B X # evsr \ otway" + | Reception: "\evsr \ otway; Says A B X \set evsr\ + \ Gets B X # evsr \ otway" (*Alice initiates a protocol run*) - | OR1: "[| evs1 \ otway; Nonce NA \ used evs1 |] - ==> Says A B \Nonce NA, Agent A, Agent B, + | 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" + # evs1 \ otway" (*Bob's response to Alice's message. Note that NB is encrypted.*) - | OR2: "[| evs2 \ otway; Nonce NB \ used evs2; - Gets B \Nonce NA, Agent A, Agent B, X\ : set evs2 |] - ==> Says B Server + | OR2: "\evs2 \ otway; Nonce NB \ used evs2; + Gets B \Nonce NA, Agent A, Agent B, X\ : set evs2\ + \ Says B Server \Nonce NA, Agent A, Agent B, X, Crypt (shrK B) \Nonce NA, Nonce NB, Agent A, Agent B\\ - # evs2 : otway" + # evs2 \ otway" (*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; Key KAB \ used evs3; + | OR3: "\evs3 \ otway; Key KAB \ 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\\ - : set evs3 |] - ==> Says Server B + : set evs3\ + \ Says Server B \Nonce NA, Crypt (shrK A) \Nonce NA, Key KAB\, Crypt (shrK B) \Nonce NB, Key KAB\\ - # evs3 : otway" + # evs3 \ otway" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need B \ Server because we allow messages to self.*) - | OR4: "[| evs4 \ otway; B \ Server; + | 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\\ : set evs4; Gets B \Nonce NA, X, Crypt (shrK B) \Nonce NB, Key K\\ - : set evs4 |] - ==> Says B A \Nonce NA, X\ # evs4 : otway" + : set evs4\ + \ Says B A \Nonce NA, X\ # evs4 \ otway" (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - | Oops: "[| evso \ otway; + | Oops: "\evso \ otway; Says Server B \Nonce NA, X, Crypt (shrK B) \Nonce NB, Key K\\ - : set evso |] - ==> Notes Spy \Nonce NA, Nonce NB, Key K\ # evso : otway" + : set evso\ + \ Notes Spy \Nonce NA, Nonce NB, Key K\ # evso \ otway" declare Says_imp_analz_Spy [dest] @@ -86,8 +86,8 @@ text\A "possibility property": there are traces that reach the end\ -lemma "[| B \ Server; Key K \ used [] |] - ==> \evs \ otway. +lemma "\B \ Server; Key K \ used []\ + \ \evs \ otway. Says B A \Nonce NA, Crypt (shrK A) \Nonce NA, Key K\\ \ set evs" apply (intro exI bexI) @@ -99,7 +99,7 @@ done lemma Gets_imp_Says [dest!]: - "[| Gets B X \ set evs; evs \ otway |] ==> \A. Says A B X \ set evs" + "\Gets B X \ set evs; evs \ otway\ \ \A. Says A B X \ set evs" apply (erule rev_mp) apply (erule otway.induct, auto) done @@ -108,13 +108,13 @@ (** For reasoning about the encrypted portion of messages **) lemma OR2_analz_knows_Spy: - "[| Gets B \N, Agent A, Agent B, X\ \ set evs; evs \ otway |] - ==> X \ analz (knows Spy evs)" + "\Gets B \N, Agent A, Agent B, X\ \ set evs; evs \ otway\ + \ X \ analz (knows Spy evs)" by blast lemma OR4_analz_knows_Spy: - "[| Gets B \N, X, Crypt (shrK B) X'\ \ set evs; evs \ otway |] - ==> X \ analz (knows Spy evs)" + "\Gets B \N, X, Crypt (shrK B) X'\ \ set evs; evs \ otway\ + \ X \ analz (knows Spy evs)" by blast (*These lemmas assist simplification by removing forwarded X-variables. @@ -132,17 +132,17 @@ text\Spy never sees a good agent's shared key!\ lemma Spy_see_shrK [simp]: - "evs \ otway ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" + "evs \ otway \ (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)" by (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) lemma Spy_analz_shrK [simp]: - "evs \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" + "evs \ otway \ (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" by auto lemma Spy_see_shrK_D [dest!]: - "[|Key (shrK A) \ parts (knows Spy evs); evs \ otway|] ==> A \ bad" + "\Key (shrK A) \ parts (knows Spy evs); evs \ otway\ \ A \ bad" by (blast dest: Spy_see_shrK) @@ -151,16 +151,16 @@ (*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\\ \ set evs; - evs \ otway |] - ==> K \ range shrK & (\i. NA = Nonce i) & (\j. NB = Nonce j)" + "\Says Server B \NA, X, Crypt (shrK B) \NB, Key K\\ \ set evs; + evs \ otway\ + \ K \ range shrK & (\i. NA = Nonce i) & (\j. NB = Nonce j)" by (erule rev_mp, erule otway.induct, simp_all) (**** The following is to prove theorems of the form - Key K \ analz (insert (Key KAB) (knows Spy evs)) ==> + Key K \ analz (insert (Key KAB) (knows Spy evs)) \ Key K \ analz (knows Spy evs) A more general formula must be proved inductively. @@ -171,7 +171,7 @@ text\The equality makes the induction hypothesis easier to apply\ lemma analz_image_freshK [rule_format]: - "evs \ otway ==> + "evs \ otway \ \K KK. KK <= -(range shrK) --> (Key K \ analz (Key`KK Un (knows Spy evs))) = (K \ KK | Key K \ analz (knows Spy evs))" @@ -182,7 +182,7 @@ done lemma analz_insert_freshK: - "[| evs \ otway; KAB \ range shrK |] ==> + "\evs \ otway; KAB \ range shrK\ \ (Key K \ analz (insert (Key KAB) (knows Spy evs))) = (K = KAB | Key K \ analz (knows Spy evs))" by (simp only: analz_image_freshK analz_image_freshK_simps) @@ -190,9 +190,9 @@ text\The Key K uniquely identifies the Server's message.\ lemma unique_session_keys: - "[| Says Server B \NA, X, Crypt (shrK B) \NB, K\\ \ set evs; + "\Says Server B \NA, X, Crypt (shrK B) \NB, K\\ \ set evs; Says Server B' \NA',X',Crypt (shrK B') \NB',K\\ \ set evs; - evs \ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" + evs \ otway\ \ X=X' & B=B' & NA=NA' & NB=NB'" apply (erule rev_mp) apply (erule rev_mp) apply (erule otway.induct, simp_all) @@ -204,8 +204,8 @@ text\Only OR1 can have caused such a part of a message to appear.\ lemma Crypt_imp_OR1 [rule_format]: - "[| A \ bad; evs \ otway |] - ==> Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs) --> + "\A \ bad; evs \ otway\ + \ Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs) --> Says A B \NA, Agent A, Agent B, Crypt (shrK A) \NA, Agent A, Agent B\\ \ set evs" @@ -213,10 +213,10 @@ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) lemma Crypt_imp_OR1_Gets: - "[| Gets B \NA, Agent A, Agent B, + "\Gets B \NA, Agent A, Agent B, Crypt (shrK A) \NA, Agent A, Agent B\\ \ set evs; - A \ bad; evs \ otway |] - ==> Says A B \NA, Agent A, Agent B, + A \ bad; evs \ otway\ + \ Says A B \NA, Agent A, Agent B, Crypt (shrK A) \NA, Agent A, Agent B\\ \ set evs" by (blast dest: Crypt_imp_OR1) @@ -224,10 +224,10 @@ text\The Nonce NA uniquely identifies A's message\ lemma unique_NA: - "[| Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs); + "\Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs); Crypt (shrK A) \NA, Agent A, Agent C\ \ parts (knows Spy evs); - evs \ otway; A \ bad |] - ==> B = C" + evs \ otway; A \ bad\ + \ B = C" apply (erule rev_mp, erule rev_mp) apply (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) @@ -238,9 +238,9 @@ OR2 encrypts Nonce NB. It prevents the attack that can occur in the over-simplified version of this protocol: see \OtwayRees_Bad\.\ lemma no_nonce_OR1_OR2: - "[| Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs); - A \ bad; evs \ otway |] - ==> Crypt (shrK A) \NA', NA, Agent A', Agent A\ \ parts (knows Spy evs)" + "\Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs); + A \ bad; evs \ otway\ + \ Crypt (shrK A) \NA', NA, Agent A', Agent A\ \ parts (knows Spy evs)" apply (erule rev_mp) apply (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) @@ -249,8 +249,8 @@ text\Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server!\ lemma NA_Crypt_imp_Server_msg [rule_format]: - "[| A \ bad; evs \ otway |] - ==> Says A B \NA, Agent A, Agent B, + "\A \ bad; evs \ otway\ + \ Says A B \NA, Agent A, Agent B, Crypt (shrK A) \NA, Agent A, Agent B\\ \ set evs --> Crypt (shrK A) \NA, Key K\ \ parts (knows Spy evs) --> (\NB. Says Server B @@ -259,9 +259,12 @@ Crypt (shrK B) \NB, Key K\\ \ set evs)" apply (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) -apply blast \\OR1: by freshness\ -apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) \\OR3\ -apply (blast intro!: Crypt_imp_OR1) \\OR4\ + subgoal \\OR1: by freshness\ + by blast + subgoal \\OR3\ + by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) + subgoal \\OR4\ + by (blast intro!: Crypt_imp_OR1) done @@ -270,11 +273,11 @@ bad form of this protocol, even though we can prove \Spy_not_see_encrypted_key\\ lemma A_trusts_OR4: - "[| Says A B \NA, Agent A, Agent B, + "\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; - A \ bad; evs \ otway |] - ==> \NB. Says Server B + A \ bad; evs \ otway\ + \ \NB. Says Server B \NA, Crypt (shrK A) \NA, Key K\, Crypt (shrK B) \NB, Key K\\ @@ -286,28 +289,32 @@ Does not in itself guarantee security: an attack could violate the premises, e.g. by having @{term "A=Spy"}\ lemma secrecy_lemma: - "[| A \ bad; B \ bad; evs \ otway |] - ==> Says Server B + "\A \ bad; B \ bad; evs \ otway\ + \ Says Server B \NA, Crypt (shrK A) \NA, Key K\, Crypt (shrK B) \NB, Key K\\ \ set evs --> Notes Spy \NA, NB, Key K\ \ set evs --> Key K \ analz (knows Spy evs)" -apply (erule otway.induct, force) -apply (frule_tac [7] Says_Server_message_form) -apply (drule_tac [6] OR4_analz_knows_Spy) -apply (drule_tac [4] OR2_analz_knows_Spy) -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) -apply spy_analz \\Fake\ -apply (blast dest: unique_session_keys)+ \\OR3, OR4, Oops\ -done + apply (erule otway.induct, force, simp_all) + subgoal \\Fake\ + by spy_analz + subgoal \\OR2\ + by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq) + subgoal \\OR3\ + by (auto simp add: analz_insert_freshK pushes) + subgoal \\OR4\ + by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq) + subgoal \\Oops\ + by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys) + done theorem Spy_not_see_encrypted_key: - "[| Says Server B + "\Says Server B \NA, Crypt (shrK A) \NA, Key K\, 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 (knows Spy evs)" + A \ bad; B \ bad; evs \ otway\ + \ Key K \ analz (knows Spy evs)" by (blast dest: Says_Server_message_form secrecy_lemma) text\This form is an immediate consequence of the previous result. It is @@ -318,24 +325,24 @@ other than Fake are trivial, while Fake requires @{term "Key K \ analz (knows Spy evs)"}.\ lemma Spy_not_know_encrypted_key: - "[| Says Server B + "\Says Server B \NA, Crypt (shrK A) \NA, Key K\, Crypt (shrK B) \NB, Key K\\ \ set evs; Notes Spy \NA, NB, Key K\ \ set evs; - A \ bad; B \ bad; evs \ otway |] - ==> Key K \ knows Spy evs" + A \ bad; B \ bad; evs \ otway\ + \ Key K \ knows Spy evs" by (blast dest: Spy_not_see_encrypted_key) text\A's guarantee. The Oops premise quantifies over NB because A cannot know what it is.\ lemma A_gets_good_key: - "[| Says A B \NA, Agent A, Agent B, + "\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; \NB. Notes Spy \NA, NB, Key K\ \ set evs; - A \ bad; B \ bad; evs \ otway |] - ==> Key K \ analz (knows Spy evs)" + A \ bad; B \ bad; evs \ otway\ + \ Key K \ analz (knows Spy evs)" by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) @@ -344,9 +351,9 @@ text\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.\ lemma Crypt_imp_OR2: - "[| Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts (knows Spy evs); - B \ bad; evs \ otway |] - ==> \X. Says B Server + "\Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts (knows Spy evs); + B \ bad; evs \ otway\ + \ \X. Says B Server \NA, Agent A, Agent B, X, Crypt (shrK B) \NA, NB, Agent A, Agent B\\ \ set evs" @@ -358,10 +365,10 @@ text\The Nonce NB uniquely identifies B's message\ lemma unique_NB: - "[| Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts(knows Spy evs); + "\Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts(knows Spy evs); Crypt (shrK B) \NC, NB, Agent C, Agent B\ \ parts(knows Spy evs); - evs \ otway; B \ bad |] - ==> NC = NA & C = A" + evs \ otway; B \ bad\ + \ NC = NA & C = A" apply (erule rev_mp, erule rev_mp) apply (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all) @@ -371,8 +378,8 @@ text\If the encrypted message appears, and B has used Nonce NB, then it originated with the Server! Quite messy proof.\ lemma NB_Crypt_imp_Server_msg [rule_format]: - "[| B \ bad; evs \ otway |] - ==> Crypt (shrK B) \NB, Key K\ \ parts (knows Spy evs) + "\B \ bad; evs \ otway\ + \ Crypt (shrK B) \NB, Key K\ \ parts (knows Spy evs) --> (\X'. Says B Server \NA, Agent A, Agent B, X', Crypt (shrK B) \NA, NB, Agent A, Agent B\\ @@ -382,24 +389,27 @@ Crypt (shrK B) \NB, Key K\\ \ set evs)" apply simp -apply (erule otway.induct, force, - drule_tac [4] OR2_parts_knows_Spy, simp_all) -apply blast \\Fake\ -apply blast \\OR2\ -apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \\OR3\ -apply (blast dest!: Crypt_imp_OR2) \\OR4\ +apply (erule otway.induct, force, simp_all) + subgoal \\Fake\ + by blast + subgoal \\OR2\ + by (force dest!: OR2_parts_knows_Spy) + subgoal \\OR3\ + by (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \\OR3\ + subgoal \\OR4\ + by (blast dest!: Crypt_imp_OR2) done text\Guarantee for B: if it gets a message with matching NB then the Server has sent the correct message.\ theorem B_trusts_OR3: - "[| Says B Server \NA, Agent A, Agent B, X', + "\Says B Server \NA, Agent A, Agent B, X', Crypt (shrK B) \NA, NB, Agent A, Agent B\\ \ set evs; Gets B \NA, X, Crypt (shrK B) \NB, Key K\\ \ set evs; - B \ bad; evs \ otway |] - ==> Says Server B + B \ bad; evs \ otway\ + \ Says Server B \NA, Crypt (shrK A) \NA, Key K\, Crypt (shrK B) \NB, Key K\\ @@ -410,22 +420,22 @@ text\The obvious combination of \B_trusts_OR3\ with \Spy_not_see_encrypted_key\\ lemma B_gets_good_key: - "[| Says B Server \NA, Agent A, Agent B, X', + "\Says B Server \NA, Agent A, Agent B, X', Crypt (shrK B) \NA, NB, Agent A, Agent B\\ \ set evs; Gets 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 (knows Spy evs)" + A \ bad; B \ bad; evs \ otway\ + \ Key K \ analz (knows Spy evs)" by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key) lemma OR3_imp_OR2: - "[| Says Server B + "\Says Server B \NA, Crypt (shrK A) \NA, Key K\, Crypt (shrK B) \NB, Key K\\ \ set evs; - B \ bad; evs \ otway |] - ==> \X. Says B Server \NA, Agent A, Agent B, X, + B \ bad; evs \ otway\ + \ \X. Says B Server \NA, Agent A, Agent B, X, Crypt (shrK B) \NA, NB, Agent A, Agent B\\ \ set evs" apply (erule rev_mp) @@ -438,11 +448,11 @@ We could probably prove that X has the expected form, but that is not strictly necessary for authentication.\ theorem A_auths_B: - "[| Says B' A \NA, Crypt (shrK A) \NA, Key K\\ \ set 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 |] - ==> \NB X. Says B Server \NA, Agent A, Agent B, X, + A \ bad; B \ bad; evs \ otway\ + \ \NB X. Says B Server \NA, Agent A, Agent B, X, Crypt (shrK B) \NA, NB, Agent A, Agent B\\ \ set evs" by (blast dest!: A_trusts_OR4 OR3_imp_OR2)