# HG changeset patch # User wenzelm # Date 1126732497 -7200 # Node ID a8c9ed3f98186a0927e0a0ac12b68040fd27c83f # Parent 23b7e14ce640293e78c99e74463d41d306389ada renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions; diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/Guard_NS_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Wed Sep 14 23:14:57 2005 +0200 @@ -0,0 +1,204 @@ +(****************************************************************************** +incorporating Lowe's fix (inclusion of B's identity in round 2) + +date: march 2002 +author: Frederic Blanqui +email: blanqui@lri.fr +webpage: http://www.lri.fr/~blanqui/ + +University of Cambridge, Computer Laboratory +William Gates Building, JJ Thomson Avenue +Cambridge CB3 0FD, United Kingdom +******************************************************************************) + +header{*Needham-Schroeder-Lowe Public-Key Protocol*} + +theory Guard_NS_Public imports Guard_Public begin + +subsection{*messages used in the protocol*} + +syntax ns1 :: "agent => agent => nat => event" + +translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})" + +syntax ns1' :: "agent => agent => agent => nat => event" + +translations "ns1' A' A B NA" +=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})" + +syntax ns2 :: "agent => agent => nat => nat => event" + +translations "ns2 B A NA NB" +=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" + +syntax ns2' :: "agent => agent => agent => nat => nat => event" + +translations "ns2' B' B A NA NB" +=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" + +syntax ns3 :: "agent => agent => nat => event" + +translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))" + +subsection{*definition of the protocol*} + +consts nsp :: "event list set" + +inductive nsp +intros + +Nil: "[]:nsp" + +Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp" + +NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp" + +NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==> +ns2 B A NA NB # evs2:nsp" + +NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==> +ns3 A B NB # evs3:nsp" + +subsection{*declarations for tactics*} + +declare knows_Spy_partsEs [elim] +declare Fake_parts_insert [THEN subsetD, dest] +declare initState.simps [simp del] + +subsection{*general properties of nsp*} + +lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs" +by (erule nsp.induct, auto) + +lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp" +by (auto simp: Gets_correct_def dest: nsp_has_no_Gets) + +lemma nsp_is_one_step [iff]: "one_step nsp" +by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto) + +lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==> +ev:set evs --> (EX A B X. ev=Says A B X)" +by (erule nsp.induct, auto) + +lemma nsp_has_only_Says [iff]: "has_only_Says nsp" +by (auto simp: has_only_Says_def dest: nsp_has_only_Says') + +lemma nsp_is_regular [iff]: "regular nsp" +apply (simp only: regular_def, clarify) +by (erule nsp.induct, auto simp: initState.simps knows.simps) + +subsection{*nonce are used only once*} + +lemma NA_is_uniq [rule_format]: "evs:nsp ==> +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) +--> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs) +--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'" +apply (erule nsp.induct, simp_all) +by (blast intro: analz_insertI)+ + +lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==> +Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs) +--> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) +--> Nonce NA:analz (spies evs)" +apply (erule nsp.induct, simp_all) +by (blast intro: analz_insertI)+ + +lemma no_Nonce_NS1_NS2' [rule_format]: +"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs); +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |] +==> Nonce NA:analz (spies evs)" +by (rule no_Nonce_NS1_NS2, auto) + +lemma NB_is_uniq [rule_format]: "evs:nsp ==> +Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) +--> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs) +--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'" +apply (erule nsp.induct, simp_all) +by (blast intro: analz_insertI)+ + +subsection{*guardedness of NA*} + +lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> +ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)" +apply (erule nsp.induct) +(* Nil *) +apply simp_all +(* Fake *) +apply safe +apply (erule in_synth_Guard, erule Guard_analz, simp) +(* NS1 *) +apply blast +apply blast +apply blast +apply (drule Nonce_neq, simp+, rule No_Nonce, simp) +(* NS2 *) +apply (frule_tac A=A in Nonce_neq, simp+) +apply (case_tac "NAa=NA") +apply (drule Guard_Nonce_analz, simp+) +apply (drule Says_imp_knows_Spy)+ +apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto) +(* NS3 *) +apply (case_tac "NB=NA", clarify) +apply (drule Guard_Nonce_analz, simp+) +apply (drule Says_imp_knows_Spy)+ +by (drule no_Nonce_NS1_NS2, auto) + +subsection{*guardedness of NB*} + +lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> +ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" +apply (erule nsp.induct) +(* Nil *) +apply simp_all +(* Fake *) +apply safe +apply (erule in_synth_Guard, erule Guard_analz, simp) +(* NS1 *) +apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp) +(* NS2 *) +apply blast +apply blast +apply blast +apply (frule_tac A=B and n=NB in Nonce_neq, simp+) +apply (case_tac "NAa=NB") +apply (drule Guard_Nonce_analz, simp+) +apply (drule Says_imp_knows_Spy)+ +apply (drule no_Nonce_NS1_NS2, auto) +(* NS3 *) +apply (case_tac "NBa=NB", clarify) +apply (drule Guard_Nonce_analz, simp+) +apply (drule Says_imp_knows_Spy)+ +by (drule_tac A=Aa and A'=A in NB_is_uniq, auto) + +subsection{*Agents' Authentication*} + +lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==> +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) +--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs" +apply (erule nsp.induct, simp_all) +by (blast intro: analz_insertI)+ + +lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs +--> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) +--> ns2 B A NA NB:set evs" +apply (erule nsp.induct, simp_all, safe) +apply (frule_tac B=B in ns1_imp_Guard, simp+) +apply (drule Guard_Nonce_analz, simp+, blast) +apply (frule_tac B=B in ns1_imp_Guard, simp+) +apply (drule Guard_Nonce_analz, simp+, blast) +apply (frule_tac B=B in ns1_imp_Guard, simp+) +by (drule Guard_Nonce_analz, simp+, blast+) + +lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs +--> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs" +apply (erule nsp.induct, simp_all, safe) +apply (frule_tac B=B in ns2_imp_Guard, simp+) +apply (drule Guard_Nonce_analz, simp+, blast) +apply (frule_tac B=B in ns2_imp_Guard, simp+) +apply (drule Guard_Nonce_analz, simp+, blast) +apply (frule_tac B=B in ns2_imp_Guard, simp+) +apply (drule Guard_Nonce_analz, simp+, blast, blast) +apply (frule_tac B=B in ns2_imp_Guard, simp+) +by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq) + +end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/Guard_OtwayRees.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Wed Sep 14 23:14:57 2005 +0200 @@ -0,0 +1,195 @@ +(****************************************************************************** +date: march 2002 +author: Frederic Blanqui +email: blanqui@lri.fr +webpage: http://www.lri.fr/~blanqui/ + +University of Cambridge, Computer Laboratory +William Gates Building, JJ Thomson Avenue +Cambridge CB3 0FD, United Kingdom +******************************************************************************) + +header{*Otway-Rees Protocol*} + +theory Guard_OtwayRees imports Guard_Shared begin + +subsection{*messages used in the protocol*} + +syntax nil :: "msg" + +translations "nil" == "Number 0" + +syntax or1 :: "agent => agent => nat => event" + +translations "or1 A B NA" +=> "Says A B {|Nonce NA, Agent A, Agent B, + Ciph A {|Nonce NA, Agent A, Agent B|}|}" + +syntax or1' :: "agent => agent => agent => nat => msg => event" + +translations "or1' A' A B NA X" +=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}" + +syntax or2 :: "agent => agent => nat => nat => msg => event" + +translations "or2 A B NA NB X" +=> "Says B Server {|Nonce NA, Agent A, Agent B, X, + Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" + +syntax or2' :: "agent => agent => agent => nat => nat => event" + +translations "or2' B' A B NA NB" +=> "Says B' Server {|Nonce NA, Agent A, Agent B, + Ciph A {|Nonce NA, Agent A, Agent B|}, + Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" + +syntax or3 :: "agent => agent => nat => nat => key => event" + +translations "or3 A B NA NB K" +=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|}, + Ciph B {|Nonce NB, Key K|}|}" + +syntax or3':: "agent => msg => agent => agent => nat => nat => key => event" + +translations "or3' S Y A B NA NB K" +=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}" + +syntax or4 :: "agent => agent => nat => msg => event" + +translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}" + +syntax or4' :: "agent => agent => nat => msg => event" + +translations "or4' B' A NA K" => +"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}" + +subsection{*definition of the protocol*} + +consts or :: "event list set" + +inductive or +intros + +Nil: "[]:or" + +Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or" + +OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or" + +OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |] +==> or2 A B NA NB X # evs2:or" + +OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |] +==> or3 A B NA NB K # evs3:or" + +OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |] +==> or4 A B NA X # evs4:or" + +subsection{*declarations for tactics*} + +declare knows_Spy_partsEs [elim] +declare Fake_parts_insert [THEN subsetD, dest] +declare initState.simps [simp del] + +subsection{*general properties of or*} + +lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs" +by (erule or.induct, auto) + +lemma or_is_Gets_correct [iff]: "Gets_correct or" +by (auto simp: Gets_correct_def dest: or_has_no_Gets) + +lemma or_is_one_step [iff]: "one_step or" +by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto) + +lemma or_has_only_Says' [rule_format]: "evs:or ==> +ev:set evs --> (EX A B X. ev=Says A B X)" +by (erule or.induct, auto) + +lemma or_has_only_Says [iff]: "has_only_Says or" +by (auto simp: has_only_Says_def dest: or_has_only_Says') + +subsection{*or is regular*} + +lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs +==> X:parts (spies evs)" +by blast + +lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs +==> X:parts (spies evs)" +by blast + +lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs +==> K:parts (spies evs)" +by blast + +lemma or_is_regular [iff]: "regular or" +apply (simp only: regular_def, clarify) +apply (erule or.induct, simp_all add: initState.simps knows.simps) +by (auto dest: parts_sub) + +subsection{*guardedness of KAB*} + +lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==> +or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" +apply (erule or.induct) +(* Nil *) +apply simp_all +(* Fake *) +apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp) +(* OR1 *) +apply blast +(* OR2 *) +apply safe +apply (blast dest: Says_imp_spies, blast) +(* OR3 *) +apply blast +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) +(* OR4 *) +by (blast dest: Says_imp_spies in_GuardK_kparts) + +subsection{*guardedness of NB*} + +lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==> +or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" +apply (erule or.induct) +(* Nil *) +apply simp_all +(* Fake *) +apply safe +apply (erule in_synth_Guard, erule Guard_analz, simp) +(* OR1 *) +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) +(* OR2 *) +apply blast +apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp) +apply (blast intro!: No_Nonce dest: used_parts) +apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp) +apply (blast intro!: No_Nonce dest: used_parts) +apply (blast dest: Says_imp_spies) +apply (blast dest: Says_imp_spies) +apply (case_tac "Ba=B", clarsimp) +apply (drule_tac n=NB and A=B in Nonce_neq, simp+) +apply (drule Says_imp_spies) +apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp) +(* OR3 *) +apply (drule Says_imp_spies) +apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp) +apply (case_tac "Aa=B", clarsimp) +apply (case_tac "NAa=NB", clarsimp) +apply (drule Says_imp_spies) +apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}" + and K="shrK Aa" in in_Guard_kparts_Crypt, simp+) +apply (simp add: No_Nonce) +apply (case_tac "Ba=B", clarsimp) +apply (case_tac "NBa=NB", clarify) +apply (drule Says_imp_spies) +apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}" + and K="shrK Ba" in in_Guard_kparts_Crypt, simp+) +apply (simp add: No_Nonce) +(* OR4 *) +by (blast dest: Says_imp_spies)+ + +end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/Guard_Yahalom.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Sep 14 23:14:57 2005 +0200 @@ -0,0 +1,259 @@ +(****************************************************************************** +date: march 2002 +author: Frederic Blanqui +email: blanqui@lri.fr +webpage: http://www.lri.fr/~blanqui/ + +University of Cambridge, Computer Laboratory +William Gates Building, JJ Thomson Avenue +Cambridge CB3 0FD, United Kingdom +******************************************************************************) + +header{*Yahalom Protocol*} + +theory Guard_Yahalom imports Guard_Shared begin + +subsection{*messages used in the protocol*} + +syntax ya1 :: "agent => agent => nat => event" + +translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}" + +syntax ya1' :: "agent => agent => agent => nat => event" + +translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}" + +syntax ya2 :: "agent => agent => nat => nat => event" + +translations "ya2 A B NA NB" +=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}" + +syntax ya2' :: "agent => agent => agent => nat => nat => event" + +translations "ya2' B' A B NA NB" +=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}" + +syntax ya3 :: "agent => agent => nat => nat => key => event" + +translations "ya3 A B NA NB K" +=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, + Ciph B {|Agent A, Key K|}|}" + +syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event" + +translations "ya3' S Y A B NA NB K" +=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}" + +syntax ya4 :: "agent => agent => nat => nat => msg => event" + +translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}" + +syntax ya4' :: "agent => agent => nat => nat => msg => event" + +translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}" + +subsection{*definition of the protocol*} + +consts ya :: "event list set" + +inductive ya +intros + +Nil: "[]:ya" + +Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya" + +YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya" + +YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |] +==> ya2 A B NA NB # evs2:ya" + +YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |] +==> ya3 A B NA NB K # evs3:ya" + +YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |] +==> ya4 A B K NB Y # evs4:ya" + +subsection{*declarations for tactics*} + +declare knows_Spy_partsEs [elim] +declare Fake_parts_insert [THEN subsetD, dest] +declare initState.simps [simp del] + +subsection{*general properties of ya*} + +lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs" +by (erule ya.induct, auto) + +lemma ya_is_Gets_correct [iff]: "Gets_correct ya" +by (auto simp: Gets_correct_def dest: ya_has_no_Gets) + +lemma ya_is_one_step [iff]: "one_step ya" +by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto) + +lemma ya_has_only_Says' [rule_format]: "evs:ya ==> +ev:set evs --> (EX A B X. ev=Says A B X)" +by (erule ya.induct, auto) + +lemma ya_has_only_Says [iff]: "has_only_Says ya" +by (auto simp: has_only_Says_def dest: ya_has_only_Says') + +lemma ya_is_regular [iff]: "regular ya" +apply (simp only: regular_def, clarify) +apply (erule ya.induct, simp_all add: initState.simps knows.simps) +by (auto dest: parts_sub) + +subsection{*guardedness of KAB*} + +lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==> +ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" +apply (erule ya.induct) +(* Nil *) +apply simp_all +(* Fake *) +apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp) +(* YA1 *) +(* YA2 *) +apply safe +apply (blast dest: Says_imp_spies) +(* YA3 *) +apply blast +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) +(* YA4 *) +apply (blast dest: Says_imp_spies in_GuardK_kparts) +by blast + +subsection{*session keys are not symmetric keys*} + +lemma KAB_isnt_shrK [rule_format]: "evs:ya ==> +ya3 A B NA NB K:set evs --> K ~:range shrK" +by (erule ya.induct, auto) + +lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs" +by (blast dest: KAB_isnt_shrK) + +subsection{*ya2' implies ya1'*} + +lemma ya2'_parts_imp_ya1'_parts [rule_format]: + "[| evs:ya; B ~:bad |] ==> + Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) --> + {|Agent A, Nonce NA|}:spies evs" +by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts) + +lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |] +==> {|Agent A, Nonce NA|}:spies evs" +by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts) + +subsection{*uniqueness of NB*} + +lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==> +Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) --> +Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) --> +A=A' & B=B' & NA=NA'" +apply (erule ya.induct, simp_all, clarify) +apply (drule Crypt_synth_insert, simp+) +apply (drule Crypt_synth_insert, simp+, safe) +apply (drule not_used_parts_false, simp+)+ +by (drule Says_not_parts, simp+)+ + +lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs; +ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |] +==> A=A' & B=B' & NA=NA'" +by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies) + +subsection{*ya3' implies ya2'*} + +lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==> +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs) +--> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)" +apply (erule ya.induct, simp_all) +apply (clarify, drule Crypt_synth_insert, simp+) +apply (blast intro: parts_sub, blast) +by (auto dest: Says_imp_spies parts_parts) + +lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==> +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs) +--> (EX B'. ya2' B' A B NA NB:set evs)" +apply (erule ya.induct, simp_all, safe) +apply (drule Crypt_synth_insert, simp+) +apply (drule Crypt_synth_insert, simp+, blast) +apply blast +apply blast +by (auto dest: Says_imp_spies2 parts_parts) + +lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |] +==> (EX B'. ya2' B' A B NA NB:set evs)" +by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies) + +subsection{*ya3' implies ya3*} + +lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==> +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs) +--> ya3 A B NA NB K:set evs" +apply (erule ya.induct, simp_all, safe) +apply (drule Crypt_synth_insert, simp+) +by (blast dest: Says_imp_spies2 parts_parts) + +lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |] +==> ya3 A B NA NB K:set evs" +by (blast dest: Says_imp_spies ya3'_parts_imp_ya3) + +subsection{*guardedness of NB*} + +constdefs ya_keys :: "agent => agent => nat => nat => event list => key set" +"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}" + +lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==> +ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)" +apply (erule ya.induct) +(* Nil *) +apply (simp_all add: ya_keys_def) +(* Fake *) +apply safe +apply (erule in_synth_Guard, erule Guard_analz, simp, clarify) +apply (frule_tac B=B in Guard_KAB, simp+) +apply (drule_tac p=ya in GuardK_Key_analz, simp+) +apply (blast dest: KAB_isnt_shrK, simp) +(* YA1 *) +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) +(* YA2 *) +apply blast +apply (drule Says_imp_spies) +apply (drule_tac n=NB in Nonce_neq, simp+) +apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+) +apply (rule No_Nonce, simp) +(* YA3 *) +apply (rule Guard_extand, simp, blast) +apply (case_tac "NAa=NB", clarify) +apply (frule Says_imp_spies) +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) +apply (drule ya2'_imp_ya1'_parts, simp, blast, blast) +apply (case_tac "NBa=NB", clarify) +apply (frule Says_imp_spies) +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) +apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+) +apply (simp add: No_Nonce, blast) +(* YA4 *) +apply (blast dest: Says_imp_spies) +apply (case_tac "NBa=NB", clarify) +apply (frule_tac A=S in Says_imp_spies) +apply (frule in_Guard_kparts_Crypt, simp+) +apply (blast dest: Says_imp_spies) +apply (case_tac "NBa=NB", clarify) +apply (frule_tac A=S in Says_imp_spies) +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp) +apply (frule ya3'_imp_ya2', simp+, blast, clarify) +apply (frule_tac A=B' in Says_imp_spies) +apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+) +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) +apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify) +apply (drule ya3'_imp_ya3, simp+) +apply (simp add: Guard_Nonce) +apply (simp add: No_Nonce) +done + +end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/NS_Public.thy --- a/src/HOL/Auth/Guard/NS_Public.thy Wed Sep 14 23:06:02 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,204 +0,0 @@ -(****************************************************************************** -incorporating Lowe's fix (inclusion of B's identity in round 2) - -date: march 2002 -author: Frederic Blanqui -email: blanqui@lri.fr -webpage: http://www.lri.fr/~blanqui/ - -University of Cambridge, Computer Laboratory -William Gates Building, JJ Thomson Avenue -Cambridge CB3 0FD, United Kingdom -******************************************************************************) - -header{*Needham-Schroeder-Lowe Public-Key Protocol*} - -theory NS_Public imports Guard_Public begin - -subsection{*messages used in the protocol*} - -syntax ns1 :: "agent => agent => nat => event" - -translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})" - -syntax ns1' :: "agent => agent => agent => nat => event" - -translations "ns1' A' A B NA" -=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})" - -syntax ns2 :: "agent => agent => nat => nat => event" - -translations "ns2 B A NA NB" -=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" - -syntax ns2' :: "agent => agent => agent => nat => nat => event" - -translations "ns2' B' B A NA NB" -=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" - -syntax ns3 :: "agent => agent => nat => event" - -translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))" - -subsection{*definition of the protocol*} - -consts nsp :: "event list set" - -inductive nsp -intros - -Nil: "[]:nsp" - -Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp" - -NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp" - -NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==> -ns2 B A NA NB # evs2:nsp" - -NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==> -ns3 A B NB # evs3:nsp" - -subsection{*declarations for tactics*} - -declare knows_Spy_partsEs [elim] -declare Fake_parts_insert [THEN subsetD, dest] -declare initState.simps [simp del] - -subsection{*general properties of nsp*} - -lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs" -by (erule nsp.induct, auto) - -lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp" -by (auto simp: Gets_correct_def dest: nsp_has_no_Gets) - -lemma nsp_is_one_step [iff]: "one_step nsp" -by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto) - -lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==> -ev:set evs --> (EX A B X. ev=Says A B X)" -by (erule nsp.induct, auto) - -lemma nsp_has_only_Says [iff]: "has_only_Says nsp" -by (auto simp: has_only_Says_def dest: nsp_has_only_Says') - -lemma nsp_is_regular [iff]: "regular nsp" -apply (simp only: regular_def, clarify) -by (erule nsp.induct, auto simp: initState.simps knows.simps) - -subsection{*nonce are used only once*} - -lemma NA_is_uniq [rule_format]: "evs:nsp ==> -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) ---> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs) ---> Nonce NA ~:analz (spies evs) --> A=A' & B=B'" -apply (erule nsp.induct, simp_all) -by (blast intro: analz_insertI)+ - -lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==> -Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs) ---> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) ---> Nonce NA:analz (spies evs)" -apply (erule nsp.induct, simp_all) -by (blast intro: analz_insertI)+ - -lemma no_Nonce_NS1_NS2' [rule_format]: -"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs); -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |] -==> Nonce NA:analz (spies evs)" -by (rule no_Nonce_NS1_NS2, auto) - -lemma NB_is_uniq [rule_format]: "evs:nsp ==> -Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) ---> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs) ---> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'" -apply (erule nsp.induct, simp_all) -by (blast intro: analz_insertI)+ - -subsection{*guardedness of NA*} - -lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> -ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)" -apply (erule nsp.induct) -(* Nil *) -apply simp_all -(* Fake *) -apply safe -apply (erule in_synth_Guard, erule Guard_analz, simp) -(* NS1 *) -apply blast -apply blast -apply blast -apply (drule Nonce_neq, simp+, rule No_Nonce, simp) -(* NS2 *) -apply (frule_tac A=A in Nonce_neq, simp+) -apply (case_tac "NAa=NA") -apply (drule Guard_Nonce_analz, simp+) -apply (drule Says_imp_knows_Spy)+ -apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto) -(* NS3 *) -apply (case_tac "NB=NA", clarify) -apply (drule Guard_Nonce_analz, simp+) -apply (drule Says_imp_knows_Spy)+ -by (drule no_Nonce_NS1_NS2, auto) - -subsection{*guardedness of NB*} - -lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> -ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" -apply (erule nsp.induct) -(* Nil *) -apply simp_all -(* Fake *) -apply safe -apply (erule in_synth_Guard, erule Guard_analz, simp) -(* NS1 *) -apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp) -(* NS2 *) -apply blast -apply blast -apply blast -apply (frule_tac A=B and n=NB in Nonce_neq, simp+) -apply (case_tac "NAa=NB") -apply (drule Guard_Nonce_analz, simp+) -apply (drule Says_imp_knows_Spy)+ -apply (drule no_Nonce_NS1_NS2, auto) -(* NS3 *) -apply (case_tac "NBa=NB", clarify) -apply (drule Guard_Nonce_analz, simp+) -apply (drule Says_imp_knows_Spy)+ -by (drule_tac A=Aa and A'=A in NB_is_uniq, auto) - -subsection{*Agents' Authentication*} - -lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==> -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) ---> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs" -apply (erule nsp.induct, simp_all) -by (blast intro: analz_insertI)+ - -lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs ---> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) ---> ns2 B A NA NB:set evs" -apply (erule nsp.induct, simp_all, safe) -apply (frule_tac B=B in ns1_imp_Guard, simp+) -apply (drule Guard_Nonce_analz, simp+, blast) -apply (frule_tac B=B in ns1_imp_Guard, simp+) -apply (drule Guard_Nonce_analz, simp+, blast) -apply (frule_tac B=B in ns1_imp_Guard, simp+) -by (drule Guard_Nonce_analz, simp+, blast+) - -lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs ---> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs" -apply (erule nsp.induct, simp_all, safe) -apply (frule_tac B=B in ns2_imp_Guard, simp+) -apply (drule Guard_Nonce_analz, simp+, blast) -apply (frule_tac B=B in ns2_imp_Guard, simp+) -apply (drule Guard_Nonce_analz, simp+, blast) -apply (frule_tac B=B in ns2_imp_Guard, simp+) -apply (drule Guard_Nonce_analz, simp+, blast, blast) -apply (frule_tac B=B in ns2_imp_Guard, simp+) -by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq) - -end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/OtwayRees.thy --- a/src/HOL/Auth/Guard/OtwayRees.thy Wed Sep 14 23:06:02 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -(****************************************************************************** -date: march 2002 -author: Frederic Blanqui -email: blanqui@lri.fr -webpage: http://www.lri.fr/~blanqui/ - -University of Cambridge, Computer Laboratory -William Gates Building, JJ Thomson Avenue -Cambridge CB3 0FD, United Kingdom -******************************************************************************) - -header{*Otway-Rees Protocol*} - -theory OtwayRees imports Guard_Shared begin - -subsection{*messages used in the protocol*} - -syntax nil :: "msg" - -translations "nil" == "Number 0" - -syntax or1 :: "agent => agent => nat => event" - -translations "or1 A B NA" -=> "Says A B {|Nonce NA, Agent A, Agent B, - Ciph A {|Nonce NA, Agent A, Agent B|}|}" - -syntax or1' :: "agent => agent => agent => nat => msg => event" - -translations "or1' A' A B NA X" -=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}" - -syntax or2 :: "agent => agent => nat => nat => msg => event" - -translations "or2 A B NA NB X" -=> "Says B Server {|Nonce NA, Agent A, Agent B, X, - Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" - -syntax or2' :: "agent => agent => agent => nat => nat => event" - -translations "or2' B' A B NA NB" -=> "Says B' Server {|Nonce NA, Agent A, Agent B, - Ciph A {|Nonce NA, Agent A, Agent B|}, - Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" - -syntax or3 :: "agent => agent => nat => nat => key => event" - -translations "or3 A B NA NB K" -=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|}, - Ciph B {|Nonce NB, Key K|}|}" - -syntax or3':: "agent => msg => agent => agent => nat => nat => key => event" - -translations "or3' S Y A B NA NB K" -=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}" - -syntax or4 :: "agent => agent => nat => msg => event" - -translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}" - -syntax or4' :: "agent => agent => nat => msg => event" - -translations "or4' B' A NA K" => -"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}" - -subsection{*definition of the protocol*} - -consts or :: "event list set" - -inductive or -intros - -Nil: "[]:or" - -Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or" - -OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or" - -OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |] -==> or2 A B NA NB X # evs2:or" - -OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |] -==> or3 A B NA NB K # evs3:or" - -OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |] -==> or4 A B NA X # evs4:or" - -subsection{*declarations for tactics*} - -declare knows_Spy_partsEs [elim] -declare Fake_parts_insert [THEN subsetD, dest] -declare initState.simps [simp del] - -subsection{*general properties of or*} - -lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs" -by (erule or.induct, auto) - -lemma or_is_Gets_correct [iff]: "Gets_correct or" -by (auto simp: Gets_correct_def dest: or_has_no_Gets) - -lemma or_is_one_step [iff]: "one_step or" -by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto) - -lemma or_has_only_Says' [rule_format]: "evs:or ==> -ev:set evs --> (EX A B X. ev=Says A B X)" -by (erule or.induct, auto) - -lemma or_has_only_Says [iff]: "has_only_Says or" -by (auto simp: has_only_Says_def dest: or_has_only_Says') - -subsection{*or is regular*} - -lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs -==> X:parts (spies evs)" -by blast - -lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs -==> X:parts (spies evs)" -by blast - -lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs -==> K:parts (spies evs)" -by blast - -lemma or_is_regular [iff]: "regular or" -apply (simp only: regular_def, clarify) -apply (erule or.induct, simp_all add: initState.simps knows.simps) -by (auto dest: parts_sub) - -subsection{*guardedness of KAB*} - -lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==> -or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" -apply (erule or.induct) -(* Nil *) -apply simp_all -(* Fake *) -apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp) -(* OR1 *) -apply blast -(* OR2 *) -apply safe -apply (blast dest: Says_imp_spies, blast) -(* OR3 *) -apply blast -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) -(* OR4 *) -by (blast dest: Says_imp_spies in_GuardK_kparts) - -subsection{*guardedness of NB*} - -lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==> -or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" -apply (erule or.induct) -(* Nil *) -apply simp_all -(* Fake *) -apply safe -apply (erule in_synth_Guard, erule Guard_analz, simp) -(* OR1 *) -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) -(* OR2 *) -apply blast -apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp) -apply (blast intro!: No_Nonce dest: used_parts) -apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp) -apply (blast intro!: No_Nonce dest: used_parts) -apply (blast dest: Says_imp_spies) -apply (blast dest: Says_imp_spies) -apply (case_tac "Ba=B", clarsimp) -apply (drule_tac n=NB and A=B in Nonce_neq, simp+) -apply (drule Says_imp_spies) -apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp) -(* OR3 *) -apply (drule Says_imp_spies) -apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp) -apply (case_tac "Aa=B", clarsimp) -apply (case_tac "NAa=NB", clarsimp) -apply (drule Says_imp_spies) -apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}" - and K="shrK Aa" in in_Guard_kparts_Crypt, simp+) -apply (simp add: No_Nonce) -apply (case_tac "Ba=B", clarsimp) -apply (case_tac "NBa=NB", clarify) -apply (drule Says_imp_spies) -apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}" - and K="shrK Ba" in in_Guard_kparts_Crypt, simp+) -apply (simp add: No_Nonce) -(* OR4 *) -by (blast dest: Says_imp_spies)+ - -end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/Guard/Yahalom.thy --- a/src/HOL/Auth/Guard/Yahalom.thy Wed Sep 14 23:06:02 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,259 +0,0 @@ -(****************************************************************************** -date: march 2002 -author: Frederic Blanqui -email: blanqui@lri.fr -webpage: http://www.lri.fr/~blanqui/ - -University of Cambridge, Computer Laboratory -William Gates Building, JJ Thomson Avenue -Cambridge CB3 0FD, United Kingdom -******************************************************************************) - -header{*Yahalom Protocol*} - -theory Yahalom imports Guard_Shared begin - -subsection{*messages used in the protocol*} - -syntax ya1 :: "agent => agent => nat => event" - -translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}" - -syntax ya1' :: "agent => agent => agent => nat => event" - -translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}" - -syntax ya2 :: "agent => agent => nat => nat => event" - -translations "ya2 A B NA NB" -=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}" - -syntax ya2' :: "agent => agent => agent => nat => nat => event" - -translations "ya2' B' A B NA NB" -=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}" - -syntax ya3 :: "agent => agent => nat => nat => key => event" - -translations "ya3 A B NA NB K" -=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, - Ciph B {|Agent A, Key K|}|}" - -syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event" - -translations "ya3' S Y A B NA NB K" -=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}" - -syntax ya4 :: "agent => agent => nat => nat => msg => event" - -translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}" - -syntax ya4' :: "agent => agent => nat => nat => msg => event" - -translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}" - -subsection{*definition of the protocol*} - -consts ya :: "event list set" - -inductive ya -intros - -Nil: "[]:ya" - -Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya" - -YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya" - -YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |] -==> ya2 A B NA NB # evs2:ya" - -YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |] -==> ya3 A B NA NB K # evs3:ya" - -YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |] -==> ya4 A B K NB Y # evs4:ya" - -subsection{*declarations for tactics*} - -declare knows_Spy_partsEs [elim] -declare Fake_parts_insert [THEN subsetD, dest] -declare initState.simps [simp del] - -subsection{*general properties of ya*} - -lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs" -by (erule ya.induct, auto) - -lemma ya_is_Gets_correct [iff]: "Gets_correct ya" -by (auto simp: Gets_correct_def dest: ya_has_no_Gets) - -lemma ya_is_one_step [iff]: "one_step ya" -by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto) - -lemma ya_has_only_Says' [rule_format]: "evs:ya ==> -ev:set evs --> (EX A B X. ev=Says A B X)" -by (erule ya.induct, auto) - -lemma ya_has_only_Says [iff]: "has_only_Says ya" -by (auto simp: has_only_Says_def dest: ya_has_only_Says') - -lemma ya_is_regular [iff]: "regular ya" -apply (simp only: regular_def, clarify) -apply (erule ya.induct, simp_all add: initState.simps knows.simps) -by (auto dest: parts_sub) - -subsection{*guardedness of KAB*} - -lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==> -ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" -apply (erule ya.induct) -(* Nil *) -apply simp_all -(* Fake *) -apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp) -(* YA1 *) -(* YA2 *) -apply safe -apply (blast dest: Says_imp_spies) -(* YA3 *) -apply blast -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) -(* YA4 *) -apply (blast dest: Says_imp_spies in_GuardK_kparts) -by blast - -subsection{*session keys are not symmetric keys*} - -lemma KAB_isnt_shrK [rule_format]: "evs:ya ==> -ya3 A B NA NB K:set evs --> K ~:range shrK" -by (erule ya.induct, auto) - -lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs" -by (blast dest: KAB_isnt_shrK) - -subsection{*ya2' implies ya1'*} - -lemma ya2'_parts_imp_ya1'_parts [rule_format]: - "[| evs:ya; B ~:bad |] ==> - Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) --> - {|Agent A, Nonce NA|}:spies evs" -by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts) - -lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |] -==> {|Agent A, Nonce NA|}:spies evs" -by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts) - -subsection{*uniqueness of NB*} - -lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==> -Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) --> -Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) --> -A=A' & B=B' & NA=NA'" -apply (erule ya.induct, simp_all, clarify) -apply (drule Crypt_synth_insert, simp+) -apply (drule Crypt_synth_insert, simp+, safe) -apply (drule not_used_parts_false, simp+)+ -by (drule Says_not_parts, simp+)+ - -lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs; -ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |] -==> A=A' & B=B' & NA=NA'" -by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies) - -subsection{*ya3' implies ya2'*} - -lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==> -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs) ---> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)" -apply (erule ya.induct, simp_all) -apply (clarify, drule Crypt_synth_insert, simp+) -apply (blast intro: parts_sub, blast) -by (auto dest: Says_imp_spies parts_parts) - -lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==> -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs) ---> (EX B'. ya2' B' A B NA NB:set evs)" -apply (erule ya.induct, simp_all, safe) -apply (drule Crypt_synth_insert, simp+) -apply (drule Crypt_synth_insert, simp+, blast) -apply blast -apply blast -by (auto dest: Says_imp_spies2 parts_parts) - -lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |] -==> (EX B'. ya2' B' A B NA NB:set evs)" -by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies) - -subsection{*ya3' implies ya3*} - -lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==> -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs) ---> ya3 A B NA NB K:set evs" -apply (erule ya.induct, simp_all, safe) -apply (drule Crypt_synth_insert, simp+) -by (blast dest: Says_imp_spies2 parts_parts) - -lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |] -==> ya3 A B NA NB K:set evs" -by (blast dest: Says_imp_spies ya3'_parts_imp_ya3) - -subsection{*guardedness of NB*} - -constdefs ya_keys :: "agent => agent => nat => nat => event list => key set" -"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}" - -lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==> -ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)" -apply (erule ya.induct) -(* Nil *) -apply (simp_all add: ya_keys_def) -(* Fake *) -apply safe -apply (erule in_synth_Guard, erule Guard_analz, simp, clarify) -apply (frule_tac B=B in Guard_KAB, simp+) -apply (drule_tac p=ya in GuardK_Key_analz, simp+) -apply (blast dest: KAB_isnt_shrK, simp) -(* YA1 *) -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) -(* YA2 *) -apply blast -apply (drule Says_imp_spies) -apply (drule_tac n=NB in Nonce_neq, simp+) -apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+) -apply (rule No_Nonce, simp) -(* YA3 *) -apply (rule Guard_extand, simp, blast) -apply (case_tac "NAa=NB", clarify) -apply (frule Says_imp_spies) -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) -apply (drule ya2'_imp_ya1'_parts, simp, blast, blast) -apply (case_tac "NBa=NB", clarify) -apply (frule Says_imp_spies) -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) -apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+) -apply (simp add: No_Nonce, blast) -(* YA4 *) -apply (blast dest: Says_imp_spies) -apply (case_tac "NBa=NB", clarify) -apply (frule_tac A=S in Says_imp_spies) -apply (frule in_Guard_kparts_Crypt, simp+) -apply (blast dest: Says_imp_spies) -apply (case_tac "NBa=NB", clarify) -apply (frule_tac A=S in Says_imp_spies) -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp) -apply (frule ya3'_imp_ya2', simp+, blast, clarify) -apply (frule_tac A=B' in Says_imp_spies) -apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+) -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) -apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify) -apply (drule ya3'_imp_ya3, simp+) -apply (simp add: Guard_Nonce) -apply (simp add: No_Nonce) -done - -end diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Wed Sep 14 23:06:02 2005 +0200 +++ b/src/HOL/Auth/ROOT.ML Wed Sep 14 23:14:57 2005 +0200 @@ -8,6 +8,8 @@ no_document use_thy "NatPair"; +add_path "Guard"; + set timing; (*Shared-key protocols*) @@ -31,9 +33,9 @@ time_use_thy "CertifiedEmail"; (*Blanqui's "guard" concept: protocol-independent secrecy*) -time_use_thy "Guard/P1"; -time_use_thy "Guard/P2"; -time_use_thy "Guard/NS_Public"; -time_use_thy "Guard/OtwayRees"; -time_use_thy "Guard/Yahalom"; -time_use_thy "Guard/Proto"; +time_use_thy "P1"; +time_use_thy "P2"; +time_use_thy "Guard_NS_Public"; +time_use_thy "Guard_OtwayRees"; +time_use_thy "Guard_Yahalom"; +time_use_thy "Proto"; diff -r 23b7e14ce640 -r a8c9ed3f9818 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Sep 14 23:06:02 2005 +0200 +++ b/src/HOL/IsaMakefile Wed Sep 14 23:14:57 2005 +0200 @@ -390,9 +390,9 @@ Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \ Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \ Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ - Auth/Guard/NS_Public.thy Auth/Guard/OtwayRees.thy \ + Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \ Auth/Guard/P1.thy Auth/Guard/P2.thy \ - Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy\ + Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\ Auth/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL Auth