# HG changeset patch # User paulson # Date 988107541 -7200 # Node ID a47a9288f3f698a68661890a0b47258c6d258785 # Parent e502756bcb1129362eb8fbac1b2f97db1fb1c473 (rough) conversion of Auth/Recur to Isar format diff -r e502756bcb11 -r a47a9288f3f6 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Mon Apr 23 17:11:19 2001 +0200 +++ b/src/HOL/Auth/Message.thy Tue Apr 24 12:19:01 2001 +0200 @@ -146,4 +146,12 @@ Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} "for proving the Fake case when analz is involved" +method_setup atomic_spy_analz = {* + Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *} + "for debugging spy_analz" + +method_setup Fake_insert_simp = {* + Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *} + "for debugging spy_analz" + end diff -r e502756bcb11 -r a47a9288f3f6 src/HOL/Auth/Message_lemmas.ML --- a/src/HOL/Auth/Message_lemmas.ML Mon Apr 23 17:11:19 2001 +0200 +++ b/src/HOL/Auth/Message_lemmas.ML Tue Apr 24 12:19:01 2001 +0200 @@ -158,7 +158,7 @@ by (Blast_tac 1); qed "parts_increasing"; -val parts_insertI = impOfSubs (subset_insertI RS parts_mono); +bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono)); Goal "parts{} = {}"; by Safe_tac; diff -r e502756bcb11 -r a47a9288f3f6 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Mon Apr 23 17:11:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,404 +0,0 @@ -(* Title: HOL/Auth/Recur - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "recur" for the Recursive Authentication protocol. -*) - -Pretty.setdepth 30; - -AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; -AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; - - -(** Possibility properties: traces that reach the end - ONE theorem would be more elegant and faster! - By induction on a list of agents (no repetitions) -**) - - -(*Simplest case: Alice goes directly to the server*) -Goal "\\K NA. \\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 (3,recur.RA3))) 2); -by possibility_tac; -result(); - - -(*Case two: Alice, Bob and the server*) -Goal "\\K. \\NA. \\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 (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)); -result(); - - -(*Case three: Alice, Bob, Charlie and the server - TOO SLOW to run every time! -Goal "\\K. \\NA. \\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 - (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); -by basic_possibility_tac; -by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 - ORELSE - eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); -result(); -****************) - -(**** Inductive proofs about recur ****) - -Goal "(PA,RB,KAB) \\ respond evs ==> Key KAB \\ used evs"; -by (etac respond.induct 1); -by (REPEAT (assume_tac 1)); -qed "respond_imp_not_used"; - -Goal "[| Key K \\ parts {RB}; (PB,RB,K') \\ respond evs |] ==> Key K \\ used evs"; -by (etac rev_mp 1); -by (etac respond.induct 1); -by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used], - simpset())); -qed_spec_mp "Key_in_parts_respond"; - -(*Simple inductive reasoning about responses*) -Goal "(PA,RB,KAB) \\ respond evs ==> RB \\ responses evs"; -by (etac respond.induct 1); -by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); -qed "respond_imp_responses"; - - -(** For reasoning about the encrypted portion of messages **) - -val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; - -Goal "Says C' B {|Crypt K X, X', RA|} \\ set evs ==> RA \\ analz (spies evs)"; -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); -qed "RA4_analz_spies"; - -(*RA2_analz... and RA4_analz... let us treat those cases using the same - argument as for the Fake case. This is possible for most, but not all, - proofs: Fake does not invent new nonces (as in RA2), and of course Fake - messages originate from the Spy. *) - -bind_thm ("RA2_parts_spies", - RA2_analz_spies RS (impOfSubs analz_subset_parts)); -bind_thm ("RA4_parts_spies", - RA4_analz_spies RS (impOfSubs analz_subset_parts)); - -(*For proving the easier theorems about X \\ parts (spies evs).*) -fun parts_induct_tac i = - EVERY [etac recur.induct i, - ftac RA4_parts_spies (i+5), - ftac respond_imp_responses (i+4), - ftac RA2_parts_spies (i+3), - prove_simple_subgoals_tac i]; - - -(** Theorems of the form X \\ parts (spies evs) imply that NOBODY - sends messages containing X! **) - - -(** Spy never sees another agent's shared key! (unless it's bad at start) **) - -Goal "evs \\ recur ==> (Key (shrK A) \\ parts (spies evs)) = (A \\ bad)"; -by (parts_induct_tac 1); -by Auto_tac; -(*RA3*) -by (auto_tac (claset() addDs [Key_in_parts_respond], - simpset() addsimps [parts_insert_spies])); -qed "Spy_see_shrK"; -Addsimps [Spy_see_shrK]; - -Goal "evs \\ recur ==> (Key (shrK A) \\ analz (spies evs)) = (A \\ bad)"; -by Auto_tac; -qed "Spy_analz_shrK"; -Addsimps [Spy_analz_shrK]; - -AddSDs [Spy_see_shrK RSN (2, rev_iffD1), - Spy_analz_shrK RSN (2, rev_iffD1)]; - - - -(*** Proofs involving analz ***) - -(*For proofs involving analz.*) -val analz_spies_tac = - dtac RA2_analz_spies 4 THEN - ftac respond_imp_responses 5 THEN - dtac RA4_analz_spies 6; - - -(** Session keys are not used to encrypt other session keys **) - -(*Version for "responses" relation. Handles case RA3 in the theorem below. - Note that it holds for *any* set H (not just "spies evs") - satisfying the inductive hypothesis.*) -Goal "[| RB \\ responses evs; \ -\ \\K KK. KK \\ - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un H)) = \ -\ (K \\ KK | Key K \\ analz H) |] \ -\ ==> \\K KK. KK \\ - (range shrK) --> \ -\ (Key K \\ analz (insert RB (Key`KK Un H))) = \ -\ (K \\ KK | Key K \\ analz (insert RB H))"; -by (etac responses.induct 1); -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); -qed "resp_analz_image_freshK_lemma"; - -(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) -Goal "evs \\ recur ==> \ -\ \\K KK. KK \\ - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un (spies evs))) = \ -\ (K \\ KK | Key K \\ analz (spies evs))"; -by (etac recur.induct 1); -by analz_spies_tac; -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); -by (ALLGOALS - (asm_simp_tac - (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); -(*Fake*) -by (spy_analz_tac 1); -val raw_analz_image_freshK = result(); -qed_spec_mp "analz_image_freshK"; - - -(*Instance of the lemma with H replaced by (spies evs): - [| RB \\ responses evs; evs \\ recur; |] - ==> KK \\ - (range shrK) --> - Key K \\ analz (insert RB (Key`KK Un spies evs)) = - (K \\ KK | Key K \\ analz (insert RB (spies evs))) -*) -bind_thm ("resp_analz_image_freshK", - raw_analz_image_freshK RSN - (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); - -Goal "[| 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); -qed "analz_insert_freshK"; - - -(*Everything that's hashed is already in past traffic. *) -Goal "[| Hash {|Key(shrK A), X|} \\ parts (spies evs); \ -\ evs \\ recur; A \\ bad |] ==> X \\ parts (spies evs)"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -(*RA3 requires a further induction*) -by (etac responses.induct 2); -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (blast_tac (claset() addIs [parts_insertI]) 1); -qed "Hash_imp_body"; - - -(** The Nonce NA uniquely identifies A's message. - This theorem applies to steps RA1 and RA2! - - Unicity is not used in other proofs but is desirable in its own right. -**) - -Goal - "[| 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 (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Blast_tac 1); -by (etac responses.induct 3); -by (Asm_full_simp_tac 4); -(*RA1,2: creation of new Nonce*) -by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1)); -qed "unique_NA"; - - -(*** Lemmas concerning the Server's response - (relations "respond" and "responses") -***) - -Goal "[| RB \\ responses evs; evs \\ recur |] \ -\ ==> (Key (shrK B) \\ analz (insert RB (spies evs))) = (B:bad)"; -by (etac responses.induct 1); -by (ALLGOALS - (asm_simp_tac - (analz_image_freshK_ss addsimps [Spy_analz_shrK, - resp_analz_image_freshK]))); -qed "shrK_in_analz_respond"; -Addsimps [shrK_in_analz_respond]; - - -Goal "[| RB \\ responses evs; \ -\ \\K KK. KK \\ - (range shrK) --> \ -\ (Key K \\ analz (Key`KK Un H)) = \ -\ (K \\ KK | Key K \\ analz H) |] \ -\ ==> (Key K \\ analz (insert RB H)) --> \ -\ (Key K \\ parts{RB} | Key K \\ analz H)"; -by (etac responses.induct 1); -by (ALLGOALS - (asm_simp_tac - (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); -(*Simplification using two distinct treatments of "image"*) -by (simp_tac (simpset() addsimps [parts_insert2]) 1); -by (blast_tac (claset() delrules [allE]) 1); -qed "resp_analz_insert_lemma"; - -bind_thm ("resp_analz_insert", - raw_analz_image_freshK RSN - (2, resp_analz_insert_lemma) RSN(2, rev_mp)); - - -(*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}"; -by (etac respond.elim 1); -by (ALLGOALS Asm_full_simp_tac); -qed "respond_certificate"; - -(*This unicity proof differs from all the others in the HOL/Auth directory. - The conclusion isn't quite unicity but duplicity, in that there are two - possibilities. Also, the presence of two different matching messages in - the inductive step complicates the case analysis. Unusually for such proofs, - the quantifiers appear to be necessary.*) -Goal "(PB,RB,KXY) \\ respond evs ==> \ -\ \\A B N. Crypt (shrK A) {|Key K, Agent B, N|} \\ parts {RB} --> \ -\ (\\A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \\ parts {RB} --> \ -\ (A'=A & B'=B) | (A'=B & B'=A))"; -by (etac respond.induct 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); -by (blast_tac (claset() addDs [respond_certificate]) 1); -qed_spec_mp "unique_lemma"; - -Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} \\ parts {RB}; \ -\ Crypt (shrK A') {|Key K, Agent B', N'|} \\ parts {RB}; \ -\ (PB,RB,KXY) \\ respond evs |] \ -\ ==> (A'=A & B'=B) | (A'=B & B'=A)"; -by (rtac unique_lemma 1); -by Auto_tac; -qed "unique_session_keys"; - - -(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 - Does not in itself guarantee security: an attack could violate - the premises, e.g. by having A=Spy **) - -Goal "[| (PB,RB,KAB) \\ respond evs; evs \\ recur |] \ -\ ==> \\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); -by (ftac respond_imp_responses 2); -by (ftac respond_imp_not_used 2); -by (ALLGOALS (*6 seconds*) - (asm_simp_tac - (analz_image_freshK_ss - addsimps split_ifs - addsimps - [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); -by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); -(** LEVEL 5 **) -by (Blast_tac 1); -by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); -by (ALLGOALS Clarify_tac); -by (blast_tac (claset() addSDs [resp_analz_insert]) 3); -by (blast_tac (claset() addSDs [respond_certificate]) 2); -by (Asm_full_simp_tac 1); -(*by unicity, either B=Aa or B=A', a contradiction if B \\ bad*) -by (blast_tac - (claset() addDs [respond_certificate RSN (2, unique_session_keys)]) 1); -qed_spec_mp "respond_Spy_not_see_session_key"; - - -Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} \\ parts (spies evs); \ -\ A \\ bad; A' \\ bad; evs \\ recur |] \ -\ ==> Key K \\ analz (spies evs)"; -by (etac rev_mp 1); -by (etac recur.induct 1); -by analz_spies_tac; -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK]))); -(*RA4*) -by (Blast_tac 5); -(*RA2*) -by (Blast_tac 3); -(*Fake*) -by (spy_analz_tac 2); -(*Base*) -by (Force_tac 1); -(*RA3 remains*) -by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); -by (safe_tac (claset() delrules [impCE])); -(*RA3, case 2: K is an old key*) -by (blast_tac (claset() addSDs [resp_analz_insert] - addDs [Key_in_parts_respond]) 2); -(*RA3, case 1: use lemma previously proved by induction*) -by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN - (2,rev_notE)]) 1); -qed "Spy_not_see_session_key"; - -(**** Authenticity properties for Agents ****) - -(*The response never contains Hashes*) -Goal "[| Hash {|Key (shrK B), M|} \\ parts (insert RB H); \ -\ (PB,RB,K) \\ respond evs |] \ -\ ==> Hash {|Key (shrK B), M|} \\ parts H"; -by (etac rev_mp 1); -by (etac (respond_imp_responses RS responses.induct) 1); -by Auto_tac; -qed "Hash_in_parts_respond"; - -(*Only RA1 or RA2 can have caused such a part of a message to appear. - This result is of no use to B, who cannot verify the Hash. Moreover, - it can say nothing about how recent A's message is. It might later be - used to prove B's presence to A at the run's conclusion.*) -Goalw [HPair_def] - "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \\ parts(spies evs); \ -\ A \\ bad; evs \\ recur |] \ -\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \\ set evs"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Blast_tac 1); -(*RA3*) -by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1); -qed_spec_mp "Hash_auth_sender"; - -(** These two results subsume (for all agents) the guarantees proved - separately for A and B in the Otway-Rees protocol. -**) - - -(*Certificates can only originate with the Server.*) -Goal "[| Crypt (shrK A) Y \\ parts (spies evs); \ -\ A \\ bad; evs \\ recur |] \ -\ ==> \\C RC. Says Server C RC \\ set evs & \ -\ Crypt (shrK A) Y \\ parts {RC}"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (Blast_tac 1); -(*RA4*) -by (Blast_tac 4); -(*RA3*) -by (full_simp_tac (simpset() addsimps [parts_insert_spies]) 3 - THEN Blast_tac 3); -(*RA1*) -by (Blast_tac 1); -(*RA2: it cannot be a new Nonce, contradiction.*) -by (Blast_tac 1); -qed "Cert_imp_Server_msg"; diff -r e502756bcb11 -r a47a9288f3f6 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Mon Apr 23 17:11:19 2001 +0200 +++ b/src/HOL/Auth/Recur.thy Tue Apr 24 12:19:01 2001 +0200 @@ -6,10 +6,10 @@ Inductive relation "recur" for the Recursive Authentication protocol. *) -Recur = Shared + +theory Recur = Shared: (*End marker for message bundles*) -syntax END :: msg +syntax END :: "msg" translations "END" == "Number 0" (*Two session keys are distributed to each agent except for the initiator, @@ -18,89 +18,488 @@ *) consts respond :: "event list => (msg*msg*key)set" inductive "respond evs" (*Server's response to the nested message*) - intrs - One "Key KAB \\ used evs - ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, + intros + 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" + 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}; + 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|} |] - ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, - {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, + ==> (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|}, RA|}, KBC) - \\ respond evs" + \ respond evs" (*Induction over "respond" can be difficult due to the complexity of the subgoals. Set "responses" captures the general form of certificates. *) -consts responses :: event list => msg set -inductive "responses evs" - intrs +consts responses :: "event list => msg set" +inductive "responses evs" + intros (*Server terminates lists*) - Nil "END \\ responses evs" + Nil: "END \ responses evs" - Cons "[| RA \\ responses evs; Key KAB \\ used evs |] + Cons: "[| RA \ responses evs; Key KAB \ used evs |] ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, - RA|} \\ responses evs" + RA|} \ responses evs" -consts recur :: event list set +consts recur :: "event list set" inductive "recur" - intrs + intros (*Initial trace is empty*) - Nil "[] \\ recur" + Nil: "[] \ recur" (*The spy MAY say anything he CAN say. Common to all similar protocols.*) - Fake "[| evs: recur; X: synth (analz (spies evs)) |] - ==> Says Spy B X # evs \\ recur" + Fake: "[| evsf \ recur; X \ synth (analz (knows Spy evsf)) |] + ==> Says Spy B X # evsf \ recur" (*Alice initiates a protocol run. END is a placeholder to terminate the nesting.*) - RA1 "[| evs1: recur; Nonce NA \\ used evs1 |] + RA1: "[| evs1: recur; Nonce NA \ used evs1 |] ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}) - # evs1 \\ recur" + # 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; Nonce NB \\ used evs2; - Says A' B PA \\ set 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" + # evs2 \ recur" (*The Server receives Bob's message and prepares a response.*) - RA3 "[| evs3: recur; Says B' Server PB \\ set evs3; - (PB,RB,K) \\ respond evs3 |] - ==> Says Server B RB # evs3 \\ recur" + 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; - 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|}, - Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, - RA|} \\ set evs4 |] - ==> Says B A RA # evs4 \\ recur" - -end + 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|}, + Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, + RA|} \ set evs4 |] + ==> Says B A RA # evs4 \ recur" (*No "oops" message can easily be expressed. Each session key is - associated--in two separate messages--with two nonces. This is + associated--in two separate messages--with two nonces. This is one try, but it isn't that useful. Re domino attack, note that Recur.ML proves that each session key is secure provided the two peers are, even if there are compromised agents elsewhere in the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, etc. - Oops "[| evso: recur; Says Server B RB \\ set evso; - RB \\ responses evs'; Key K \\ parts {RB} |] - ==> Notes Spy {|Key K, RB|} # evso \\ recur" + Oops: "[| evso: recur; Says Server B RB \ set evso; + RB \ responses evs'; Key K \ parts {RB} |] + ==> Notes Spy {|Key K, RB|} # evso \ recur" *) + + +declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] + + +(** Possibility properties: traces that reach the end + ONE theorem would be more elegant and faster! + By induction on a list of agents (no repetitions) +**) + + +(*Simplest case: Alice goes directly to the server*) +lemma "\K NA. \evs \ recur. + Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, + END|} \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] recur.Nil [THEN recur.RA1, + THEN recur.RA3 [OF _ _ respond.One]]) +apply possibility +done + + +(*Case two: Alice, Bob and the server +WHY WON'T INSERT LET VARS REMAIN??? +lemma "\K. \NA. \evs \ recur. + Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, + END|} \ set evs" +apply (insert Nonce_supply2 Key_supply2) +apply clarify +apply (intro exI bexI) +apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2, + THEN recur.RA3 [OF _ _ respond.One]]) +apply possibility +apply (DEPTH_SOLVE (erule asm_rl less_not_refl2 less_not_refl3)) +done +*) + +(*Case three: Alice, Bob, Charlie and the server + TOO SLOW to run every time! +Goal "\K. \NA. \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 + (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); +by basic_possibility_tac; +by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 + ORELSE + eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); +result(); +****) + +(**** Inductive proofs about recur ****) + +lemma respond_imp_not_used: "(PA,RB,KAB) \ respond evs ==> Key KAB \ used evs" +by (erule respond.induct, simp_all) + +lemma Key_in_parts_respond [rule_format]: + "[| Key K \ parts {RB}; (PB,RB,K') \ respond evs |] ==> Key K \ used evs" +apply (erule rev_mp, erule respond.induct) +apply (auto dest: Key_not_used respond_imp_not_used) +done + +(*Simple inductive reasoning about responses*) +lemma respond_imp_responses: + "(PA,RB,KAB) \ respond evs ==> RB \ responses evs" +apply (erule respond.induct) +apply (blast intro!: respond_imp_not_used responses.intros)+ +done + + +(** For reasoning about the encrypted portion of messages **) + +lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj] + +lemma RA4_analz_spies: + "Says C' B {|Crypt K X, X', RA|} \ set evs ==> RA \ analz (spies evs)" +by blast + + +(*RA2_analz... and RA4_analz... let us treat those cases using the same + argument as for the Fake case. This is possible for most, but not all, + proofs: Fake does not invent new nonces (as in RA2), and of course Fake + messages originate from the Spy. *) + +lemmas RA2_parts_spies = RA2_analz_spies [THEN analz_into_parts] +lemmas RA4_parts_spies = RA4_analz_spies [THEN analz_into_parts] + + +(** Theorems of the form X \ parts (spies evs) imply that NOBODY + sends messages containing X! **) + +(** Spy never sees another agent's shared key! (unless it's bad at start) **) + +lemma Spy_see_shrK [simp]: + "evs \ recur ==> (Key (shrK A) \ parts (spies evs)) = (A \ bad)" +apply (erule recur.induct) +apply auto +(*RA3. It's ugly to call auto twice, but it seems necessary.*) +apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies) +done + +lemma Spy_analz_shrK [simp]: + "evs \ recur ==> (Key (shrK A) \ analz (spies evs)) = (A \ bad)" +by auto + +lemma Spy_see_shrK_D [dest!]: + "[|Key (shrK A) \ parts (knows Spy evs); evs \ recur|] ==> A \ bad" +by (blast dest: Spy_see_shrK) + + +(*** Proofs involving analz ***) + +(** Session keys are not used to encrypt other session keys **) + +(*Version for "responses" relation. Handles case RA3 in the theorem below. + Note that it holds for *any* set H (not just "spies evs") + satisfying the inductive hypothesis.*) +lemma resp_analz_image_freshK_lemma: + "[| RB \ responses evs; + \K KK. KK \ - (range shrK) --> + (Key K \ analz (Key`KK Un H)) = + (K \ KK | Key K \ analz H) |] + ==> \K KK. KK \ - (range shrK) --> + (Key K \ analz (insert RB (Key`KK Un H))) = + (K \ KK | Key K \ analz (insert RB H))" +by (erule responses.induct, + simp_all del: image_insert + add: analz_image_freshK_simps) + + +(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) +lemma raw_analz_image_freshK: + "evs \ recur ==> + \K KK. KK \ - (range shrK) --> + (Key K \ analz (Key`KK Un (spies evs))) = + (K \ KK | Key K \ analz (spies evs))" +apply (erule recur.induct) +apply (drule_tac [4] RA2_analz_spies, + frule_tac [5] respond_imp_responses, + drule_tac [6] RA4_analz_spies) +apply analz_freshK +apply spy_analz +(*RA3*) +apply (simp_all add: resp_analz_image_freshK_lemma) +done + + +(*Instance of the lemma with H replaced by (spies evs): + [| RB \ responses evs; evs \ recur; |] + ==> KK \ - (range shrK) --> + Key K \ analz (insert RB (Key`KK Un spies evs)) = + (K \ KK | Key K \ analz (insert RB (spies evs))) +*) +lemmas resp_analz_image_freshK = + resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK] + +lemma analz_insert_freshK: + "[| evs \ recur; KAB \ range shrK |] + ==> Key K \ analz (insert (Key KAB) (spies evs)) = + (K = KAB | Key K \ analz (spies evs))" +by (simp del: image_insert + add: analz_image_freshK_simps raw_analz_image_freshK) + + +(*Everything that's hashed is already in past traffic. *) +lemma Hash_imp_body: "[| Hash {|Key(shrK A), X|} \ parts (spies evs); + evs \ recur; A \ bad |] ==> X \ parts (spies evs)" +apply (erule rev_mp) +apply (erule recur.induct, + frule_tac [6] RA4_parts_spies, + frule_tac [5] respond_imp_responses, + frule_tac [4] RA2_parts_spies) +(*RA3 requires a further induction*) +apply (erule_tac [5] responses.induct) +apply simp_all +(*Nil*) +apply force +(*Fake*) +apply (blast intro: parts_insertI) +done + + +(** The Nonce NA uniquely identifies A's message. + This theorem applies to steps RA1 and RA2! + + Unicity is not used in other proofs but is desirable in its own right. +**) + +lemma unique_NA: + "[| 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'" +apply (erule rev_mp, erule rev_mp) +apply (erule recur.induct, + frule_tac [5] respond_imp_responses) +apply (force, simp_all) +(*Fake*) +apply blast +apply (erule_tac [3] responses.induct) +(*RA1,2: creation of new Nonce*) +apply simp_all +apply (blast dest!: Hash_imp_body)+ +done + + +(*** Lemmas concerning the Server's response + (relations "respond" and "responses") +***) + +lemma shrK_in_analz_respond [simp]: + "[| RB \ responses evs; evs \ recur |] + ==> (Key (shrK B) \ analz (insert RB (spies evs))) = (B:bad)" +by (erule responses.induct, + simp_all del: image_insert + add: analz_image_freshK_simps resp_analz_image_freshK) + + +lemma resp_analz_insert_lemma: + "[| Key K \ analz (insert RB H); + \K KK. KK \ - (range shrK) --> + (Key K \ analz (Key`KK Un H)) = + (K \ KK | Key K \ analz H); + RB \ responses evs |] + ==> (Key K \ parts{RB} | Key K \ analz H)" +apply (erule rev_mp, erule responses.induct) +apply (simp_all del: image_insert + add: analz_image_freshK_simps resp_analz_image_freshK_lemma) +(*Simplification using two distinct treatments of "image"*) +apply (simp add: parts_insert2) +apply blast +done + +lemmas resp_analz_insert = + resp_analz_insert_lemma [OF _ raw_analz_image_freshK] + +(*The last key returned by respond indeed appears in a certificate*) +lemma respond_certificate: + "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \ respond evs + ==> Crypt (shrK A) {|Key K, B, NA|} \ parts {RA}" +apply (ind_cases "(X, RA, K) \ respond evs") +apply simp_all +done + +(*This unicity proof differs from all the others in the HOL/Auth directory. + The conclusion isn't quite unicity but duplicity, in that there are two + possibilities. Also, the presence of two different matching messages in + the inductive step complicates the case analysis. Unusually for such proofs, + the quantifiers appear to be necessary.*) +lemma unique_lemma [rule_format]: + "(PB,RB,KXY) \ respond evs ==> + \A B N. Crypt (shrK A) {|Key K, Agent B, N|} \ parts {RB} --> + (\A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \ parts {RB} --> + (A'=A & B'=B) | (A'=B & B'=A))" +apply (erule respond.induct) +apply (simp_all add: all_conj_distrib) +apply (blast dest: respond_certificate) +done + +lemma unique_session_keys: + "[| Crypt (shrK A) {|Key K, Agent B, N|} \ parts {RB}; + Crypt (shrK A') {|Key K, Agent B', N'|} \ parts {RB}; + (PB,RB,KXY) \ respond evs |] + ==> (A'=A & B'=B) | (A'=B & B'=A)" +by (rule unique_lemma, auto) + + +(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 + Does not in itself guarantee security: an attack could violate + the premises, e.g. by having A=Spy **) + +lemma respond_Spy_not_see_session_key [rule_format]: + "[| (PB,RB,KAB) \ respond evs; evs \ recur |] + ==> \A A' N. A \ bad & A' \ bad --> + Crypt (shrK A) {|Key K, Agent A', N|} \ parts{RB} --> + Key K \ analz (insert RB (spies evs))" +apply (erule respond.induct) +apply (frule_tac [2] respond_imp_responses) +apply (frule_tac [2] respond_imp_not_used) +apply (simp_all del: image_insert + add: analz_image_freshK_simps split_ifs shrK_in_analz_respond + resp_analz_image_freshK parts_insert2) +apply (simp_all add: ex_disj_distrib) +(** LEVEL 5 **) +(*Base case of respond*) +apply blast +(*Inductive step of respond*) +apply (intro allI conjI impI) +apply simp_all +(*by unicity, either B=Aa or B=A', a contradiction if B \ bad*) +apply (blast dest: unique_session_keys [OF _ respond_certificate]) +apply (blast dest!: respond_certificate) +apply (blast dest!: resp_analz_insert) +done + + +(*WHAT'S GOING ON??*) +method_setup newbla = {* + Method.no_args (Method.METHOD (fn facts => Blast_tac 1)) *} + "for debugging spy_analz" + +lemma Spy_not_see_session_key: + "[| Crypt (shrK A) {|Key K, Agent A', N|} \ parts (spies evs); + A \ bad; A' \ bad; evs \ recur |] + ==> Key K \ analz (spies evs)" +apply (erule rev_mp) +apply (erule recur.induct) +apply (drule_tac [4] RA2_analz_spies, + frule_tac [5] respond_imp_responses, + drule_tac [6] RA4_analz_spies, + simp_all add: split_ifs analz_insert_eq analz_insert_freshK) +(*Base*) +apply force +(*Fake*) +apply (intro allI impI notI conjI iffI) +apply Fake_insert_simp +apply (blast ); +(*???ASK MARKUS WHY METHOD_SETUP DOESN'T WORK. Should be just +apply spy_analz +*) +(*RA2*) +apply blast +(*RA3 remains*) +apply (simp add: parts_insert_spies) +(*Now we split into two cases. A single blast could do it, but it would take + a CPU minute.*) +apply (safe del: impCE) +(*RA3, case 1: use lemma previously proved by induction*) +apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key]) +(*RA3, case 2: K is an old key*) +apply (blast dest: resp_analz_insert dest: Key_in_parts_respond) +(*RA4*) +apply blast +done + +(**** Authenticity properties for Agents ****) + +(*The response never contains Hashes*) +lemma Hash_in_parts_respond: + "[| Hash {|Key (shrK B), M|} \ parts (insert RB H); + (PB,RB,K) \ respond evs |] + ==> Hash {|Key (shrK B), M|} \ parts H" +apply (erule rev_mp) +apply (erule respond_imp_responses [THEN responses.induct]) +apply auto +done + +(*Only RA1 or RA2 can have caused such a part of a message to appear. + This result is of no use to B, who cannot verify the Hash. Moreover, + it can say nothing about how recent A's message is. It might later be + used to prove B's presence to A at the run's conclusion.*) +lemma Hash_auth_sender [rule_format]: + "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \ parts(spies evs); + A \ bad; evs \ recur |] + ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \ set evs" +apply (unfold HPair_def) +apply (erule rev_mp) +apply (erule recur.induct, + frule_tac [6] RA4_parts_spies, + frule_tac [4] RA2_parts_spies, + simp_all) +(*Nil*) +apply force +(*Fake, RA3*) +apply (blast dest: Hash_in_parts_respond)+; +done + +(** These two results subsume (for all agents) the guarantees proved + separately for A and B in the Otway-Rees protocol. +**) + + +(*Certificates can only originate with the Server.*) +lemma Cert_imp_Server_msg: + "[| Crypt (shrK A) Y \ parts (spies evs); + A \ bad; evs \ recur |] + ==> \C RC. Says Server C RC \ set evs & + Crypt (shrK A) Y \ parts {RC}" +apply (erule rev_mp, erule recur.induct, simp_all) +(*Nil*) +apply force +(*Fake*) +apply blast +(*RA1*) +apply blast +(*RA2: it cannot be a new Nonce, contradiction.*) +apply blast +(*RA3*) +apply (simp add: parts_insert_spies, blast) +(*RA4*) +apply blast +done + +end diff -r e502756bcb11 -r a47a9288f3f6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Apr 23 17:11:19 2001 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 24 12:19:01 2001 +0200 @@ -306,7 +306,7 @@ Auth/NS_Public_Bad.thy \ Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \ Auth/OtwayRees_Bad.thy Auth/Public_lemmas.ML Auth/Public.thy Auth/ROOT.ML \ - Auth/Recur.ML Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \ + Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \ Auth/TLS.ML Auth/TLS.thy Auth/WooLam.thy \ Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \ Auth/KerberosIV.ML Auth/KerberosIV.thy \