# HG changeset patch # User paulson # Date 1064324493 -7200 # Node ID d8598e24f8fa793943f3945198fcff96f8f0cf50 # Parent d3b8d972a4881745f747b805b37ef81cf8c14798 Removal of the Key_supply axiom (affects many possbility proofs) and minor changes diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/CertifiedEmail.thy --- a/src/HOL/Auth/CertifiedEmail.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/CertifiedEmail.thy Tue Sep 23 15:41:33 2003 +0200 @@ -93,14 +93,15 @@ declare analz_into_parts [dest] (*A "possibility property": there are traces that reach the end*) -lemma "\S2TTP. \evs \ certified_mail. +lemma "[| Key K \ used []; K \ symKeys |] ==> + \S2TTP. \evs \ certified_mail. Says TTP S (Crypt (priSK TTP) S2TTP) \ set evs" -apply (rule bexE [OF Key_supply1]) apply (intro exI bexI) apply (rule_tac [2] certified_mail.Nil [THEN certified_mail.CM1, THEN certified_mail.Reception, THEN certified_mail.CM2, - THEN certified_mail.CM3], possibility, possibility, auto) + THEN certified_mail.CM3]) +apply (possibility, auto) done diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Event.thy Tue Sep 23 15:41:33 2003 +0200 @@ -35,13 +35,10 @@ text{*Spy has access to his own key for spoof messages, but Server is secure*} specification (bad) - bad_properties: "Spy \ bad & Server \ bad" + Spy_in_bad [iff]: "Spy \ bad" + Server_not_bad [iff]: "Server \ bad" by (rule exI [of _ "{Spy}"], simp) -lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff] -lemmas Server_not_bad = bad_properties [THEN conjunct2, iff] - - primrec knows_Nil: "knows A [] = initState A" knows_Cons: @@ -111,8 +108,8 @@ "knows Spy (Says A B X # evs) = insert X (knows Spy evs)" by simp -text{*The point of letting the Spy see "bad" agents' notes is to prevent - redundant case-splits on whether A=Spy and whether A:bad*} +text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits + on whether @{term "A=Spy"} and whether @{term "A\bad"}*} lemma knows_Spy_Notes [simp]: "knows Spy (Notes A X # evs) = (if A:bad then insert X (knows Spy evs) else knows Spy evs)" diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Tue Sep 23 15:41:33 2003 +0200 @@ -242,9 +242,10 @@ (*---------------------------------------------------------------------*) -declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest] -declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare Says_imp_knows_Spy [THEN parts.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] subsection{*Lemmas about Lists*} @@ -294,31 +295,27 @@ ev \ Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk, (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|})) ==> AuthKeys (ev # evs) = AuthKeys evs" -apply (unfold AuthKeys_def, auto) -done +by (unfold AuthKeys_def, auto) lemma AuthKeys_insert: "AuthKeys (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk, (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs) = insert K (AuthKeys evs)" -apply (unfold AuthKeys_def, auto) -done +by (unfold AuthKeys_def, auto) lemma AuthKeys_simp: "K \ AuthKeys (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk, (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs) ==> K = K' | K \ AuthKeys evs" -apply (unfold AuthKeys_def, auto) -done +by (unfold AuthKeys_def, auto) lemma AuthKeysI: "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk, (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \ set evs ==> K \ AuthKeys evs" -apply (unfold AuthKeys_def, auto) -done +by (unfold AuthKeys_def, auto) lemma AuthKeys_used: "K \ AuthKeys evs ==> Key K \ used evs" by (simp add: AuthKeys_def, blast) @@ -344,8 +341,7 @@ lemma K5_msg_in_parts_spies: "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|}) \ set evs ==> ServTicket \ parts (spies evs)" -apply blast -done +by blast lemma Oops_range_spies2: "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) @@ -358,8 +354,7 @@ lemma Says_ticket_in_parts_spies: "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \ set evs ==> Ticket \ parts (spies evs)" -apply blast -done +by blast (*Spy never sees another agent's shared key! (unless it's lost at start)*) @@ -980,8 +975,7 @@ ~ ExpirAuth Tk evs; A \ bad; evs \ kerberos |] ==> Key AuthKey \ analz (spies evs)" -apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma) -done +by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma) subsection{* Guarantees for Tgs *} @@ -1261,8 +1255,8 @@ ~ ExpirAuth Tk evs; A \ bad; evs \ kerberos |] ==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \ set evs" -apply (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis) -done +by (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis) + text{*Note: requires a temporal check*} @@ -1422,8 +1416,7 @@ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; A \ bad; B \ bad; B \ Tgs; evs \ kerberos |] ==> B Issues A with (Crypt ServKey (Number Ta)) on evs" -apply (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma) -done +by (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma) lemma B_Knows_B_Knows_ServKey_refined: "[| Says B A (Crypt ServKey (Number Ta)) \ set evs; @@ -1432,9 +1425,7 @@ ~ ExpirServ Tt evs; A \ bad; B \ bad; B \ Tgs; evs \ kerberos |] ==> B Issues A with (Crypt ServKey (Number Ta)) on evs" -apply (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma) -done - +by (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma) lemma A_Knows_B_Knows_ServKey: "[| Crypt ServKey (Number Ta) \ parts (spies evs); @@ -1445,8 +1436,7 @@ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; A \ bad; B \ bad; B \ Tgs; evs \ kerberos |] ==> B Issues A with (Crypt ServKey (Number Ta)) on evs" -apply (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma) -done +by (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma) lemma K3_imp_K2: "[| Says A Tgs @@ -1525,8 +1515,7 @@ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; B \ Tgs; A \ bad; B \ bad; evs \ kerberos |] ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs" -apply (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma) -done +by (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma) lemma B_Knows_A_Knows_ServKey: "[| Crypt ServKey {|Agent A, Number Ta|} \ parts (spies evs); @@ -1539,8 +1528,7 @@ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; B \ Tgs; A \ bad; B \ bad; evs \ kerberos |] ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs" -apply (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma) -done +by (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma) lemma B_Knows_A_Knows_ServKey_refined: @@ -1550,7 +1538,6 @@ ~ ExpirServ Tt evs; B \ Tgs; A \ bad; B \ bad; evs \ kerberos |] ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs" -apply (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma) -done +by (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma) end diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 23 15:41:33 2003 +0200 @@ -100,20 +100,22 @@ ==> Notes Spy {|Number Ts, Key K|} # evso \ kerberos_ban" -declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest] -declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare Says_imp_knows_Spy [THEN parts.Inj, dest] +declare parts.Body [dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] (*A "possibility property": there are traces that reach the end.*) -lemma "\Timestamp K. \evs \ kerberos_ban. +lemma "Key K \ used [] + ==> \Timestamp. \evs \ kerberos_ban. Says B A (Crypt K (Number Timestamp)) \ set evs" apply (cut_tac SesKeyLife_LB) apply (intro exI bexI) apply (rule_tac [2] kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, - THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility) -apply (simp_all (no_asm_simp)) + THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4]) +apply (possibility, simp_all (no_asm_simp) add: used_Cons) done diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Message.thy Tue Sep 23 15:41:33 2003 +0200 @@ -39,13 +39,13 @@ agent = Server | Friend nat | Spy datatype - msg = Agent agent (*Agent names*) - | Number nat (*Ordinary integers, timestamps, ...*) - | Nonce nat (*Unguessable nonces*) - | Key key (*Crypto keys*) - | Hash msg (*Hashing*) - | MPair msg msg (*Compound messages*) - | Crypt key msg (*Encryption, public- or shared-key*) + msg = Agent agent --{*Agent names*} + | Number nat --{*Ordinary integers, timestamps, ...*} + | Nonce nat --{*Unguessable nonces*} + | Key key --{*Crypto keys*} + | Hash msg --{*Hashing*} + | MPair msg msg --{*Compound messages*} + | Crypt key msg --{*Encryption, public- or shared-key*} (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) @@ -69,7 +69,7 @@ keysFor :: "msg set => key set" "keysFor H == invKey ` {K. \X. Crypt K X \ H}" -(** Inductive definition of all "parts" of a message. **) +subsubsection{*Inductive definition of all "parts" of a message. *} consts parts :: "msg set => msg set" inductive "parts H" @@ -81,7 +81,7 @@ (*Monotonicity*) -lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" +lemma parts_mono: "G\H ==> parts(G) \ parts(H)" apply auto apply (erule parts.induct) apply (auto dest: Fst Snd Body) @@ -99,7 +99,7 @@ by auto -(** Inverse of keys **) +subsubsection{*Inverse of keys *} lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" apply safe @@ -142,8 +142,7 @@ lemma keysFor_insert_Crypt [simp]: "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" -apply (unfold keysFor_def, auto) -done +by (unfold keysFor_def, auto) lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}" by (unfold keysFor_def, auto) @@ -183,7 +182,7 @@ by (erule parts.induct, blast+) -(** Unions **) +subsubsection{*Unions *} lemma parts_Un_subset1: "parts(G) \ parts(H) \ parts(G \ H)" by (intro Un_least parts_mono Un_upper1 Un_upper2) @@ -203,7 +202,8 @@ (*TWO inserts to avoid looping. This rewrite is better than nothing. Not suitable for Addsimps: its behaviour can be strange.*) -lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \ parts {Y} \ parts H" +lemma parts_insert2: + "parts (insert X (insert Y H)) = parts {X} \ parts {Y} \ parts H" apply (simp add: Un_assoc) apply (simp add: parts_insert [symmetric]) done @@ -231,7 +231,7 @@ lemma parts_insert_subset: "insert X (parts H) \ parts(insert X H)" by (blast intro: parts_mono [THEN [2] rev_subsetD]) -(** Idempotence and transitivity **) +subsubsection{*Idempotence and transitivity *} lemma parts_partsD [dest!]: "X\ parts (parts H) ==> X\ parts H" by (erule parts.induct, blast+) @@ -243,46 +243,51 @@ by (drule parts_mono, blast) (*Cut*) -lemma parts_cut: "[| Y\ parts (insert X G); X\ parts H |] - ==> Y\ parts (G \ H)" -apply (erule parts_trans, auto) -done +lemma parts_cut: + "[| Y\ parts (insert X G); X\ parts H |] ==> Y\ parts (G \ H)" +by (erule parts_trans, auto) lemma parts_cut_eq [simp]: "X\ parts H ==> parts (insert X H) = parts H" by (force dest!: parts_cut intro: parts_insertI) -(** Rewrite rules for pulling out atomic messages **) +subsubsection{*Rewrite rules for pulling out atomic messages *} lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] -lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" +lemma parts_insert_Agent [simp]: + "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" apply (rule parts_insert_eq_I) apply (erule parts.induct, auto) done -lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" +lemma parts_insert_Nonce [simp]: + "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" apply (rule parts_insert_eq_I) apply (erule parts.induct, auto) done -lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)" +lemma parts_insert_Number [simp]: + "parts (insert (Number N) H) = insert (Number N) (parts H)" apply (rule parts_insert_eq_I) apply (erule parts.induct, auto) done -lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)" +lemma parts_insert_Key [simp]: + "parts (insert (Key K) H) = insert (Key K) (parts H)" apply (rule parts_insert_eq_I) apply (erule parts.induct, auto) done -lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)" +lemma parts_insert_Hash [simp]: + "parts (insert (Hash X) H) = insert (Hash X) (parts H)" apply (rule parts_insert_eq_I) apply (erule parts.induct, auto) done -lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) = +lemma parts_insert_Crypt [simp]: + "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" apply (rule equalityI) apply (rule subsetI) @@ -291,7 +296,8 @@ apply (blast intro: parts.Body)+ done -lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) = +lemma parts_insert_MPair [simp]: + "parts (insert {|X,Y|} H) = insert {|X,Y|} (parts (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -320,9 +326,9 @@ subsection{*Inductive relation "analz"*} -(** Inductive definition of "analz" -- what can be broken down from a set of +text{*Inductive definition of "analz" -- what can be broken down from a set of messages, including keys. A form of downward closure. Pairs can - be taken apart; messages decrypted with known keys. **) + be taken apart; messages decrypted with known keys. *} consts analz :: "msg set => msg set" inductive "analz H" @@ -335,7 +341,7 @@ (*Monotonicity; Lemma 1 of Lowe's paper*) -lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" +lemma analz_mono: "G\H ==> analz(G) \ analz(H)" apply auto apply (erule analz.induct) apply (auto dest: Fst Snd) @@ -356,6 +362,8 @@ apply (erule analz.induct, blast+) done +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] + lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard] @@ -372,7 +380,7 @@ lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard] -(** General equational properties **) +subsubsection{*General equational properties *} lemma analz_empty [simp]: "analz{} = {}" apply safe @@ -387,26 +395,30 @@ lemma analz_insert: "insert X (analz H) \ analz(insert X H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) -(** Rewrite rules for pulling out atomic messages **) +subsubsection{*Rewrite rules for pulling out atomic messages *} lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] -lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" +lemma analz_insert_Agent [simp]: + "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" apply (rule analz_insert_eq_I) apply (erule analz.induct, auto) done -lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" +lemma analz_insert_Nonce [simp]: + "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" apply (rule analz_insert_eq_I) apply (erule analz.induct, auto) done -lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)" +lemma analz_insert_Number [simp]: + "analz (insert (Number N) H) = insert (Number N) (analz H)" apply (rule analz_insert_eq_I) apply (erule analz.induct, auto) done -lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)" +lemma analz_insert_Hash [simp]: + "analz (insert (Hash X) H) = insert (Hash X) (analz H)" apply (rule analz_insert_eq_I) apply (erule analz.induct, auto) done @@ -420,7 +432,8 @@ apply (erule analz.induct, auto) done -lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) = +lemma analz_insert_MPair [simp]: + "analz (insert {|X,Y|} H) = insert {|X,Y|} (analz (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -453,7 +466,8 @@ apply (blast intro: analz_insertI analz.Decrypt) done -lemma analz_insert_Decrypt: "Key (invKey K) \ analz H ==> +lemma analz_insert_Decrypt: + "Key (invKey K) \ analz H ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H))" by (intro equalityI lemma1 lemma2) @@ -471,7 +485,8 @@ (*This rule supposes "for the sake of argument" that we have the key.*) -lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \ +lemma analz_insert_Crypt_subset: + "analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) apply (erule analz.induct, auto) @@ -484,7 +499,7 @@ done -(** Idempotence and transitivity **) +subsubsection{*Idempotence and transitivity *} lemma analz_analzD [dest!]: "X\ analz (analz H) ==> X\ analz H" by (erule analz.induct, blast+) @@ -510,32 +525,35 @@ by (blast intro: analz_cut analz_insertI) -(** A congruence rule for "analz" **) +text{*A congruence rule for "analz" *} -lemma analz_subset_cong: "[| analz G \ analz G'; analz H \ analz H' +lemma analz_subset_cong: + "[| analz G \ analz G'; analz H \ analz H' |] ==> analz (G \ H) \ analz (G' \ H')" apply clarify apply (erule analz.induct) apply (best intro: analz_mono [THEN subsetD])+ done -lemma analz_cong: "[| analz G = analz G'; analz H = analz H' +lemma analz_cong: + "[| analz G = analz G'; analz H = analz H' |] ==> analz (G \ H) = analz (G' \ H')" -apply (intro equalityI analz_subset_cong, simp_all) -done +by (intro equalityI analz_subset_cong, simp_all) - -lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')" +lemma analz_insert_cong: + "analz H = analz H' ==> analz(insert X H) = analz(insert X H')" by (force simp only: insert_def intro!: analz_cong) (*If there are no pairs or encryptions then analz does nothing*) -lemma analz_trivial: "[| \X Y. {|X,Y|} \ H; \X K. Crypt K X \ H |] ==> analz H = H" +lemma analz_trivial: + "[| \X Y. {|X,Y|} \ H; \X K. Crypt K X \ H |] ==> analz H = H" apply safe apply (erule analz.induct, blast+) done (*These two are obsolete (with a single Spy) but cost little to prove...*) -lemma analz_UN_analz_lemma: "X\ analz (\i\A. analz (H i)) ==> X\ analz (\i\A. H i)" +lemma analz_UN_analz_lemma: + "X\ analz (\i\A. analz (H i)) ==> X\ analz (\i\A. H i)" apply (erule analz.induct) apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ done @@ -546,10 +564,10 @@ subsection{*Inductive relation "synth"*} -(** Inductive definition of "synth" -- what can be built up from a set of +text{*Inductive definition of "synth" -- what can be built up from a set of messages. A form of upward closure. Pairs can be built, messages encrypted with known keys. Agent names are public domain. - Numbers can be guessed, but Nonces cannot be. **) + Numbers can be guessed, but Nonces cannot be. *} consts synth :: "msg set => msg set" inductive "synth H" @@ -562,7 +580,7 @@ Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" (*Monotonicity*) -lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" +lemma synth_mono: "G\H ==> synth(G) \ synth(H)" apply auto apply (erule synth.induct) apply (auto dest: Fst Snd Body) @@ -579,7 +597,7 @@ lemma synth_increasing: "H \ synth(H)" by blast -(** Unions **) +subsubsection{*Unions *} (*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*) @@ -589,7 +607,7 @@ lemma synth_insert: "insert X (synth H) \ synth(insert X H)" by (blast intro: synth_mono [THEN [2] rev_subsetD]) -(** Idempotence and transitivity **) +subsubsection{*Idempotence and transitivity *} lemma synth_synthD [dest!]: "X\ synth (synth H) ==> X\ synth H" by (erule synth.induct, blast+) @@ -616,17 +634,17 @@ lemma Key_synth_eq [simp]: "(Key K \ synth H) = (Key K \ H)" by blast -lemma Crypt_synth_eq [simp]: "Key K \ H ==> (Crypt K X \ synth H) = (Crypt K X \ H)" +lemma Crypt_synth_eq [simp]: + "Key K \ H ==> (Crypt K X \ synth H) = (Crypt K X \ H)" by blast lemma keysFor_synth [simp]: "keysFor (synth H) = keysFor H \ invKey`{K. Key K \ H}" -apply (unfold keysFor_def, blast) -done +by (unfold keysFor_def, blast) -(*** Combinations of parts, analz and synth ***) +subsubsection{*Combinations of parts, analz and synth *} lemma parts_synth [simp]: "parts (synth H) = parts H \ synth H" apply (rule equalityI) @@ -655,22 +673,29 @@ done -(** For reasoning about the Fake rule in traces **) +subsubsection{*For reasoning about the Fake rule in traces *} lemma parts_insert_subset_Un: "X\ G ==> parts(insert X H) \ parts G \ parts H" by (rule subset_trans [OF parts_mono parts_Un_subset2], blast) (*More specifically for Fake. Very occasionally we could do with a version of the form parts{X} \ synth (analz H) \ parts H *) -lemma Fake_parts_insert: "X \ synth (analz H) ==> +lemma Fake_parts_insert: + "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" apply (drule parts_insert_subset_Un) apply (simp (no_asm_use)) apply blast done +lemma Fake_parts_insert_in_Un: + "[|Z \ parts (insert X H); X: synth (analz H)|] + ==> Z \ synth (analz H) \ parts H"; +by (blast dest: Fake_parts_insert [THEN subsetD, dest]) + (*H is sometimes (Key ` KK \ spies evs), so can't put G=H*) -lemma Fake_analz_insert: "X\ synth (analz G) ==> +lemma Fake_analz_insert: + "X\ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" apply (rule subsetI) apply (subgoal_tac "x \ analz (synth (analz G) \ H) ") @@ -679,10 +704,12 @@ apply blast done -lemma analz_conj_parts [simp]: "(X \ analz H & X \ parts H) = (X \ analz H)" +lemma analz_conj_parts [simp]: + "(X \ analz H & X \ parts H) = (X \ analz H)" by (blast intro: analz_subset_parts [THEN subsetD]) -lemma analz_disj_parts [simp]: "(X \ analz H | X \ parts H) = (X \ parts H)" +lemma analz_disj_parts [simp]: + "(X \ analz H | X \ parts H) = (X \ parts H)" by (blast intro: analz_subset_parts [THEN subsetD]) (*Without this equation, other rules for synth and analz would yield @@ -692,19 +719,21 @@ (X \ synth (analz H) & Y \ synth (analz H))" by blast -lemma Crypt_synth_analz: "[| Key K \ analz H; Key (invKey K) \ analz H |] +lemma Crypt_synth_analz: + "[| Key K \ analz H; Key (invKey K) \ analz H |] ==> (Crypt K X \ synth (analz H)) = (X \ synth (analz H))" by blast -lemma Hash_synth_analz [simp]: "X \ synth (analz H) +lemma Hash_synth_analz [simp]: + "X \ synth (analz H) ==> (Hash{|X,Y|} \ synth (analz H)) = (Hash{|X,Y|} \ analz H)" by blast subsection{*HPair: a combination of Hash and MPair*} -(*** Freeness ***) +subsubsection{*Freeness *} lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y" by (unfold HPair_def, simp) @@ -733,14 +762,16 @@ lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)" by (simp add: HPair_def) -lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)" +lemma MPair_eq_HPair [iff]: + "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)" by (simp add: HPair_def) -lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)" +lemma HPair_eq_MPair [iff]: + "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)" by (auto simp add: HPair_def) -(*** Specialized laws, proved in terms of those for Hash and MPair ***) +subsubsection{*Specialized laws, proved in terms of those for Hash and MPair *} lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H" by (simp add: HPair_def) @@ -766,37 +797,10 @@ declare parts.Body [rule del] +text{*Rewrites to push in Key and Crypt messages, so that other messages can + be pulled out using the @{text analz_insert} rules*} ML {* -(*ML bindings for definitions*) - -val invKey = thm "invKey" -val keysFor_def = thm "keysFor_def" -val HPair_def = thm "HPair_def" -val symKeys_def = thm "symKeys_def" - -structure parts = - struct - val induct = thm "parts.induct" - val Inj = thm "parts.Inj" - val Fst = thm "parts.Fst" - val Snd = thm "parts.Snd" - val Body = thm "parts.Body" - end - -structure analz = - struct - val induct = thm "analz.induct" - val Inj = thm "analz.Inj" - val Fst = thm "analz.Fst" - val Snd = thm "analz.Snd" - val Decrypt = thm "analz.Decrypt" - end - - -(** Rewrites to push in Key and Crypt messages, so that other messages can - be pulled out using the analz_insert rules **) - fun insComm x y = inst "x" x (inst "y" y insert_commute); bind_thms ("pushKeys", @@ -818,79 +822,19 @@ subsection{*Tactics useful for many protocol proofs*} ML {* +val invKey = thm "invKey" +val keysFor_def = thm "keysFor_def" +val HPair_def = thm "HPair_def" +val symKeys_def = thm "symKeys_def" val parts_mono = thm "parts_mono"; val analz_mono = thm "analz_mono"; -val Key_image_eq = thm "Key_image_eq"; -val Nonce_Key_image_eq = thm "Nonce_Key_image_eq"; -val keysFor_Un = thm "keysFor_Un"; -val keysFor_mono = thm "keysFor_mono"; -val keysFor_image_Key = thm "keysFor_image_Key"; -val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor"; -val MPair_parts = thm "MPair_parts"; -val parts_increasing = thm "parts_increasing"; -val parts_insertI = thm "parts_insertI"; -val parts_empty = thm "parts_empty"; -val parts_emptyE = thm "parts_emptyE"; -val parts_singleton = thm "parts_singleton"; -val parts_Un_subset1 = thm "parts_Un_subset1"; -val parts_Un_subset2 = thm "parts_Un_subset2"; -val parts_insert = thm "parts_insert"; -val parts_insert2 = thm "parts_insert2"; -val parts_UN_subset1 = thm "parts_UN_subset1"; -val parts_UN_subset2 = thm "parts_UN_subset2"; -val parts_UN = thm "parts_UN"; -val parts_insert_subset = thm "parts_insert_subset"; -val parts_partsD = thm "parts_partsD"; -val parts_trans = thm "parts_trans"; -val parts_cut = thm "parts_cut"; -val parts_cut_eq = thm "parts_cut_eq"; -val parts_insert_eq_I = thm "parts_insert_eq_I"; -val parts_image_Key = thm "parts_image_Key"; -val MPair_analz = thm "MPair_analz"; +val synth_mono = thm "synth_mono"; val analz_increasing = thm "analz_increasing"; + +val analz_insertI = thm "analz_insertI"; val analz_subset_parts = thm "analz_subset_parts"; -val not_parts_not_analz = thm "not_parts_not_analz"; -val parts_analz = thm "parts_analz"; -val analz_parts = thm "analz_parts"; -val analz_insertI = thm "analz_insertI"; -val analz_empty = thm "analz_empty"; -val analz_Un = thm "analz_Un"; -val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset"; -val analz_image_Key = thm "analz_image_Key"; -val analz_analzD = thm "analz_analzD"; -val analz_trans = thm "analz_trans"; -val analz_cut = thm "analz_cut"; -val analz_insert_eq = thm "analz_insert_eq"; -val analz_subset_cong = thm "analz_subset_cong"; -val analz_cong = thm "analz_cong"; -val analz_insert_cong = thm "analz_insert_cong"; -val analz_trivial = thm "analz_trivial"; -val analz_UN_analz = thm "analz_UN_analz"; -val synth_mono = thm "synth_mono"; -val synth_increasing = thm "synth_increasing"; -val synth_Un = thm "synth_Un"; -val synth_insert = thm "synth_insert"; -val synth_synthD = thm "synth_synthD"; -val synth_trans = thm "synth_trans"; -val synth_cut = thm "synth_cut"; -val Agent_synth = thm "Agent_synth"; -val Number_synth = thm "Number_synth"; -val Nonce_synth_eq = thm "Nonce_synth_eq"; -val Key_synth_eq = thm "Key_synth_eq"; -val Crypt_synth_eq = thm "Crypt_synth_eq"; -val keysFor_synth = thm "keysFor_synth"; -val parts_synth = thm "parts_synth"; -val analz_analz_Un = thm "analz_analz_Un"; -val analz_synth_Un = thm "analz_synth_Un"; -val analz_synth = thm "analz_synth"; -val parts_insert_subset_Un = thm "parts_insert_subset_Un"; val Fake_parts_insert = thm "Fake_parts_insert"; val Fake_analz_insert = thm "Fake_analz_insert"; -val analz_conj_parts = thm "analz_conj_parts"; -val analz_disj_parts = thm "analz_disj_parts"; -val MPair_synth_analz = thm "MPair_synth_analz"; -val Crypt_synth_analz = thm "Crypt_synth_analz"; -val Hash_synth_analz = thm "Hash_synth_analz"; val pushes = thms "pushes"; @@ -952,7 +896,7 @@ lemma Hash_notin_image_Key [simp] :"Hash X \ Key ` A" by auto -lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))" +lemma synth_analz_mono: "G\H ==> synth (analz(G)) \ synth (analz(H))" by (simp add: synth_mono analz_mono) lemma Fake_analz_eq [simp]: @@ -964,14 +908,6 @@ apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) done - -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] - -lemma Fake_parts_insert_in_Un: - "[|Z \ parts (insert X H); X: synth (analz H)|] - ==> Z \ synth (analz H) \ parts H"; -by (blast dest: Fake_parts_insert [THEN subsetD, dest]) - text{*Two generalizations of @{text analz_insert_eq}*} lemma gen_analz_insert_eq [rule_format]: "X \ analz H ==> ALL G. H \ G --> analz (insert X G) = analz G"; diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:41:33 2003 +0200 @@ -43,8 +43,9 @@ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" declare knows_Spy_partsEs [elim] -declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare knows_Spy_partsEs [elim] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] declare image_eq_UN [simp] (*accelerates proofs involving nested images*) (*A "possibility property": there are traces that reach the end*) @@ -55,9 +56,6 @@ apply possibility done - -(**** Inductive proofs about ns_public ****) - (** Theorems of the form X \ parts (spies evs) imply that NOBODY sends messages containing X! **) @@ -70,8 +68,7 @@ "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)" by auto - -(*** Authenticity properties obtained from NS2 ***) +subsection{*Authenticity properties obtained from NS2*} (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce @@ -143,8 +140,7 @@ done - -(*** Authenticity properties obtained from NS2 ***) +subsection{*Authenticity properties obtained from NS2*} (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B [unicity of B makes Lowe's fix work] @@ -189,8 +185,7 @@ \ Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" by (blast intro: B_trusts_NS3_lemma) -(*** Overall guarantee for B ***) - +subsection{*Overall guarantee for B*} (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with NA, then A initiated the run using NA.*) diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 23 15:41:33 2003 +0200 @@ -46,8 +46,8 @@ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" declare knows_Spy_partsEs [elim] -declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare analz_into_parts [dest] +declare Fake_parts_insert_in_Un [dest] declare image_eq_UN [simp] (*accelerates proofs involving nested images*) (*A "possibility property": there are traces that reach the end*) @@ -207,6 +207,9 @@ apply (frule_tac A' = A in Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto) apply (rename_tac C B' evs3) +txt{*This is the attack! +@{subgoals[display,indent=0,margin=65]} +*} oops (* diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 23 15:41:33 2003 +0200 @@ -80,12 +80,14 @@ text{*A "possibility property": there are traces that reach the end*} -lemma "A \ Server \ \N K. \evs \ ns_shared. - Says A B (Crypt K \Nonce N, Nonce N\) \ set evs" +lemma "[| A \ Server; Key K \ used [] |] + ==> \N. \evs \ ns_shared. + Says A B (Crypt K \Nonce N, Nonce N\) \ set evs" apply (intro exI bexI) apply (rule_tac [2] ns_shared.Nil [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3, - THEN ns_shared.NS4, THEN ns_shared.NS5], possibility) + THEN ns_shared.NS4, THEN ns_shared.NS5]) +apply (possibility, simp add: used_Cons) done (*This version is similar, while instantiating ?K and ?N to epsilon-terms diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Tue Sep 23 15:41:33 2003 +0200 @@ -89,16 +89,16 @@ text{*A "possibility property": there are traces that reach the end*} -lemma "B \ Server - ==> \K. \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) apply (rule_tac [2] otway.Nil [THEN otway.OR1, THEN otway.Reception, THEN otway.OR2, THEN otway.Reception, - THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], - possibility) + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says [dest!]: diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 23 15:41:33 2003 +0200 @@ -82,15 +82,16 @@ (*A "possibility property": there are traces that reach the end*) -lemma "B \ Server - ==> \K. \evs \ otway. +lemma "[| B \ Server; Key K \ used [] |] + ==> \evs \ otway. Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ set evs" apply (intro exI bexI) apply (rule_tac [2] otway.Nil [THEN otway.OR1, THEN otway.Reception, THEN otway.OR2, THEN otway.Reception, - THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility) + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says [dest!]: diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 23 15:41:33 2003 +0200 @@ -90,15 +90,16 @@ declare Fake_parts_insert_in_Un [dest] (*A "possibility property": there are traces that reach the end*) -lemma "B \ Server - ==> \K. \NA. \evs \ otway. +lemma "[| B \ Server; Key K \ used [] |] + ==> \NA. \evs \ otway. Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ set evs" apply (intro exI bexI) apply (rule_tac [2] otway.Nil [THEN otway.OR1, THEN otway.Reception, THEN otway.OR2, THEN otway.Reception, - THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility) + THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says [dest!]: diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Public.thy Tue Sep 23 15:41:33 2003 +0200 @@ -400,7 +400,7 @@ simp_thms mem_simps --{*these two allow its use with @{text "only:"}*} disj_comms image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset - analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD] + analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD] insert_Key_singleton Key_not_used insert_Key_image Un_assoc [THEN sym] @@ -412,19 +412,4 @@ addsimps thms"analz_image_freshK_simps" *} -axioms - Key_supply_ax: "finite KK ==> \K\symKeys. K \ KK & Key K \ used evs" - --{*Unlike the corresponding property of nonces, this cannot be proved. - We have infinitely many agents and there is nothing to stop their - long-term keys from exhausting all the natural numbers. The axiom - assumes that their keys are dispersed so as to leave room for infinitely - many fresh session keys. We could, alternatively, restrict agents to - an unspecified finite number. We could however replace @{term"used evs"} - by @{term "used []"}.*} - - -lemma Key_supply1: "\K\symKeys. Key K \ used evs" -by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast) - - end diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Recur.thy Tue Sep 23 15:41:33 2003 +0200 @@ -117,37 +117,40 @@ text{*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" +lemma "Key K \ used [] + ==> \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]], possibility) + THEN recur.RA3 [OF _ _ respond.One]]) +apply (possibility, simp add: used_Cons) done text{*Case two: Alice, Bob and the server*} -lemma "\K. \NA. \evs \ recur. +lemma "[| Key K \ used []; Key K' \ used []; K \ K' |] + ==> \K. \NA. \evs \ recur. Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, END|} \ set evs" -apply (cut_tac Nonce_supply2 Key_supply2, clarify) +apply (cut_tac Nonce_supply2, clarify) apply (intro exI bexI) apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2, THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]], THEN recur.RA4]) -apply (tactic "basic_possibility_tac") -apply (tactic - "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)") +apply possibility +apply (auto simp add: used_Cons) done -(*Case three: Alice, Bob, Charlie and the server - Rather slow (16 seconds) to run every time... -lemma "\K. \NA. \evs \ recur. - Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, - END|} \ set evs" -apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify) +(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*) +lemma "[| Key K \ used []; Key K' \ used []; + Key K'' \ used []; K \ K'; K' \ K''; K \ K'' |] + ==> \K. \NA. \evs \ recur. + Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, + END|} \ set evs" +apply (cut_tac Nonce_supply3, clarify) apply (intro exI bexI) apply (rule_tac [2] recur.Nil [THEN recur.RA1, @@ -157,11 +160,8 @@ [THEN respond.Cons, THEN respond.Cons]], THEN recur.RA4, THEN recur.RA4]) apply (tactic "basic_possibility_tac") -apply (tactic - "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \ -\ eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)") +apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)") done -*) (**** Inductive proofs about recur ****) diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Shared.thy Tue Sep 23 15:41:33 2003 +0200 @@ -51,10 +51,7 @@ text{*Now cancel the @{text dest} attribute given to @{text analz.Decrypt} in its declaration.*} -ML -{* -Delrules [analz.Decrypt]; -*} +declare analz.Decrypt [rule del] text{*Rewrites should not refer to @{term "initState(Friend i)"} because that expression is not in normal form.*} @@ -137,7 +134,7 @@ apply (cut_tac evs = evs in Nonce_supply_lemma) apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) apply (rule_tac x = N in exI) -apply (rule_tac x = "Suc (N+Na) " in exI) +apply (rule_tac x = "Suc (N+Na)" in exI) apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) done @@ -147,7 +144,7 @@ apply (cut_tac evs = "evs'" in Nonce_supply_lemma) apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) apply (rule_tac x = N in exI) -apply (rule_tac x = "Suc (N+Na) " in exI) +apply (rule_tac x = "Suc (N+Na)" in exI) apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) done @@ -157,42 +154,12 @@ apply (rule someI, blast) done -subsection{*Supply fresh keys for possibility theorems.*} - -axioms - Key_supply_ax: "finite KK ==> \K. K \ KK & Key K \ used evs" - --{*Unlike the corresponding property of nonces, this cannot be proved. +text{*Unlike the corresponding property of nonces, we cannot prove + @{term "finite KK ==> \K. K \ KK & Key K \ used evs"}. We have infinitely many agents and there is nothing to stop their - long-term keys from exhausting all the natural numbers. The axiom - assumes that their keys are dispersed so as to leave room for infinitely - many fresh session keys. We could, alternatively, restrict agents to - an unspecified finite number. We could however replace @{term"used evs"} - by @{term "used []"}.*} - -lemma Key_supply1: "\K. Key K \ used evs" -by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast) + long-term keys from exhausting all the natural numbers. Instead, + possibility theorems must assume the existence of a few keys.*} -lemma Key_supply2: "\K K'. Key K \ used evs & Key K' \ used evs' & K \ K'" -apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) -apply (erule exE) -apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) -done - -lemma Key_supply3: "\K K' K''. Key K \ used evs & Key K' \ used evs' & - Key K'' \ used evs'' & K \ K' & K' \ K'' & K \ K''" -apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) -apply (erule exE) -(*Blast_tac requires instantiation of the keys for some reason*) -apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax]) -apply (erule exE) -apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K - in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast) -done - -lemma Key_supply: "Key (@ K. Key K \ used evs) \ used evs" -apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE]) -apply (rule someI, blast) -done subsection{*Tactics for possibility theorems*} @@ -200,8 +167,6 @@ {* val inj_shrK = thm "inj_shrK"; val isSym_keys = thm "isSym_keys"; -val Key_supply_ax = thm "Key_supply_ax"; -val Key_supply = thm "Key_supply"; val Nonce_supply = thm "Nonce_supply"; val invKey_K = thm "invKey_K"; val analz_Decrypt' = thm "analz_Decrypt'"; @@ -221,10 +186,6 @@ val Nonce_supply2 = thm "Nonce_supply2"; val Nonce_supply3 = thm "Nonce_supply3"; val Nonce_supply = thm "Nonce_supply"; -val Key_supply1 = thm "Key_supply1"; -val Key_supply2 = thm "Key_supply2"; -val Key_supply3 = thm "Key_supply3"; -val Key_supply = thm "Key_supply"; *} @@ -238,7 +199,7 @@ setSolver safe_solver)) THEN REPEAT_FIRST (eq_assume_tac ORELSE' - resolve_tac [refl, conjI, Nonce_supply, Key_supply]))) + resolve_tac [refl, conjI, Nonce_supply]))) (*Tactic for possibility theorems (ML script version)*) fun possibility_tac state = gen_possibility_tac (simpset()) state diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Yahalom.thy Tue Sep 23 15:41:33 2003 +0200 @@ -88,15 +88,16 @@ declare analz_into_parts [dest] (*A "possibility property": there are traces that reach the end*) -lemma "A \ Server - ==> \X NB K. \evs \ yahalom. +lemma "[| A \ Server; Key K \ used [] |] + ==> \X NB. \evs \ yahalom. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" apply (intro exI bexI) apply (rule_tac [2] yahalom.Nil [THEN yahalom.YM1, THEN yahalom.Reception, THEN yahalom.YM2, THEN yahalom.Reception, THEN yahalom.YM3, THEN yahalom.Reception, - THEN yahalom.YM4], possibility) + THEN yahalom.YM4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says: diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Yahalom2.thy Tue Sep 23 15:41:33 2003 +0200 @@ -80,14 +80,16 @@ declare analz_into_parts [dest] text{*A "possibility property": there are traces that reach the end*} -lemma "\X NB K. \evs \ yahalom. +lemma "Key K \ used [] + ==> \X NB. \evs \ yahalom. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" apply (intro exI bexI) apply (rule_tac [2] yahalom.Nil [THEN yahalom.YM1, THEN yahalom.Reception, THEN yahalom.YM2, THEN yahalom.Reception, THEN yahalom.YM3, THEN yahalom.Reception, - THEN yahalom.YM4], possibility) + THEN yahalom.YM4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says: diff -r d3b8d972a488 -r d8598e24f8fa src/HOL/Auth/Yahalom_Bad.thy --- a/src/HOL/Auth/Yahalom_Bad.thy Tue Sep 23 15:40:27 2003 +0200 +++ b/src/HOL/Auth/Yahalom_Bad.thy Tue Sep 23 15:41:33 2003 +0200 @@ -70,15 +70,16 @@ (*A "possibility property": there are traces that reach the end*) -lemma "A \ Server - ==> \X NB K. \evs \ yahalom. - Says A B {|X, Crypt K (Nonce NB)|} \ set evs" +lemma "[| A \ Server; Key K \ used [] |] + ==> \X NB. \evs \ yahalom. + Says A B {|X, Crypt K (Nonce NB)|} \ set evs" apply (intro exI bexI) apply (rule_tac [2] yahalom.Nil [THEN yahalom.YM1, THEN yahalom.Reception, THEN yahalom.YM2, THEN yahalom.Reception, THEN yahalom.YM3, THEN yahalom.Reception, - THEN yahalom.YM4], possibility) + THEN yahalom.YM4]) +apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says: