# HG changeset patch # User paulson # Date 1029938010 -7200 # Node ID 890d736b93a50c9aa68ea08640e67b358e0d29a7 # Parent febb8e5d2a9d2d34b7d322191b17de798daa0498 Frederic Blanqui's new "guard" examples diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Analz.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Analz.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,277 @@ +(****************************************************************************** +date: december 2001 +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{*Decomposition of Analz into two parts*} + +theory Analz = Extensions: + +text{*decomposition of @{term analz} into two parts: + @{term pparts} (for pairs) and analz of @{term kparts}*} + +subsection{*messages that do not contribute to analz*} + +consts pparts :: "msg set => msg set" + +inductive "pparts H" +intros +Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H" +Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H" +Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H" + +subsection{*basic facts about @{term pparts}*} + +lemma pparts_is_MPair [dest]: "X:pparts H ==> is_MPair X" +by (erule pparts.induct, auto) + +lemma Crypt_notin_pparts [iff]: "Crypt K X ~:pparts H" +by auto + +lemma Key_notin_pparts [iff]: "Key K ~:pparts H" +by auto + +lemma Nonce_notin_pparts [iff]: "Nonce n ~:pparts H" +by auto + +lemma Number_notin_pparts [iff]: "Number n ~:pparts H" +by auto + +lemma Agent_notin_pparts [iff]: "Agent A ~:pparts H" +by auto + +lemma pparts_empty [iff]: "pparts {} = {}" +by (auto, erule pparts.induct, auto) + +lemma pparts_insertI [intro]: "X:pparts H ==> X:pparts (insert Y H)" +by (erule pparts.induct, auto) + +lemma pparts_sub: "[| X:pparts G; G<=H |] ==> X:pparts H" +by (erule pparts.induct, auto) + +lemma pparts_insert2 [iff]: "pparts (insert X (insert Y H)) += pparts {X} Un pparts {Y} Un pparts H" +by (rule eq, (erule pparts.induct, auto)+) + +lemma pparts_insert_MPair [iff]: "pparts (insert {|X,Y|} H) += insert {|X,Y|} (pparts ({X,Y} Un H))" +apply (rule eq, (erule pparts.induct, auto)+) +apply (rule_tac Y=Y in pparts.Fst, auto) +apply (erule pparts.induct, auto) +by (rule_tac X=X in pparts.Snd, auto) + +lemma pparts_insert_Nonce [iff]: "pparts (insert (Nonce n) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_Crypt [iff]: "pparts (insert (Crypt K X) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_Key [iff]: "pparts (insert (Key K) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_Agent [iff]: "pparts (insert (Agent A) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_Number [iff]: "pparts (insert (Number n) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_Hash [iff]: "pparts (insert (Hash X) H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert: "X:pparts (insert Y H) ==> X:pparts {Y} Un pparts H" +by (erule pparts.induct, blast+) + +lemma insert_pparts: "X:pparts {Y} Un pparts H ==> X:pparts (insert Y H)" +by (safe, erule pparts.induct, auto) + +lemma pparts_Un [iff]: "pparts (G Un H) = pparts G Un pparts H" +by (rule eq, erule pparts.induct, auto dest: pparts_sub) + +lemma pparts_pparts [iff]: "pparts (pparts H) = pparts H" +by (rule eq, erule pparts.induct, auto) + +lemma pparts_insert_eq: "pparts (insert X H) = pparts {X} Un pparts H" +by (rule_tac A=H in insert_Un, rule pparts_Un) + +lemmas pparts_insert_substI = pparts_insert_eq [THEN ssubst] + +lemma in_pparts: "Y:pparts H ==> EX X. X:H & Y:pparts {X}" +by (erule pparts.induct, auto) + +subsection{*facts about @{term pparts} and @{term parts}*} + +lemma pparts_no_Nonce [dest]: "[| X:pparts {Y}; Nonce n ~:parts {Y} |] +==> Nonce n ~:parts {X}" +by (erule pparts.induct, simp_all) + +subsection{*facts about @{term pparts} and @{term analz}*} + +lemma pparts_analz: "X:pparts H ==> X:analz H" +by (erule pparts.induct, auto) + +lemma pparts_analz_sub: "[| X:pparts G; G<=H |] ==> X:analz H" +by (auto dest: pparts_sub pparts_analz) + +subsection{*messages that contribute to analz*} + +consts kparts :: "msg set => msg set" + +inductive "kparts H" +intros +Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H" +Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H" +Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H" + +subsection{*basic facts about @{term kparts}*} + +lemma kparts_not_MPair [dest]: "X:kparts H ==> not_MPair X" +by (erule kparts.induct, auto) + +lemma kparts_empty [iff]: "kparts {} = {}" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insertI [intro]: "X:kparts H ==> X:kparts (insert Y H)" +by (erule kparts.induct, auto dest: pparts_insertI) + +lemma kparts_insert2 [iff]: "kparts (insert X (insert Y H)) += kparts {X} Un kparts {Y} Un kparts H" +by (rule eq, (erule kparts.induct, auto)+) + +lemma kparts_insert_MPair [iff]: "kparts (insert {|X,Y|} H) += kparts ({X,Y} Un H)" +by (rule eq, (erule kparts.induct, auto)+) + +lemma kparts_insert_Nonce [iff]: "kparts (insert (Nonce n) H) += insert (Nonce n) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_Crypt [iff]: "kparts (insert (Crypt K X) H) += insert (Crypt K X) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_Key [iff]: "kparts (insert (Key K) H) += insert (Key K) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_Agent [iff]: "kparts (insert (Agent A) H) += insert (Agent A) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_Number [iff]: "kparts (insert (Number n) H) += insert (Number n) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_Hash [iff]: "kparts (insert (Hash X) H) += insert (Hash X) (kparts H)" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert: "X:kparts (insert X H) ==> X:kparts {X} Un kparts H" +by (erule kparts.induct, (blast dest: pparts_insert)+) + +lemma kparts_insert_fst [rule_format,dest]: "X:kparts (insert Z H) ==> +X ~:kparts H --> X:kparts {Z}" +by (erule kparts.induct, (blast dest: pparts_insert)+) + +lemma kparts_sub: "[| X:kparts G; G<=H |] ==> X:kparts H" +by (erule kparts.induct, auto dest: pparts_sub) + +lemma kparts_Un [iff]: "kparts (G Un H) = kparts G Un kparts H" +by (rule eq, erule kparts.induct, auto dest: kparts_sub) + +lemma pparts_kparts [iff]: "pparts (kparts H) = {}" +by (rule eq, erule pparts.induct, auto) + +lemma kparts_kparts [iff]: "kparts (kparts H) = kparts H" +by (rule eq, erule kparts.induct, auto) + +lemma kparts_insert_eq: "kparts (insert X H) = kparts {X} Un kparts H" +by (rule_tac A=H in insert_Un, rule kparts_Un) + +lemmas kparts_insert_substI = kparts_insert_eq [THEN ssubst] + +lemma in_kparts: "Y:kparts H ==> EX X. X:H & Y:kparts {X}" +by (erule kparts.induct, auto dest: in_pparts) + +lemma kparts_has_no_pair [iff]: "has_no_pair (kparts H)" +by auto + +subsection{*facts about @{term kparts} and @{term parts}*} + +lemma kparts_no_Nonce [dest]: "[| X:kparts {Y}; Nonce n ~:parts {Y} |] +==> Nonce n ~:parts {X}" +by (erule kparts.induct, auto) + +lemma kparts_parts: "X:kparts H ==> X:parts H" +by (erule kparts.induct, auto dest: pparts_analz) + +lemma parts_kparts: "X:parts (kparts H) ==> X:parts H" +by (erule parts.induct, auto dest: kparts_parts +intro: parts.Fst parts.Snd parts.Body) + +lemma Crypt_kparts_Nonce_parts [dest]: "[| Crypt K Y:kparts {Z}; +Nonce n:parts {Y} |] ==> Nonce n:parts {Z}" +by auto + +subsection{*facts about @{term kparts} and @{term analz}*} + +lemma kparts_analz: "X:kparts H ==> X:analz H" +by (erule kparts.induct, auto dest: pparts_analz) + +lemma kparts_analz_sub: "[| X:kparts G; G<=H |] ==> X:analz H" +by (erule kparts.induct, auto dest: pparts_analz_sub) + +lemma analz_kparts [rule_format,dest]: "X:analz H ==> +Y:kparts {X} --> Y:analz H" +by (erule analz.induct, auto dest: kparts_analz_sub) + +lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H" +by (erule analz.induct, auto dest: kparts_analz) + +lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> +X:analz (kparts {Z} Un kparts H)" +by (rule analz_sub, auto) + +lemma Key_analz_kparts_insert: "Key K:analz (kparts {Z} Un H) +==> Key K:analz (insert Z H)" +apply (subgoal_tac "Key K:analz ({Z} Un H)", simp) +by (rule_tac in_analz_subset_cong, auto dest: analz_kparts_analz) + +lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G) +==> Nonce n:kparts {Y} --> Nonce n:analz G" +by (erule synth.induct, auto) + +lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G); +Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G" +apply (drule parts_insert_substD, clarify) +apply (drule in_sub, drule_tac X=Y in parts_sub, simp) +by (auto dest: Nonce_kparts_synth) + +lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G); +Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G" +apply (drule parts_insert_substD, clarify) +apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp) +apply (ind_cases "Crypt K Y:synth (analz G)") +by (auto dest: Nonce_kparts_synth) + +subsection{*analz is pparts + analz of kparts*} + +lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)" +apply (erule analz.induct) +apply (rule_tac X=X in is_MPairE, blast, blast) +apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast) +by (erule disjE, rule_tac X=Y in is_MPairE, blast+) + +lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)" +by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz) + +lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst] +lemmas analz_pparts_kparts_substD += analz_pparts_kparts_eq [THEN sym, THEN ssubst] + +end diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Extensions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,652 @@ +(****************************************************************************** +date: november 2001 +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 {*Extensions to Standard Theories*} + +theory Extensions = Event: + + +subsection{*Extensions to Theory @{text Set}*} + +lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B" +by auto + +lemma Un_eq: "[| A=A'; B=B' |] ==> A Un B = A' Un B'" +by auto + +lemma insert_absorb_substI: "[| x:A; P (insert x A) |] ==> P A" +by (simp add: insert_absorb) + +lemma insert_Diff_substD: "[| x:A; P A |] ==> P (insert x (A - {x}))" +by (simp add: insert_Diff) + +lemma insert_Diff_substI: "[| x:A; P (insert x (A - {x})) |] ==> P A" +by (simp add: insert_Diff) + +lemma insert_Un: "P ({x} Un A) ==> P (insert x A)" +by simp + +lemma in_sub: "x:A ==> {x}<=A" +by auto + + +subsection{*Extensions to Theory @{text List}*} + +subsubsection{*"minus l x" erase the first element of "l" equal to "x"*} + +consts minus :: "'a list => 'a => 'a list" + +primrec +"minus [] y = []" +"minus (x#xs) y = (if x=y then xs else x # minus xs y)" + +lemma set_minus: "set (minus l x) <= set l" +by (induct l, auto) + +subsection{*Extensions to Theory @{text Message}*} + +subsubsection{*declarations for tactics*} + +declare analz_subset_parts [THEN subsetD, dest] +declare image_eq_UN [simp] +declare parts_insert2 [simp] +declare analz_cut [dest] +declare split_if_asm [split] +declare analz_insertI [intro] +declare Un_Diff [simp] + +subsubsection{*extract the agent number of an Agent message*} + +consts agt_nb :: "msg => agent" + +recdef agt_nb "measure size" +"agt_nb (Agent A) = A" + +subsubsection{*messages that are pairs*} + +constdefs is_MPair :: "msg => bool" +"is_MPair X == EX Y Z. X = {|Y,Z|}" + +declare is_MPair_def [simp] + +lemma MPair_is_MPair [iff]: "is_MPair {|X,Y|}" +by simp + +lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)" +by simp + +lemma Number_isnt_MPair [iff]: "~ is_MPair (Number n)" +by simp + +lemma Key_isnt_MPair [iff]: "~ is_MPair (Key K)" +by simp + +lemma Nonce_isnt_MPair [iff]: "~ is_MPair (Nonce n)" +by simp + +lemma Hash_isnt_MPair [iff]: "~ is_MPair (Hash X)" +by simp + +lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)" +by simp + +syntax not_MPair :: "msg => bool" + +translations "not_MPair X" == "~ is_MPair X" + +lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P" +by auto + +declare is_MPair_def [simp del] + +constdefs has_no_pair :: "msg set => bool" +"has_no_pair H == ALL X Y. {|X,Y|} ~:H" + +declare has_no_pair_def [simp] + +subsubsection{*well-foundedness of messages*} + +lemma wf_Crypt1 [iff]: "Crypt K X ~= X" +by (induct X, auto) + +lemma wf_Crypt2 [iff]: "X ~= Crypt K X" +by (induct X, auto) + +lemma parts_size: "X:parts {Y} ==> X=Y | size X < size Y" +by (erule parts.induct, auto) + +lemma wf_Crypt_parts [iff]: "Crypt K X ~:parts {X}" +by (auto dest: parts_size) + +subsubsection{*lemmas on keysFor*} + +constdefs usekeys :: "msg set => key set" +"usekeys G == {K. EX Y. Crypt K Y:G}" + +lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)" +apply (simp add: keysFor_def) +apply (rule finite_UN_I, auto) +apply (erule finite_induct, auto) +apply (case_tac "EX K X. x = Crypt K X", clarsimp) +apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F} += insert K (usekeys F)", auto simp: usekeys_def) +by (subgoal_tac "{K. EX X. Crypt K X = x | Crypt K X:F} = usekeys F", +auto simp: usekeys_def) + +subsubsection{*lemmas on parts*} + +lemma parts_sub: "[| X:parts G; G<=H |] ==> X:parts H" +by (auto dest: parts_mono) + +lemma parts_Diff [dest]: "X:parts (G - H) ==> X:parts G" +by (erule parts_sub, auto) + +lemma parts_Diff_notin: "[| Y ~:H; Nonce n ~:parts (H - {Y}) |] +==> Nonce n ~:parts H" +by simp + +lemmas parts_insert_substI = parts_insert [THEN ssubst] +lemmas parts_insert_substD = parts_insert [THEN sym, THEN ssubst] + +lemma finite_parts_msg [iff]: "finite (parts {X})" +by (induct X, auto) + +lemma finite_parts [intro]: "finite H ==> finite (parts H)" +apply (erule finite_induct, simp) +by (rule parts_insert_substI, simp) + +lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G" +by (drule_tac x=Y in in_sub, drule parts_mono, auto) + +lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G" +by (auto dest: parts_parts) + +lemma parts_parts_Crypt: "[| Crypt K X:parts G; Nonce n:parts {X} |] +==> Nonce n:parts G" +by (blast intro: parts.Body dest: parts_parts) + +subsubsection{*lemmas on synth*} + +lemma synth_sub: "[| X:synth G; G<=H |] ==> X:synth H" +by (auto dest: synth_mono) + +lemma Crypt_synth [rule_format]: "[| X:synth G; Key K ~:G |] ==> +Crypt K Y:parts {X} --> Crypt K Y:parts G" +by (erule synth.induct, auto dest: parts_sub) + +subsubsection{*lemmas on analz*} + +lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)" +by (subgoal_tac "G <= G Un H", auto dest: analz_mono) + +lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H" +by (auto dest: analz_mono) + +lemma analz_Diff [dest]: "X:analz (G - H) ==> X:analz G" +by (erule analz.induct, auto) + +lemmas in_analz_subset_cong = analz_subset_cong [THEN subsetD] + +lemma analz_eq: "A=A' ==> analz A = analz A'" +by auto + +lemmas insert_commute_substI = insert_commute [THEN ssubst] + +lemma analz_insertD: "[| Crypt K Y:H; Key (invKey K):H |] +==> analz (insert Y H) = analz H" +apply (rule_tac x="Crypt K Y" and P="%H. analz (insert Y H) = analz H" +in insert_absorb_substI, simp) +by (rule_tac insert_commute_substI, simp) + +lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==> +X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)" +by (erule analz.induct, auto) + +lemma analz_needs_only_finite: "X:analz H ==> EX G. G <= H & finite G" +by (erule analz.induct, auto) + +lemma notin_analz_insert: "X ~:analz (insert Y G) ==> X ~:analz G" +by auto + +subsubsection{*lemmas on parts, synth and analz*} + +lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==> +X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H" +by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body) + +lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}" +by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body) + +lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD] + +lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H); +Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H" +apply (drule parts_insert_substD, clarify) +apply (frule in_sub) +apply (frule parts_mono) +by auto + +subsubsection{*greatest nonce used in a message*} + +consts greatest_msg :: "msg => nat" + +recdef greatest_msg "measure size" +"greatest_msg (Nonce n) = n" +"greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)" +"greatest_msg (Crypt K X) = greatest_msg X" +"greatest_msg other = 0" + +lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X" +by (induct X, auto, arith+) + +subsubsection{*sets of keys*} + +constdefs keyset :: "msg set => bool" +"keyset G == ALL X. X:G --> (EX K. X = Key K)" + +lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K" +by (auto simp: keyset_def) + +lemma MPair_notin_keyset [simp]: "keyset G ==> {|X,Y|} ~:G" +by auto + +lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G" +by auto + +lemma Nonce_notin_keyset [simp]: "keyset G ==> Nonce n ~:G" +by auto + +lemma parts_keyset [simp]: "keyset G ==> parts G = G" +by (auto, erule parts.induct, auto) + +subsubsection{*keys a priori necessary for decrypting the messages of G*} + +constdefs keysfor :: "msg set => msg set" +"keysfor G == Key ` keysFor (parts G)" + +lemma keyset_keysfor [iff]: "keyset (keysfor G)" +by (simp add: keyset_def keysfor_def, blast) + +lemma keyset_Diff_keysfor [simp]: "keyset H ==> keyset (H - keysfor G)" +by (auto simp: keyset_def) + +lemma keysfor_Crypt: "Crypt K X:parts G ==> Key (invKey K):keysfor G" +by (auto simp: keysfor_def Crypt_imp_invKey_keysFor) + +lemma no_key_no_Crypt: "Key K ~:keysfor G ==> Crypt (invKey K) X ~:parts G" +by (auto dest: keysfor_Crypt) + +lemma finite_keysfor [intro]: "finite G ==> finite (keysfor G)" +by (auto simp: keysfor_def intro: finite_UN_I) + +subsubsection{*only the keys necessary for G are useful in analz*} + +lemma analz_keyset: "keyset H ==> +analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))" +apply (rule eq) +apply (erule analz.induct, blast) +apply (simp, blast dest: Un_upper1) +apply (simp, blast dest: Un_upper2) +apply (case_tac "Key (invKey K):H - keysfor G", clarsimp) +apply (drule_tac X=X in no_key_no_Crypt) +by (auto intro: analz_sub) + +lemmas analz_keyset_substD = analz_keyset [THEN sym, THEN ssubst] + + +subsection{*Extensions to Theory @{text Event}*} + + +subsubsection{*general protocol properties*} + +constdefs is_Says :: "event => bool" +"is_Says ev == (EX A B X. ev = Says A B X)" + +lemma is_Says_Says [iff]: "is_Says (Says A B X)" +by (simp add: is_Says_def) + +(* one could also require that Gets occurs after Says +but this is sufficient for our purpose *) +constdefs Gets_correct :: "event list set => bool" +"Gets_correct p == ALL evs B X. evs:p --> Gets B X:set evs +--> (EX A. Says A B X:set evs)" + +lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs:p |] +==> EX A. Says A B X:set evs" +apply (simp add: Gets_correct_def) +by (drule_tac x="Gets B X # evs" in spec, auto) + +constdefs one_step :: "event list set => bool" +"one_step p == ALL evs ev. ev#evs:p --> evs:p" + +lemma one_step_Cons [dest]: "[| one_step p; ev#evs:p |] ==> evs:p" +by (unfold one_step_def, blast) + +lemma one_step_app: "[| evs@evs':p; one_step p; []:p |] ==> evs':p" +by (induct evs, auto) + +lemma trunc: "[| evs @ evs':p; one_step p |] ==> evs':p" +by (induct evs, auto) + +constdefs has_only_Says :: "event list set => bool" +"has_only_Says p == ALL evs ev. evs:p --> ev:set evs +--> (EX A B X. ev = Says A B X)" + +lemma has_only_SaysD: "[| ev:set evs; evs:p; has_only_Says p |] +==> EX A B X. ev = Says A B X" +by (unfold has_only_Says_def, blast) + +lemma in_has_only_Says [dest]: "[| has_only_Says p; evs:p; ev:set evs |] +==> EX A B X. ev = Says A B X" +by (auto simp: has_only_Says_def) + +lemma has_only_Says_imp_Gets_correct [simp]: "has_only_Says p +==> Gets_correct p" +by (auto simp: has_only_Says_def Gets_correct_def) + +subsubsection{*lemma on knows*} + +lemma Says_imp_spies2: "Says A B {|X,Y|}:set evs ==> Y:parts (spies evs)" +by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp) + +lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |] +==> Y ~:parts {X}" +by (auto dest: Says_imp_spies parts_parts) + +subsubsection{*knows without initState*} + +consts knows' :: "agent => event list => msg set" + +primrec +"knows' A [] = {}" +"knows' A (ev # evs) = ( + if A = Spy then ( + case ev of + Says A' B X => insert X (knows' A evs) + | Gets A' X => knows' A evs + | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs + ) else ( + case ev of + Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs + | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs + | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs + ))" + +translations "spies" == "knows Spy" + +syntax spies' :: "event list => msg set" + +translations "spies'" == "knows' Spy" + +subsubsection{*decomposition of knows into knows' and initState*} + +lemma knows_decomp: "knows A evs = knows' A evs Un (initState A)" +by (induct evs, auto split: event.split simp: knows.simps) + +lemmas knows_decomp_substI = knows_decomp [THEN ssubst] +lemmas knows_decomp_substD = knows_decomp [THEN sym, THEN ssubst] + +lemma knows'_sub_knows: "knows' A evs <= knows A evs" +by (auto simp: knows_decomp) + +lemma knows'_Cons: "knows' A (ev#evs) = knows' A [ev] Un knows' A evs" +by (induct ev, auto) + +lemmas knows'_Cons_substI = knows'_Cons [THEN ssubst] +lemmas knows'_Cons_substD = knows'_Cons [THEN sym, THEN ssubst] + +lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev] +Un knows A evs" +apply (simp only: knows_decomp) +apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans) +by (rule Un_eq, rule knows'_Cons, simp, blast) + +lemmas knows_Cons_substI = knows_Cons [THEN ssubst] +lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst] + +lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |] +==> knows' A evs <= spies' evs" +by (induct evs, auto split: event.splits) + +subsubsection{*knows' is finite*} + +lemma finite_knows' [iff]: "finite (knows' A evs)" +by (induct evs, auto split: event.split simp: knows.simps) + +subsubsection{*monotonicity of knows*} + +lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)" +by (cases A, (induct evs, (induct ev, auto simp: knows.simps)+)) + +lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)" +by (auto dest: knows_sub_Cons [THEN subsetD]) + +lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')" +apply (induct evs, auto) +apply (simp add: knows_decomp) +by (case_tac a, auto simp: knows.simps) + +subsubsection{*maximum knowledge an agent can have +includes messages sent to the agent*} + +consts knows_max' :: "agent => event list => msg set" + +primrec +knows_max'_def_Nil: "knows_max' A [] = {}" +knows_max'_def_Cons: "knows_max' A (ev # evs) = ( + if A=Spy then ( + case ev of + Says A' B X => insert X (knows_max' A evs) + | Gets A' X => knows_max' A evs + | Notes A' X => + if A':bad then insert X (knows_max' A evs) else knows_max' A evs + ) else ( + case ev of + Says A' B X => + if A=A' | A=B then insert X (knows_max' A evs) else knows_max' A evs + | Gets A' X => + if A=A' then insert X (knows_max' A evs) else knows_max' A evs + | Notes A' X => + if A=A' then insert X (knows_max' A evs) else knows_max' A evs + ))" + +constdefs knows_max :: "agent => event list => msg set" +"knows_max A evs == knows_max' A evs Un initState A" + +consts spies_max :: "event list => msg set" + +translations "spies_max evs" == "knows_max Spy evs" + +subsubsection{*basic facts about @{term knows_max}*} + +lemma spies_max_spies [iff]: "spies_max evs = spies evs" +by (induct evs, auto simp: knows_max_def split: event.splits) + +lemma knows_max'_Cons: "knows_max' A (ev#evs) += knows_max' A [ev] Un knows_max' A evs" +by (auto split: event.splits) + +lemmas knows_max'_Cons_substI = knows_max'_Cons [THEN ssubst] +lemmas knows_max'_Cons_substD = knows_max'_Cons [THEN sym, THEN ssubst] + +lemma knows_max_Cons: "knows_max A (ev#evs) += knows_max' A [ev] Un knows_max A evs" +apply (simp add: knows_max_def del: knows_max'_def_Cons) +apply (rule_tac evs1=evs in knows_max'_Cons_substI) +by blast + +lemmas knows_max_Cons_substI = knows_max_Cons [THEN ssubst] +lemmas knows_max_Cons_substD = knows_max_Cons [THEN sym, THEN ssubst] + +lemma finite_knows_max' [iff]: "finite (knows_max' A evs)" +by (induct evs, auto split: event.split) + +lemma knows_max'_sub_spies': "[| evs:p; has_only_Says p; one_step p |] +==> knows_max' A evs <= spies' evs" +by (induct evs, auto split: event.splits) + +lemma knows_max'_in_spies' [dest]: "[| evs:p; X:knows_max' A evs; +has_only_Says p; one_step p |] ==> X:spies' evs" +by (rule knows_max'_sub_spies' [THEN subsetD], auto) + +lemma knows_max'_app: "knows_max' A (evs @ evs') += knows_max' A evs Un knows_max' A evs'" +by (induct evs, auto split: event.splits) + +lemma Says_to_knows_max': "Says A B X:set evs ==> X:knows_max' B evs" +by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app) + +lemma Says_from_knows_max': "Says A B X:set evs ==> X:knows_max' A evs" +by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app) + +subsubsection{*used without initState*} + +consts used' :: "event list => msg set" + +primrec +"used' [] = {}" +"used' (ev # evs) = ( + case ev of + Says A B X => parts {X} Un used' evs + | Gets A X => used' evs + | Notes A X => parts {X} Un used' evs + )" + +constdefs init :: "msg set" +"init == used []" + +lemma used_decomp: "used evs = init Un used' evs" +by (induct evs, auto simp: init_def split: event.split) + +lemma used'_sub_app: "used' evs <= used' (evs@evs')" +by (induct evs, auto split: event.split) + +lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs" +apply (induct evs, simp) +apply (case_tac a, simp_all) +apply (blast dest: parts_trans)+; +done + +subsubsection{*monotonicity of used*} + +lemma used_sub_Cons: "used evs <= used (ev#evs)" +by (induct evs, (induct ev, auto)+) + +lemma used_ConsI: "X:used evs ==> X:used (ev#evs)" +by (auto dest: used_sub_Cons [THEN subsetD]) + +lemma notin_used_ConsD: "X ~:used (ev#evs) ==> X ~:used evs" +by (auto dest: used_sub_Cons [THEN subsetD]) + +lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'" +by (induct evs, auto, case_tac a, auto) + +lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs" +by (case_tac ev, auto) + +lemma used_sub_app: "used evs <= used (evs@evs')" +by (auto simp: used_decomp dest: used'_sub_app [THEN subsetD]) + +lemma used_appIL: "X:used evs ==> X:used (evs' @ evs)" +by (induct evs', auto intro: used_ConsI) + +lemma used_appIR: "X:used evs ==> X:used (evs @ evs')" +by (erule used_sub_app [THEN subsetD]) + +lemma used_parts: "[| X:parts {Y}; Y:used evs |] ==> X:used evs" +apply (auto simp: used_decomp dest: used'_parts) +by (auto simp: init_def used_Nil dest: parts_trans) + +lemma parts_Says_used: "[| Says A B X:set evs; Y:parts {X} |] ==> Y:used evs" +by (induct evs, simp_all, safe, auto intro: used_ConsI) + +lemma parts_used_app: "X:parts {Y} ==> X:used (evs @ Says A B Y # evs')" +apply (drule_tac evs="[Says A B Y]" in used_parts, simp, blast) +apply (drule_tac evs'=evs' in used_appIR) +apply (drule_tac evs'=evs in used_appIL) +by simp + +subsubsection{*lemmas on used and knows*} + +lemma initState_used: "X:parts (initState A) ==> X:used evs" +by (induct evs, auto simp: used.simps split: event.split) + +lemma Says_imp_used: "Says A B X:set evs ==> parts {X} <= used evs" +by (induct evs, auto intro: used_ConsI) + +lemma not_used_not_spied: "X ~:used evs ==> X ~:parts (spies evs)" +by (induct evs, auto simp: used_Nil) + +lemma not_used_not_parts: "[| Y ~:used evs; Says A B X:set evs |] +==> Y ~:parts {X}" +by (induct evs, auto intro: used_ConsI) + +lemma not_used_parts_false: "[| X ~:used evs; Y:parts (spies evs) |] +==> X ~:parts {Y}" +by (auto dest: parts_parts) + +lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |] +==> X:parts (knows A evs) --> X:used evs" +apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used) +apply (induct evs) +apply (simp add: used.simps, blast) +apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify) +apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe) +apply (erule initState_used) +apply (case_tac a, auto) +apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says) +by (auto dest: Says_imp_used intro: used_ConsI) + +lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |] +==> X:parts (knows_max A evs) --> X:used evs" +apply (case_tac "A=Spy") +apply (simp, blast dest: parts_knows_Spy_subset_used) +apply (induct evs) +apply (simp add: knows_max_def used.simps, blast) +apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify) +apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe) +apply (case_tac a, auto) +apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says) +by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI) + +lemma not_used_not_known: "[| evs:p; X ~:used evs; +Gets_correct p; one_step p |] ==> X ~:parts (knows A evs)" +by (case_tac "A=Spy", auto dest: not_used_not_spied known_used) + +lemma not_used_not_known_max: "[| evs:p; X ~:used evs; +Gets_correct p; one_step p |] ==> X ~:parts (knows_max A evs)" +by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used) + +subsubsection{*a nonce or key in a message cannot equal a fresh nonce or key*} + +lemma Nonce_neq [dest]: "[| Nonce n' ~:used evs; +Says A B X:set evs; Nonce n:parts {X} |] ==> n ~= n'" +by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub) + +lemma Key_neq [dest]: "[| Key n' ~:used evs; +Says A B X:set evs; Key n:parts {X} |] ==> n ~= n'" +by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub) + +subsubsection{*message of an event*} + +consts msg :: "event => msg" + +recdef msg "measure size" +"msg (Says A B X) = X" +"msg (Gets A X) = X" +"msg (Notes A X) = X" + +lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs" +by (induct ev, auto) + + + +end diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Guard.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,312 @@ +(****************************************************************************** +date: january 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{*Protocol-Independent Confidentiality Theorem on Nonces*} + +theory Guard = Analz + Extensions: + +(****************************************************************************** +messages where all the occurrences of Nonce n are +in a sub-message of the form Crypt (invKey K) X with K:Ks +******************************************************************************) + +consts guard :: "nat => key set => msg set" + +inductive "guard n Ks" +intros +No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks" +Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks" +Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks" +Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> {|X,Y|}:guard n Ks" + +subsection{*basic facts about @{term guard}*} + +lemma Key_is_guard [iff]: "Key K:guard n Ks" +by auto + +lemma Agent_is_guard [iff]: "Agent A:guard n Ks" +by auto + +lemma Number_is_guard [iff]: "Number r:guard n Ks" +by auto + +lemma Nonce_notin_guard: "X:guard n Ks ==> X ~= Nonce n" +by (erule guard.induct, auto) + +lemma Nonce_notin_guard_iff [iff]: "Nonce n ~:guard n Ks" +by (auto dest: Nonce_notin_guard) + +lemma guard_has_Crypt [rule_format]: "X:guard n Ks ==> Nonce n:parts {X} +--> (EX K Y. Crypt K Y:kparts {X} & Nonce n:parts {Y})" +by (erule guard.induct, auto) + +lemma Nonce_notin_kparts_msg: "X:guard n Ks ==> Nonce n ~:kparts {X}" +by (erule guard.induct, auto) + +lemma Nonce_in_kparts_imp_no_guard: "Nonce n:kparts H +==> EX X. X:H & X ~:guard n Ks" +apply (drule in_kparts, clarify) +apply (rule_tac x=X in exI, clarify) +by (auto dest: Nonce_notin_kparts_msg) + +lemma guard_kparts [rule_format]: "X:guard n Ks ==> +Y:kparts {X} --> Y:guard n Ks" +by (erule guard.induct, auto) + +lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks" +by (ind_cases "Crypt K Y:guard n Ks", auto) + +lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)" +by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+) + +lemma guard_not_guard [rule_format]: "X:guard n Ks ==> +Crypt K Y:kparts {X} --> Nonce n:kparts {Y} --> Y ~:guard n Ks" +by (erule guard.induct, auto dest: guard_kparts) + +lemma guard_extand: "[| X:guard n Ks; Ks <= Ks' |] ==> X:guard n Ks'" +by (erule guard.induct, auto) + +subsection{*guarded sets*} + +constdefs Guard :: "nat => key set => msg set => bool" +"Guard n Ks H == ALL X. X:H --> X:guard n Ks" + +subsection{*basic facts about @{term Guard}*} + +lemma Guard_empty [iff]: "Guard n Ks {}" +by (simp add: Guard_def) + +lemma notin_parts_Guard [intro]: "Nonce n ~:parts G ==> Guard n Ks G" +apply (unfold Guard_def, clarify) +apply (subgoal_tac "Nonce n ~:parts {X}") +by (auto dest: parts_sub) + +lemma Nonce_notin_kparts [simplified]: "Guard n Ks H ==> Nonce n ~:kparts H" +by (auto simp: Guard_def dest: in_kparts Nonce_notin_kparts_msg) + +lemma Guard_must_decrypt: "[| Guard n Ks H; Nonce n:analz H |] ==> +EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H" +apply (drule_tac P="%G. Nonce n:G" in analz_pparts_kparts_substD, simp) +by (drule must_decrypt, auto dest: Nonce_notin_kparts) + +lemma Guard_kparts [intro]: "Guard n Ks H ==> Guard n Ks (kparts H)" +by (auto simp: Guard_def dest: in_kparts guard_kparts) + +lemma Guard_mono: "[| Guard n Ks H; G <= H |] ==> Guard n Ks G" +by (auto simp: Guard_def) + +lemma Guard_insert [iff]: "Guard n Ks (insert X H) += (Guard n Ks H & X:guard n Ks)" +by (auto simp: Guard_def) + +lemma Guard_Un [iff]: "Guard n Ks (G Un H) = (Guard n Ks G & Guard n Ks H)" +by (auto simp: Guard_def) + +lemma Guard_synth [intro]: "Guard n Ks G ==> Guard n Ks (synth G)" +by (auto simp: Guard_def, erule synth.induct, auto) + +lemma Guard_analz [intro]: "[| Guard n Ks G; ALL K. K:Ks --> Key K ~:analz G |] +==> Guard n Ks (analz G)" +apply (auto simp: Guard_def) +apply (erule analz.induct, auto) +by (ind_cases "Crypt K Xa:guard n Ks", auto) + +lemma in_Guard [dest]: "[| X:G; Guard n Ks G |] ==> X:guard n Ks" +by (auto simp: Guard_def) + +lemma in_synth_Guard: "[| X:synth G; Guard n Ks G |] ==> X:guard n Ks" +by (drule Guard_synth, auto) + +lemma in_analz_Guard: "[| X:analz G; Guard n Ks G; +ALL K. K:Ks --> Key K ~:analz G |] ==> X:guard n Ks" +by (drule Guard_analz, auto) + +lemma Guard_keyset [simp]: "keyset G ==> Guard n Ks G" +by (auto simp: Guard_def) + +lemma Guard_Un_keyset: "[| Guard n Ks G; keyset H |] ==> Guard n Ks (G Un H)" +by auto + +lemma in_Guard_kparts: "[| X:G; Guard n Ks G; Y:kparts {X} |] ==> Y:guard n Ks" +by blast + +lemma in_Guard_kparts_neq: "[| X:G; Guard n Ks G; Nonce n':kparts {X} |] +==> n ~= n'" +by (blast dest: in_Guard_kparts) + +lemma in_Guard_kparts_Crypt: "[| X:G; Guard n Ks G; is_MPair X; +Crypt K Y:kparts {X}; Nonce n:kparts {Y} |] ==> invKey K:Ks" +apply (drule in_Guard, simp) +apply (frule guard_not_guard, simp+) +apply (drule guard_kparts, simp) +by (ind_cases "Crypt K Y:guard n Ks", auto) + +lemma Guard_extand: "[| Guard n Ks G; Ks <= Ks' |] ==> Guard n Ks' G" +by (auto simp: Guard_def dest: guard_extand) + +lemma guard_invKey [rule_format]: "[| X:guard n Ks; Nonce n:kparts {Y} |] ==> +Crypt K Y:kparts {X} --> invKey K:Ks" +by (erule guard.induct, auto) + +lemma Crypt_guard_invKey [rule_format]: "[| Crypt K Y:guard n Ks; +Nonce n:kparts {Y} |] ==> invKey K:Ks" +by (auto dest: guard_invKey) + +subsection{*set obtained by decrypting a message*} + +syntax decrypt :: "msg set => key => msg => msg set" + +translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})" + +lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |] +==> Nonce n:analz (decrypt H K Y)" +by (drule_tac P="%H. Nonce n:analz H" in insert_Diff_substD, simp_all) + +lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)" +by auto + +lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H" +by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body) + +subsection{*number of Crypt's in a message*} + +consts crypt_nb :: "msg => nat" + +recdef crypt_nb "measure size" +"crypt_nb (Crypt K X) = Suc (crypt_nb X)" +"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" +"crypt_nb X = 0" (* otherwise *) + +subsection{*basic facts about @{term crypt_nb}*} + +lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X" +by (induct X, simp_all, safe, simp_all) + +subsection{*number of Crypt's in a message list*} + +consts cnb :: "msg list => nat" + +recdef cnb "measure size" +"cnb [] = 0" +"cnb (X#l) = crypt_nb X + cnb l" + +subsection{*basic facts about @{term cnb}*} + +lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" +by (induct l, auto) + +lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" +by (induct l, auto) + +lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] + +lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x" +apply (induct l, auto) +by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp) + +lemma parts_cnb: "Z:parts (set l) ==> +cnb l = (cnb l - crypt_nb Z) + crypt_nb Z" +by (erule parts.induct, auto simp: in_set_conv_decomp) + +lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l" +by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD) + +subsection{*list of kparts*} + +lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X" +apply (induct X, simp_all) +apply (rule_tac x="[Agent agent]" in exI, simp) +apply (rule_tac x="[Number nat]" in exI, simp) +apply (rule_tac x="[Nonce nat]" in exI, simp) +apply (rule_tac x="[Key nat]" in exI, simp) +apply (rule_tac x="[Hash msg]" in exI, simp) +apply (clarify, rule_tac x="l@la" in exI, simp) +by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp) + +lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l" +apply (induct l) +apply (rule_tac x="[]" in exI, simp, clarsimp) +apply (subgoal_tac "EX l. kparts {a} = set l & cnb l = crypt_nb a", clarify) +apply (rule_tac x="l@l'" in exI, simp) +apply (rule kparts_insert_substI, simp) +by (rule kparts_msg_set) + +subsection{*list corresponding to "decrypt"*} + +constdefs decrypt' :: "msg list => key => msg => msg list" +"decrypt' l K Y == Y # minus l (Crypt K Y)" + +declare decrypt'_def [simp] + +subsection{*basic facts about @{term decrypt'}*} + +lemma decrypt_minus: "decrypt (set l) K Y <= set (decrypt' l K Y)" +by (induct l, auto) + +subsection{*if the analyse of a finite guarded set gives n then it must also gives +one of the keys of Ks*} + +lemma Guard_invKey_by_list [rule_format]: "ALL l. cnb l = p +--> Guard n Ks (set l) --> Nonce n:analz (set l) +--> (EX K. K:Ks & Key K:analz (set l))" +apply (induct p) +(* case p=0 *) +apply (clarify, drule Guard_must_decrypt, simp, clarify) +apply (drule kparts_parts, drule non_empty_crypt, simp) +(* case p>0 *) +apply (clarify, frule Guard_must_decrypt, simp, clarify) +apply (drule_tac P="%G. Nonce n:G" in analz_pparts_kparts_substD, simp) +apply (frule analz_decrypt, simp_all) +apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp) +apply (drule_tac G="insert Y (set l' - {Crypt K Y})" +and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus) +apply (rule_tac analz_pparts_kparts_substI, simp) +apply (case_tac "K:invKey`Ks") +(* K:invKey`Ks *) +apply (clarsimp, blast) +(* K ~:invKey`Ks *) +apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))") +apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq) +apply (subgoal_tac "Crypt K Y:parts (set l)") +apply (drule parts_cnb, rotate_tac -1, simp) +apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) +apply (rule insert_mono, rule set_minus) +apply (simp add: analz_insertD, blast) +(* Crypt K Y:parts (set l) *) +apply (blast dest: kparts_parts) +(* Guard n Ks (set (decrypt' l' K Y)) *) +apply (rule_tac H="insert Y (set l')" in Guard_mono) +apply (subgoal_tac "Guard n Ks (set l')", simp) +apply (rule_tac K=K in guard_Crypt, simp add: Guard_def, simp) +apply (drule_tac t="set l'" in sym, simp) +apply (rule Guard_kparts, simp, simp) +apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast) +by (rule kparts_set) + +lemma Guard_invKey_finite: "[| Nonce n:analz G; Guard n Ks G; finite G |] +==> EX K. K:Ks & Key K:analz G" +apply (drule finite_list, clarify) +by (rule Guard_invKey_by_list, auto) + +lemma Guard_invKey: "[| Nonce n:analz G; Guard n Ks G |] +==> EX K. K:Ks & Key K:analz G" +by (auto dest: analz_needs_only_finite Guard_invKey_finite) + +subsection{*if the analyse of a finite guarded set and a (possibly infinite) set of keys +gives n then it must also gives Ks*} + +lemma Guard_invKey_keyset: "[| Nonce n:analz (G Un H); Guard n Ks G; finite G; +keyset H |] ==> EX K. K:Ks & Key K:analz (G Un H)" +apply (frule_tac P="%G. Nonce n:G" and G2=G in analz_keyset_substD, simp_all) +apply (drule_tac G="G Un (H Int keysfor G)" in Guard_invKey_finite) +by (auto simp: Guard_def intro: analz_sub) + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/GuardK.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/GuardK.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,309 @@ +(****************************************************************************** +very similar to Guard except: +- Guard is replaced by GuardK, guard by guardK, Nonce by Key +- some scripts are slightly modified (+ keyset_in, kparts_parts) +- the hypothesis Key n ~:G (keyset G) is added + +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{*protocol-independent confidentiality theorem on keys*} + +theory GuardK = Analz + Extensions: + +(****************************************************************************** +messages where all the occurrences of Key n are +in a sub-message of the form Crypt (invKey K) X with K:Ks +******************************************************************************) + +consts guardK :: "nat => key set => msg set" + +inductive "guardK n Ks" +intros +No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks" +Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks" +Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks" +Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks" + +subsection{*basic facts about @{term guardK}*} + +lemma Nonce_is_guardK [iff]: "Nonce p:guardK n Ks" +by auto + +lemma Agent_is_guardK [iff]: "Agent A:guardK n Ks" +by auto + +lemma Number_is_guardK [iff]: "Number r:guardK n Ks" +by auto + +lemma Key_notin_guardK: "X:guardK n Ks ==> X ~= Key n" +by (erule guardK.induct, auto) + +lemma Key_notin_guardK_iff [iff]: "Key n ~:guardK n Ks" +by (auto dest: Key_notin_guardK) + +lemma guardK_has_Crypt [rule_format]: "X:guardK n Ks ==> Key n:parts {X} +--> (EX K Y. Crypt K Y:kparts {X} & Key n:parts {Y})" +by (erule guardK.induct, auto) + +lemma Key_notin_kparts_msg: "X:guardK n Ks ==> Key n ~:kparts {X}" +by (erule guardK.induct, auto dest: kparts_parts) + +lemma Key_in_kparts_imp_no_guardK: "Key n:kparts H +==> EX X. X:H & X ~:guardK n Ks" +apply (drule in_kparts, clarify) +apply (rule_tac x=X in exI, clarify) +by (auto dest: Key_notin_kparts_msg) + +lemma guardK_kparts [rule_format]: "X:guardK n Ks ==> +Y:kparts {X} --> Y:guardK n Ks" +by (erule guardK.induct, auto dest: kparts_parts parts_sub) + +lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks" +by (ind_cases "Crypt K Y:guardK n Ks", auto) + +lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks) += (X:guardK n Ks & Y:guardK n Ks)" +by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+) + +lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==> +Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks" +by (erule guardK.induct, auto dest: guardK_kparts) + +lemma guardK_extand: "[| X:guardK n Ks; Ks <= Ks'; +[| K:Ks'; K ~:Ks |] ==> Key K ~:parts {X} |] ==> X:guardK n Ks'" +by (erule guardK.induct, auto) + +subsection{*guarded sets*} + +constdefs GuardK :: "nat => key set => msg set => bool" +"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks" + +subsection{*basic facts about @{term GuardK}*} + +lemma GuardK_empty [iff]: "GuardK n Ks {}" +by (simp add: GuardK_def) + +lemma Key_notin_kparts [simplified]: "GuardK n Ks H ==> Key n ~:kparts H" +by (auto simp: GuardK_def dest: in_kparts Key_notin_kparts_msg) + +lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n:analz H |] ==> +EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H" +apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp) +by (drule must_decrypt, auto dest: Key_notin_kparts) + +lemma GuardK_kparts [intro]: "GuardK n Ks H ==> GuardK n Ks (kparts H)" +by (auto simp: GuardK_def dest: in_kparts guardK_kparts) + +lemma GuardK_mono: "[| GuardK n Ks H; G <= H |] ==> GuardK n Ks G" +by (auto simp: GuardK_def) + +lemma GuardK_insert [iff]: "GuardK n Ks (insert X H) += (GuardK n Ks H & X:guardK n Ks)" +by (auto simp: GuardK_def) + +lemma GuardK_Un [iff]: "GuardK n Ks (G Un H) = (GuardK n Ks G & GuardK n Ks H)" +by (auto simp: GuardK_def) + +lemma GuardK_synth [intro]: "GuardK n Ks G ==> GuardK n Ks (synth G)" +by (auto simp: GuardK_def, erule synth.induct, auto) + +lemma GuardK_analz [intro]: "[| GuardK n Ks G; ALL K. K:Ks --> Key K ~:analz G |] +==> GuardK n Ks (analz G)" +apply (auto simp: GuardK_def) +apply (erule analz.induct, auto) +by (ind_cases "Crypt K Xa:guardK n Ks", auto) + +lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks" +by (auto simp: GuardK_def) + +lemma in_synth_GuardK: "[| X:synth G; GuardK n Ks G |] ==> X:guardK n Ks" +by (drule GuardK_synth, auto) + +lemma in_analz_GuardK: "[| X:analz G; GuardK n Ks G; +ALL K. K:Ks --> Key K ~:analz G |] ==> X:guardK n Ks" +by (drule GuardK_analz, auto) + +lemma GuardK_keyset [simp]: "[| keyset G; Key n ~:G |] ==> GuardK n Ks G" +by (simp only: GuardK_def, clarify, drule keyset_in, auto) + +lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n ~:H |] +==> GuardK n Ks (G Un H)" +by auto + +lemma in_GuardK_kparts: "[| X:G; GuardK n Ks G; Y:kparts {X} |] ==> Y:guardK n Ks" +by blast + +lemma in_GuardK_kparts_neq: "[| X:G; GuardK n Ks G; Key n':kparts {X} |] +==> n ~= n'" +by (blast dest: in_GuardK_kparts) + +lemma in_GuardK_kparts_Crypt: "[| X:G; GuardK n Ks G; is_MPair X; +Crypt K Y:kparts {X}; Key n:kparts {Y} |] ==> invKey K:Ks" +apply (drule in_GuardK, simp) +apply (frule guardK_not_guardK, simp+) +apply (drule guardK_kparts, simp) +by (ind_cases "Crypt K Y:guardK n Ks", auto) + +lemma GuardK_extand: "[| GuardK n Ks G; Ks <= Ks'; +[| K:Ks'; K ~:Ks |] ==> Key K ~:parts G |] ==> GuardK n Ks' G" +by (auto simp: GuardK_def dest: guardK_extand parts_sub) + +subsection{*set obtained by decrypting a message*} + +syntax decrypt :: "msg set => key => msg => msg set" + +translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})" + +lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |] +==> Key n:analz (decrypt H K Y)" +by (drule_tac P="%H. Key n:analz H" in insert_Diff_substD, simp_all) + +lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)" +by auto + +lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H" +by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body) + +subsection{*number of Crypt's in a message*} + +consts crypt_nb :: "msg => nat" + +recdef crypt_nb "measure size" +"crypt_nb (Crypt K X) = Suc (crypt_nb X)" +"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" +"crypt_nb X = 0" (* otherwise *) + +subsection{*basic facts about @{term crypt_nb}*} + +lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X" +by (induct X, simp_all, safe, simp_all) + +subsection{*number of Crypt's in a message list*} + +consts cnb :: "msg list => nat" + +recdef cnb "measure size" +"cnb [] = 0" +"cnb (X#l) = crypt_nb X + cnb l" + +subsection{*basic facts about @{term cnb}*} + +lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" +by (induct l, auto) + +lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" +by (induct l, auto) + +lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] + +lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x" +apply (induct l, auto) +by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp) + +lemma parts_cnb: "Z:parts (set l) ==> +cnb l = (cnb l - crypt_nb Z) + crypt_nb Z" +by (erule parts.induct, auto simp: in_set_conv_decomp) + +lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l" +by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD) + +subsection{*list of kparts*} + +lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X" +apply (induct X, simp_all) +apply (rule_tac x="[Agent agent]" in exI, simp) +apply (rule_tac x="[Number nat]" in exI, simp) +apply (rule_tac x="[Nonce nat]" in exI, simp) +apply (rule_tac x="[Key nat]" in exI, simp) +apply (rule_tac x="[Hash msg]" in exI, simp) +apply (clarify, rule_tac x="l@la" in exI, simp) +by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp) + +lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l" +apply (induct l) +apply (rule_tac x="[]" in exI, simp, clarsimp) +apply (subgoal_tac "EX l. kparts {a} = set l & cnb l = crypt_nb a", clarify) +apply (rule_tac x="l@l'" in exI, simp) +apply (rule kparts_insert_substI, simp) +by (rule kparts_msg_set) + +subsection{*list corresponding to "decrypt"*} + +constdefs decrypt' :: "msg list => key => msg => msg list" +"decrypt' l K Y == Y # minus l (Crypt K Y)" + +declare decrypt'_def [simp] + +subsection{*basic facts about @{term decrypt'}*} + +lemma decrypt_minus: "decrypt (set l) K Y <= set (decrypt' l K Y)" +by (induct l, auto) + +text{*if the analysis of a finite guarded set gives n then it must also give +one of the keys of Ks*} + +lemma GuardK_invKey_by_list [rule_format]: "ALL l. cnb l = p +--> GuardK n Ks (set l) --> Key n:analz (set l) +--> (EX K. K:Ks & Key K:analz (set l))" +apply (induct p) +(* case p=0 *) +apply (clarify, drule GuardK_must_decrypt, simp, clarify) +apply (drule kparts_parts, drule non_empty_crypt, simp) +(* case p>0 *) +apply (clarify, frule GuardK_must_decrypt, simp, clarify) +apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp) +apply (frule analz_decrypt, simp_all) +apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp) +apply (drule_tac G="insert Y (set l' - {Crypt K Y})" +and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus) +apply (rule_tac analz_pparts_kparts_substI, simp) +apply (case_tac "K:invKey`Ks") +(* K:invKey`Ks *) +apply (clarsimp, blast) +(* K ~:invKey`Ks *) +apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))") +apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq) +apply (subgoal_tac "Crypt K Y:parts (set l)") +apply (drule parts_cnb, rotate_tac -1, simp) +apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) +apply (rule insert_mono, rule set_minus) +apply (simp add: analz_insertD, blast) +(* Crypt K Y:parts (set l) *) +apply (blast dest: kparts_parts) +(* GuardK n Ks (set (decrypt' l' K Y)) *) +apply (rule_tac H="insert Y (set l')" in GuardK_mono) +apply (subgoal_tac "GuardK n Ks (set l')", simp) +apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp) +apply (drule_tac t="set l'" in sym, simp) +apply (rule GuardK_kparts, simp, simp) +apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast) +by (rule kparts_set) + +lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |] +==> EX K. K:Ks & Key K:analz G" +apply (drule finite_list, clarify) +by (rule GuardK_invKey_by_list, auto) + +lemma GuardK_invKey: "[| Key n:analz G; GuardK n Ks G |] +==> EX K. K:Ks & Key K:analz G" +by (auto dest: analz_needs_only_finite GuardK_invKey_finite) + +text{*if the analyse of a finite guarded set and a (possibly infinite) set of +keys gives n then it must also gives Ks*} + +lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G; +keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)" +apply (frule_tac P="%G. Key n:G" and G2=G in analz_keyset_substD, simp_all) +apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite) +apply (auto simp: GuardK_def intro: analz_sub) +by (drule keyset_in, auto) + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Guard_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard_Public.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,174 @@ +(****************************************************************************** +lemmas on guarded messages for public protocols + +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 +******************************************************************************) + +theory Guard_Public = Guard + Public + Extensions: + +subsection{*Extensions to Theory @{text Public}*} + +declare initState.simps [simp del] + +subsubsection{*signature*} + +constdefs sign :: "agent => msg => msg" +"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}" + +lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" +by (auto simp: sign_def) + +subsubsection{*agent associated to a key*} + +constdefs agt :: "key => agent" +"agt K == @A. K = priK A | K = pubK A" + +lemma agt_priK [simp]: "agt (priK A) = A" +by (simp add: agt_def) + +lemma agt_pubK [simp]: "agt (pubK A) = A" +by (simp add: agt_def) + +subsubsection{*basic facts about @{term initState}*} + +lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)" +by (cases A, auto simp: initState.simps) + +lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)" +by auto + +lemma no_priK_in_analz_init [simp]: "A ~:bad +==> Key (priK A) ~:analz (initState Spy)" +by (auto simp: initState.simps) + +lemma priK_notin_initState_Friend [simp]: "A ~= Friend C +==> Key (priK A) ~: parts (initState (Friend C))" +by (auto simp: initState.simps) + +lemma keyset_init [iff]: "keyset (initState A)" +by (cases A, auto simp: keyset_def initState.simps) + +subsubsection{*sets of private keys*} + +constdefs priK_set :: "key set => bool" +"priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)" + +lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A" +by (simp add: priK_set_def) + +lemma priK_set1 [iff]: "priK_set {priK A}" +by (simp add: priK_set_def) + +lemma priK_set2 [iff]: "priK_set {priK A, priK B}" +by (simp add: priK_set_def) + +subsubsection{*sets of good keys*} + +constdefs good :: "key set => bool" +"good Ks == ALL K. K:Ks --> agt K ~:bad" + +lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad" +by (simp add: good_def) + +lemma good1 [simp]: "A ~:bad ==> good {priK A}" +by (simp add: good_def) + +lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}" +by (simp add: good_def) + +subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*} + +consts greatest :: "event list => nat" + +recdef greatest "measure size" +"greatest [] = 0" +"greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)" + +lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs" +apply (induct evs, auto simp: initState.simps) +apply (drule used_sub_parts_used, safe) +apply (drule greatest_msg_is_greatest, arith) +by (simp, arith) + +subsubsection{*function giving a new nonce*} + +constdefs new :: "event list => nat" +"new evs == Suc (greatest evs)" + +lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs" +by (clarify, drule greatest_is_greatest, auto simp: new_def) + +subsection{*Proofs About Guarded Messages*} + +subsubsection{*small hack necessary because priK is defined as the inverse of pubK*} + +lemma pubK_is_invKey_priK: "pubK A = invKey (priK A)" +by simp + +lemmas pubK_is_invKey_priK_substI = pubK_is_invKey_priK [THEN ssubst] + +lemmas invKey_invKey_substI = invKey [THEN ssubst] + +lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}" +apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI) +by (rule Guard_Nonce, simp+) + +subsubsection{*guardedness results*} + +lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks" +by (auto simp: sign_def) + +lemma Guard_init [iff]: "Guard n Ks (initState B)" +by (induct B, auto simp: Guard_def initState.simps) + +lemma Guard_knows_max': "Guard n Ks (knows_max' C evs) +==> Guard n Ks (knows_max C evs)" +by (simp add: knows_max_def) + +lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs +==> Guard n Ks (spies evs)" +by (auto simp: Guard_def dest: not_used_not_known parts_sub) + +lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)" +by (auto simp: Guard_def dest: known_used parts_trans) + +lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)" +by (auto simp: Guard_def dest: known_max_used parts_trans) + +lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)" +apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono) +by (auto simp: knows_max_def) + +subsubsection{*regular protocols*} + +constdefs regular :: "event list set => bool" +"regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)" + +lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==> +(Key (priK A):parts (spies evs)) = (A:bad)" +by (auto simp: regular_def) + +lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==> +(Key (priK A):analz (spies evs)) = (A:bad)" +by auto + +lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p; +priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)" +apply (clarify, simp only: knows_decomp) +apply (drule Guard_invKey_keyset, simp+, safe) +apply (drule in_good, simp) +apply (drule in_priK_set, simp+, clarify) +apply (frule_tac A=A in priK_analz_iff_bad) +by (simp add: knows_decomp)+ + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Guard_Shared.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,187 @@ +(****************************************************************************** +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{*lemmas on guarded messages for protocols with symmetric keys*} + +theory Guard_Shared = Guard + GuardK + Shared: + +subsection{*Extensions to Theory @{text Shared}*} + +declare initState.simps [simp del] + +subsubsection{*a little abbreviation*} + +syntax Ciph :: "agent => msg" + +translations "Ciph A X" == "Crypt (shrK A) X" + +subsubsection{*agent associated to a key*} + +constdefs agt :: "key => agent" +"agt K == @A. K = shrK A" + +lemma agt_shrK [simp]: "agt (shrK A) = A" +by (simp add: agt_def) + +subsubsection{*basic facts about @{term initState}*} + +lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)" +by (cases A, auto simp: initState.simps) + +lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)" +by auto + +lemma no_shrK_in_analz_init [simp]: "A ~:bad +==> Key (shrK A) ~:analz (initState Spy)" +by (auto simp: initState.simps) + +lemma shrK_notin_initState_Friend [simp]: "A ~= Friend C +==> Key (shrK A) ~: parts (initState (Friend C))" +by (auto simp: initState.simps) + +lemma keyset_init [iff]: "keyset (initState A)" +by (cases A, auto simp: keyset_def initState.simps) + +subsubsection{*sets of symmetric keys*} + +constdefs shrK_set :: "key set => bool" +"shrK_set Ks == ALL K. K:Ks --> (EX A. K = shrK A)" + +lemma in_shrK_set: "[| shrK_set Ks; K:Ks |] ==> EX A. K = shrK A" +by (simp add: shrK_set_def) + +lemma shrK_set1 [iff]: "shrK_set {shrK A}" +by (simp add: shrK_set_def) + +lemma shrK_set2 [iff]: "shrK_set {shrK A, shrK B}" +by (simp add: shrK_set_def) + +subsubsection{*sets of good keys*} + +constdefs good :: "key set => bool" +"good Ks == ALL K. K:Ks --> agt K ~:bad" + +lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad" +by (simp add: good_def) + +lemma good1 [simp]: "A ~:bad ==> good {shrK A}" +by (simp add: good_def) + +lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {shrK A, shrK B}" +by (simp add: good_def) + + +subsection{*Proofs About Guarded Messages*} + +subsubsection{*small hack*} + +lemma shrK_is_invKey_shrK: "shrK A = invKey (shrK A)" +by simp + +lemmas shrK_is_invKey_shrK_substI = shrK_is_invKey_shrK [THEN ssubst] + +lemmas invKey_invKey_substI = invKey [THEN ssubst] + +lemma "Nonce n:parts {X} ==> Crypt (shrK A) X:guard n {shrK A}" +apply (rule shrK_is_invKey_shrK_substI, rule invKey_invKey_substI) +by (rule Guard_Nonce, simp+) + +subsubsection{*guardedness results on nonces*} + +lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks" +by (rule Guard_Nonce, simp) + +lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks" +by (rule Guard_Key, simp) + +lemma Guard_init [iff]: "Guard n Ks (initState B)" +by (induct B, auto simp: Guard_def initState.simps) + +lemma Guard_knows_max': "Guard n Ks (knows_max' C evs) +==> Guard n Ks (knows_max C evs)" +by (simp add: knows_max_def) + +lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs +==> Guard n Ks (spies evs)" +by (auto simp: Guard_def dest: not_used_not_known parts_sub) + +lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)" +by (auto simp: Guard_def dest: known_used parts_trans) + +lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)" +by (auto simp: Guard_def dest: known_max_used parts_trans) + +lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs; +Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)" +apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono) +by (auto simp: knows_max_def) + +subsubsection{*guardedness results on keys*} + +lemma GuardK_init [simp]: "n ~:range shrK ==> GuardK n Ks (initState B)" +by (induct B, auto simp: GuardK_def initState.simps) + +lemma GuardK_knows_max': "[| GuardK n A (knows_max' C evs); n ~:range shrK |] +==> GuardK n A (knows_max C evs)" +by (simp add: knows_max_def) + +lemma Key_not_used_GuardK_spies [dest]: "Key n ~:used evs +==> GuardK n A (spies evs)" +by (auto simp: GuardK_def dest: not_used_not_known parts_sub) + +lemma Key_not_used_GuardK [dest]: "[| evs:p; Key n ~:used evs; +Gets_correct p; one_step p |] ==> GuardK n A (knows (Friend C) evs)" +by (auto simp: GuardK_def dest: known_used parts_trans) + +lemma Key_not_used_GuardK_max [dest]: "[| evs:p; Key n ~:used evs; +Gets_correct p; one_step p |] ==> GuardK n A (knows_max (Friend C) evs)" +by (auto simp: GuardK_def dest: known_max_used parts_trans) + +lemma Key_not_used_GuardK_max' [dest]: "[| evs:p; Key n ~:used evs; +Gets_correct p; one_step p |] ==> GuardK n A (knows_max' (Friend C) evs)" +apply (rule_tac H="knows_max (Friend C) evs" in GuardK_mono) +by (auto simp: knows_max_def) + +subsubsection{*regular protocols*} + +constdefs regular :: "event list set => bool" +"regular p == ALL evs A. evs:p --> (Key (shrK A):parts (spies evs)) = (A:bad)" + +lemma shrK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==> +(Key (shrK A):parts (spies evs)) = (A:bad)" +by (auto simp: regular_def) + +lemma shrK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==> +(Key (shrK A):analz (spies evs)) = (A:bad)" +by auto + +lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p; +shrK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)" +apply (clarify, simp only: knows_decomp) +apply (drule Guard_invKey_keyset, simp+, safe) +apply (drule in_good, simp) +apply (drule in_shrK_set, simp+, clarify) +apply (frule_tac A=A in shrK_analz_iff_bad) +by (simp add: knows_decomp)+ + +lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p; +shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)" +apply (clarify, simp only: knows_decomp) +apply (drule GuardK_invKey_keyset, clarify, simp+, blast) +apply clarify +apply (drule in_good, simp) +apply (drule in_shrK_set, simp+, clarify) +apply (frule_tac A=A in shrK_analz_iff_bad) +by (simp add: knows_decomp)+ + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/List_Msg.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/List_Msg.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,176 @@ +(****************************************************************************** +date: november 2001 +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{*Lists of Messages and Lists of Agents*} + +theory List_Msg = Extensions: + +subsection{*Implementation of Lists by Messages*} + +subsubsection{*nil is represented by any message which is not a pair*} + +syntax cons :: "msg => msg => msg" + +translations "cons x l" => "{|x,l|}" + +subsubsection{*induction principle*} + +lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |] +==> P l" +by (induct l, auto) + +subsubsection{*head*} + +consts head :: "msg => msg" + +recdef head "measure size" +"head (cons x l) = x" + +subsubsection{*tail*} + +consts tail :: "msg => msg" + +recdef tail "measure size" +"tail (cons x l) = l" + +subsubsection{*length*} + +consts len :: "msg => nat" + +recdef len "measure size" +"len (cons x l) = Suc (len l)" +"len other = 0" + +lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'" +by (cases l, auto) + +subsubsection{*membership*} + +consts isin :: "msg * msg => bool" + +recdef isin "measure (%(x,l). size l)" +"isin (x, cons y l) = (x=y | isin (x,l))" +"isin (x, other) = False" + +subsubsection{*delete an element*} + +consts del :: "msg * msg => msg" + +recdef del "measure (%(x,l). size l)" +"del (x, cons y l) = (if x=y then l else cons y (del (x,l)))" +"del (x, other) = other" + +lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l" +by (induct l, auto) + +lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)" +by (induct l, auto) + +subsubsection{*concatenation*} + +consts app :: "msg * msg => msg" + +recdef app "measure (%(l,l'). size l)" +"app (cons x l, l') = cons x (app (l,l'))" +"app (other, l') = l'" + +lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))" +by (induct l, auto) + +subsubsection{*replacement*} + +consts repl :: "msg * nat * msg => msg" + +recdef repl "measure (%(l,i,x'). i)" +"repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))" +"repl (cons x l, 0, x') = cons x' l" +"repl (other, i, M') = other" + +subsubsection{*ith element*} + +consts ith :: "msg * nat => msg" + +recdef ith "measure (%(l,i). i)" +"ith (cons x l, Suc i) = ith (l,i)" +"ith (cons x l, 0) = x" +"ith (other, i) = other" + +lemma ith_head: "0 < len l ==> ith (l,0) = head l" +by (cases l, auto) + +subsubsection{*insertion*} + +consts ins :: "msg * nat * msg => msg" + +recdef ins "measure (%(l,i,x). i)" +"ins (cons x l, Suc i, y) = cons x (ins (l,i,y))" +"ins (l, 0, y) = cons y l" + +lemma ins_head [simp]: "ins (l,0,y) = cons y l" +by (cases l, auto) + +subsubsection{*truncation*} + +consts trunc :: "msg * nat => msg" + +recdef trunc "measure (%(l,i). i)" +"trunc (l,0) = l" +"trunc (cons x l, Suc i) = trunc (l,i)" + +lemma trunc_zero [simp]: "trunc (l,0) = l" +by (cases l, auto) + + +subsection{*Agent Lists*} + +subsubsection{*set of well-formed agent-list messages*} + +syntax nil :: msg + +translations "nil" == "Number 0" + +consts agl :: "msg set" + +inductive agl +intros +Nil[intro]: "nil:agl" +Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl" + +subsubsection{*basic facts about agent lists*} + +lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl" +by (erule agl.induct, auto) + +lemma app_in_agl [intro]: "[| I:agl; J:agl |] ==> app (I,J):agl" +by (erule agl.induct, auto) + +lemma no_Key_in_agl: "I:agl ==> Key K ~:parts {I}" +by (erule agl.induct, auto) + +lemma no_Nonce_in_agl: "I:agl ==> Nonce n ~:parts {I}" +by (erule agl.induct, auto) + +lemma no_Key_in_appdel: "[| I:agl; J:agl |] ==> +Key K ~:parts {app (J, del (Agent B, I))}" +by (rule no_Key_in_agl, auto) + +lemma no_Nonce_in_appdel: "[| I:agl; J:agl |] ==> +Nonce n ~:parts {app (J, del (Agent B, I))}" +by (rule no_Nonce_in_agl, auto) + +lemma no_Crypt_in_agl: "I:agl ==> Crypt K X ~:parts {I}" +by (erule agl.induct, auto) + +lemma no_Crypt_in_appdel: "[| I:agl; J:agl |] ==> +Crypt K X ~:parts {app (J, del (Agent B,I))}" +by (rule no_Crypt_in_agl, auto) + +end diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/NS_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/NS_Public.thy Wed Aug 21 15:53:30 2002 +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 NS_Public = Guard_Public: + +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 febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/OtwayRees.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/OtwayRees.thy Wed Aug 21 15:53:30 2002 +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 OtwayRees = Guard_Shared: + +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 febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/P1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/P1.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,659 @@ +(****************************************************************************** +from G. Karjoth, N. Asokan and C. Gulcu +"Protecting the computation results of free-roaming agents" +Mobiles Agents 1998, LNCS 1477 + +date: february 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{*Protocol P1*} + +theory P1 = Guard_Public + List_Msg: + +subsection{*Protocol Definition*} + +(****************************************************************************** + +the contents of the messages are not completely specified in the paper +we assume that the user sends his request and his itinerary in the clear + +we will adopt the following format for messages: {|A,r,I,L|} +A: originator (agent) +r: request (number) +I: next shops (agent list) +L: collected offers (offer list) + +in the paper, the authors use nonces r_i to add redundancy in the offer +in order to make it safer against dictionary attacks +it is not necessary in our modelization since crypto is assumed to be strong +(Crypt in injective) +******************************************************************************) + +subsubsection{*offer chaining: +B chains his offer for A with the head offer of L for sending it to C*} + +constdefs chain :: "agent => nat => agent => msg => agent => msg" +"chain B ofr A L C == +let m1= Crypt (pubK A) (Nonce ofr) in +let m2= Hash {|head L, Agent C|} in +sign B {|m1,m2|}" + +declare Let_def [simp] + +lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C') += (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')" +by (auto simp: chain_def Let_def) + +lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" +by (auto simp: chain_def sign_def) + +subsubsection{*agent whose key is used to sign an offer*} + +consts shop :: "msg => msg" + +recdef shop "measure size" +"shop {|B,X,Crypt K H|} = Agent (agt K)" + +lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" +by (simp add: chain_def sign_def) + +subsubsection{*nonce used in an offer*} + +consts nonce :: "msg => msg" + +recdef nonce "measure size" +"nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr" + +lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" +by (simp add: chain_def sign_def) + +subsubsection{*next shop*} + +consts next_shop :: "msg => agent" + +recdef next_shop "measure size" +"next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C" + +lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C" +by (simp add: chain_def sign_def) + +subsubsection{*anchor of the offer list*} + +constdefs anchor :: "agent => nat => agent => msg" +"anchor A n B == chain A n A (cons nil nil) B" + +lemma anchor_inj [iff]: "(anchor A n B = anchor A' n' B') += (A=A' & n=n' & B=B')" +by (auto simp: anchor_def) + +lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}" +by (auto simp: anchor_def) + +lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A" +by (simp add: anchor_def) + +lemma nonce_anchor [simp]: "nonce (anchor A n B) = Nonce n" +by (simp add: anchor_def) + +lemma next_shop_anchor [iff]: "next_shop (anchor A n B) = B" +by (simp add: anchor_def) + +subsubsection{*request event*} + +constdefs reqm :: "agent => nat => nat => msg => agent => msg" +"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I), +cons (anchor A n B) nil|}" + +lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B') += (A=A' & r=r' & n=n' & I=I' & B=B')" +by (auto simp: reqm_def) + +lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}" +by (auto simp: reqm_def) + +constdefs req :: "agent => nat => nat => msg => agent => event" +"req A r n I B == Says A B (reqm A r n I B)" + +lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B') += (A=A' & r=r' & n=n' & I=I' & B=B')" +by (auto simp: req_def) + +subsubsection{*propose event*} + +constdefs prom :: "agent => nat => agent => nat => msg => msg => +msg => agent => msg" +"prom B ofr A r I L J C == {|Agent A, Number r, +app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}" + +lemma prom_inj [dest]: "prom B ofr A r I L J C += prom B' ofr' A' r' I' L' J' C' +==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" +by (auto simp: prom_def) + +lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}" +by (auto simp: prom_def) + +constdefs pro :: "agent => nat => agent => nat => msg => msg => +msg => agent => event" +"pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)" + +lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C' +==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" +by (auto simp: pro_def dest: prom_inj) + +subsubsection{*protocol*} + +consts p1 :: "event list set" + +inductive p1 +intros + +Nil: "[]:p1" + +Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" + +Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" + +Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; +I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); +Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" + +subsubsection{*Composition of Traces*} + +lemma "evs':p1 ==> + evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) --> + evs'@evs : p1" +apply (erule p1.induct, safe) +apply (simp_all add: used_ConsI) +apply (erule p1.Fake, erule synth_sub, rule analz_mono, rule knows_sub_app) +apply (erule p1.Request, safe, simp_all add: req_def, force) +apply (erule_tac A'=A' in p1.Propose, simp_all) +apply (drule_tac x=ofr in spec, simp add: pro_def, blast) +apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def) +done + +subsubsection{*Valid Offer Lists*} + +consts valid :: "agent => nat => agent => msg set" + +inductive "valid A n B" +intros +Request [intro]: "cons (anchor A n B) nil:valid A n B" + +Propose [intro]: "L:valid A n B +==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" + +subsubsection{*basic properties of valid*} + +lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" +by (erule valid.cases, auto) + +lemma valid_pos_len: "L:valid A n B ==> 0 < len L" +by (erule valid.induct, auto) + +subsubsection{*offers of an offer list*} + +constdefs offer_nonces :: "msg => msg set" +"offer_nonces L == {X. X:parts {L} & (EX n. X = Nonce n)}" + +subsubsection{*the originator can get the offers*} + +lemma "L:valid A n B ==> offer_nonces L <= analz (insert L (initState A))" +by (erule valid.induct, auto simp: anchor_def chain_def sign_def +offer_nonces_def initState.simps) + +subsubsection{*list of offers*} + +consts offers :: "msg => msg" + +recdef offers "measure size" +"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" +"offers other = nil" + +subsubsection{*list of agents whose keys are used to sign a list of offers*} + +consts shops :: "msg => msg" + +recdef shops "measure size" +"shops (cons M L) = cons (shop M) (shops L)" +"shops other = other" + +lemma shops_in_agl: "L:valid A n B ==> shops L:agl" +by (erule valid.induct, auto simp: anchor_def chain_def sign_def) + +subsubsection{*builds a trace from an itinerary*} + +consts offer_list :: "agent * nat * agent * msg * nat => msg" + +recdef offer_list "measure (%(A,n,B,I,ofr). size I)" +"offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" +"offer_list (A,n,B,cons (Agent C) I,ofr) = ( +let L = offer_list (A,n,B,I,Suc ofr) in +cons (chain (next_shop (head L)) ofr A L C) L)" + +lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B" +by (erule agl.induct, auto) + +consts trace :: "agent * nat * agent * nat * msg * msg * msg +=> event list" + +recdef trace "measure (%(B,ofr,A,r,I,L,K). size K)" +"trace (B,ofr,A,r,I,L,nil) = []" +"trace (B,ofr,A,r,I,L,cons (Agent D) K) = ( +let C = (if K=nil then B else agt_nb (head K)) in +let I' = (if K=nil then cons (Agent A) (cons (Agent B) I) + else cons (Agent A) (app (I, cons (head K) nil))) in +let I'' = app (I, cons (head K) nil) in +pro C (Suc ofr) A r I' L nil D +# trace (B,Suc ofr,A,r,I'',tail L,K))" + +constdefs trace' :: "agent => nat => nat => msg => agent => nat => event list" +"trace' A r n I B ofr == ( +let AI = cons (Agent A) I in +let L = offer_list (A,n,B,AI,ofr) in +trace (B,ofr,A,r,nil,L,AI))" + +declare trace'_def [simp] + +subsubsection{*there is a trace in which the originator receives a valid answer*} + +lemma p1_not_empty: "evs:p1 ==> req A r n I B:set evs --> +(EX evs'. evs'@evs:p1 & pro B' ofr A r I' L J A:set evs' & L:valid A n B)" +oops + + +subsection{*properties of protocol P1*} + +text{*publicly verifiable forward integrity: +anyone can verify the validity of an offer list*} + +subsubsection{*strong forward integrity: +except the last one, no offer can be modified*} + +lemma strong_forward_integrity: "ALL L. Suc i < len L +--> L:valid A n B & repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,xa,l'a|}:valid A n B") +apply (ind_cases "{|x,M,l'a|}:valid A n B") +apply (simp add: chain_def) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +by (drule_tac x=l' in spec, simp, blast) + +subsubsection{*insertion resilience: +except at the beginning, no offer can be inserted*} + +lemma chain_isnt_head [simp]: "L:valid A n B ==> +head L ~= chain (next_shop (head L)) ofr A L C" +by (erule valid.induct, auto simp: chain_def sign_def anchor_def) + +lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L +--> ins (L,Suc i,M) ~:valid A n B" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B", simp) +apply (ind_cases "{|x,M,l'|}:valid A n B", clarsimp) +apply (ind_cases "{|head l',l'|}:valid A n B", simp, simp) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B") +apply (frule len_not_empty, clarsimp) +by (drule_tac x=l' in spec, clarsimp) + +subsubsection{*truncation resilience: +only shop i can truncate at offer i*} + +lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L +--> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|M,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp, simp) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +by (drule_tac x=l' in spec, clarsimp) + +subsubsection{*declarations for tactics*} + +declare knows_Spy_partsEs [elim] +declare Fake_parts_insert [THEN subsetD, dest] +declare initState.simps [simp del] + +subsubsection{*get components of a message*} + +lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==> +M:parts (spies evs) & L:parts (spies evs)" +by blast + +subsubsection{*general properties of p1*} + +lemma reqm_neq_prom [iff]: +"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C" +by (auto simp: reqm_def prom_def) + +lemma prom_neq_reqm [iff]: +"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B" +by (auto simp: reqm_def prom_def) + +lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C" +by (auto simp: req_def pro_def) + +lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B" +by (auto simp: req_def pro_def) + +lemma p1_has_no_Gets: "evs:p1 ==> ALL A X. Gets A X ~:set evs" +by (erule p1.induct, auto simp: req_def pro_def) + +lemma p1_is_Gets_correct [iff]: "Gets_correct p1" +by (auto simp: Gets_correct_def dest: p1_has_no_Gets) + +lemma p1_is_one_step [iff]: "one_step p1" +by (unfold one_step_def, clarify, ind_cases "ev#evs:p1", auto) + +lemma p1_has_only_Says' [rule_format]: "evs:p1 ==> +ev:set evs --> (EX A B X. ev=Says A B X)" +by (erule p1.induct, auto simp: req_def pro_def) + +lemma p1_has_only_Says [iff]: "has_only_Says p1" +by (auto simp: has_only_Says_def dest: p1_has_only_Says') + +lemma p1_is_regular [iff]: "regular p1" +apply (simp only: regular_def, clarify) +apply (erule_tac p1.induct) +apply (simp_all add: initState.simps knows.simps pro_def prom_def + req_def reqm_def anchor_def chain_def sign_def) +by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans) + +subsubsection{*private keys are safe*} + +lemma priK_parts_Friend_imp_bad [rule_format,dest]: + "[| evs:p1; Friend B ~= A |] + ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)" +apply (erule p1.induct) +apply (simp_all add: initState.simps knows.simps pro_def prom_def + req_def reqm_def anchor_def chain_def sign_def, blast) +apply (blast dest: no_Key_in_agl) +apply (auto del: parts_invKey disjE dest: parts_trans + simp add: no_Key_in_appdel) +done + +lemma priK_analz_Friend_imp_bad [rule_format,dest]: + "[| evs:p1; Friend B ~= A |] +==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)" +by auto + +lemma priK_notin_knows_max_Friend: "[| evs:p1; A ~:bad; A ~= Friend C |] +==> Key (priK A) ~:analz (knows_max (Friend C) evs)" +apply (rule not_parts_not_analz, simp add: knows_max_def, safe) +apply (drule_tac H="spies' evs" in parts_sub) +apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) +apply (drule_tac H="spies evs" in parts_sub) +by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend) + +subsubsection{*general guardedness properties*} + +lemma agl_guard [intro]: "I:agl ==> I:guard n Ks" +by (erule agl.induct, auto) + +lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs; +Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" +by (auto dest: Says_to_knows_max') + +lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs; +Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" +by (auto dest: Says_from_knows_max') + +lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs; +Nonce n ~:used evs |] ==> L:guard n Ks" +by (drule not_used_not_parts, auto) + +subsubsection{*guardedness of messages*} + +lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}" +by (case_tac "ofr=n", auto simp: chain_def sign_def) + +lemma chain_guard_Nonce_neq [intro]: "n ~= ofr +==> chain B ofr A' L C:guard n {priK A}" +by (auto simp: chain_def sign_def) + +lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}" +by (case_tac "n'=n", auto simp: anchor_def) + +lemma anchor_guard_Nonce_neq [intro]: "n ~= n' +==> anchor A' n' B:guard n {priK A}" +by (auto simp: anchor_def) + +lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}" +by (case_tac "n'=n", auto simp: reqm_def) + +lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |] +==> reqm A' r n' I B:guard n {priK A}" +by (auto simp: reqm_def) + +lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |] +==> prom B ofr A r I L J C:guard n {priK A}" +by (auto simp: prom_def) + +lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl; +L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}" +by (auto simp: prom_def) + +subsubsection{*Nonce uniqueness*} + +lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr" +by (auto simp: chain_def sign_def) + +lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n" +by (auto simp: anchor_def chain_def sign_def) + +lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B}; +I:agl |] ==> k=n" +by (auto simp: reqm_def dest: no_Nonce_in_agl) + +lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C}; +I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr" +by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel) + +subsubsection{*requests are guarded*} + +lemma req_imp_Guard [rule_format]: "[| evs:p1; A ~:bad |] ==> +req A r n I B:set evs --> Guard n {priK A} (spies evs)" +apply (erule p1.induct, simp) +apply (simp add: req_def knows.simps, safe) +apply (erule in_synth_Guard, erule Guard_analz, simp) +by (auto simp: req_def pro_def dest: Says_imp_knows_Spy) + +lemma req_imp_Guard_Friend: "[| evs:p1; A ~:bad; req A r n I B:set evs |] +==> Guard n {priK A} (knows_max (Friend C) evs)" +apply (rule Guard_knows_max') +apply (rule_tac H="spies evs" in Guard_mono) +apply (rule req_imp_Guard, simp+) +apply (rule_tac B="spies' evs" in subset_trans) +apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) +by (rule knows'_sub_knows) + +subsubsection{*propositions are guarded*} + +lemma pro_imp_Guard [rule_format]: "[| evs:p1; B ~:bad; A ~:bad |] ==> +pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)" +apply (erule p1.induct) (* +3 subgoals *) +(* Nil *) +apply simp +(* Fake *) +apply (simp add: pro_def, safe) (* +4 subgoals *) +(* 1 *) +apply (erule in_synth_Guard, drule Guard_analz, simp, simp) +(* 2 *) +apply simp +(* 3 *) +apply (simp, simp add: req_def pro_def, blast) +(* 4 *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) +(* 5 *) +apply simp +apply safe (* +1 subgoal *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard) +(* 6 *) +apply (simp add: pro_def) +apply (blast dest: Says_imp_knows_Spy) +(* Request *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) +(* Propose *) +apply simp +apply safe (* +1 subgoal *) +(* 1 *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard) +(* 2 *) +apply (simp add: pro_def) +by (blast dest: Says_imp_knows_Spy) + +lemma pro_imp_Guard_Friend: "[| evs:p1; B ~:bad; A ~:bad; +pro B ofr A r I (cons M L) J C:set evs |] +==> Guard ofr {priK A} (knows_max (Friend D) evs)" +apply (rule Guard_knows_max') +apply (rule_tac H="spies evs" in Guard_mono) +apply (rule pro_imp_Guard, simp+) +apply (rule_tac B="spies' evs" in subset_trans) +apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) +by (rule knows'_sub_knows) + +subsubsection{*data confidentiality: +no one other than the originator can decrypt the offers*} + +lemma Nonce_req_notin_spies: "[| evs:p1; req A r n I B:set evs; A ~:bad |] +==> Nonce n ~:analz (spies evs)" +by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) + +lemma Nonce_req_notin_knows_max_Friend: "[| evs:p1; req A r n I B:set evs; +A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)" +apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+) +apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) +by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) + +lemma Nonce_pro_notin_spies: "[| evs:p1; B ~:bad; A ~:bad; +pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)" +by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) + +lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p1; B ~:bad; A ~:bad; +A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |] +==> Nonce ofr ~:analz (knows_max (Friend D) evs)" +apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+) +apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) +by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) + +subsubsection{*non repudiability: +an offer signed by B has been sent by B*} + +lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'" +by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl) + +lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C}; +I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}" +apply (simp add: prom_def anchor_def chain_def sign_def) +by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel) + +lemma Crypt_safeness: "[| evs:p1; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs) +--> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})" +apply (erule p1.induct) +(* Nil *) +apply simp +(* Fake *) +apply clarsimp +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (erule disjE) +apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) +(* Request *) +apply (simp add: req_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (erule disjE) +apply (frule Crypt_reqm, simp, clarify) +apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast) +(* Propose *) +apply (simp add: pro_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (rotate_tac -1, erule disjE) +apply (frule Crypt_prom, simp, simp) +apply (rotate_tac -1, erule disjE) +apply (rule_tac x=C in exI) +apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast) +apply (subgoal_tac "cons M L:parts (spies evsp)") +apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast) +apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj) +apply (drule parts.Snd, drule parts.Snd, drule parts.Snd) +by auto + +lemma Crypt_Hash_imp_sign: "[| evs:p1; A ~:bad |] ==> +Crypt (priK A) (Hash X):parts (spies evs) +--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" +apply (erule p1.induct) +(* Nil *) +apply simp +(* Fake *) +apply clarsimp +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (erule disjE) +apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) +(* Request *) +apply (simp add: req_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (erule disjE) +apply (frule Crypt_reqm, simp+) +apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI) +apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl) +apply (simp add: chain_def sign_def, blast) +(* Propose *) +apply (simp add: pro_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (rotate_tac -1, erule disjE) +apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel) +apply (simp add: chain_def sign_def) +apply (rotate_tac -1, erule disjE) +apply (rule_tac x=C in exI) +apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI) +apply (simp add: prom_def chain_def sign_def) +apply (erule impE) +apply (blast dest: get_ML parts_sub) +apply (blast del: MPair_parts)+ +done + +lemma sign_safeness: "[| evs:p1; A ~:bad |] ==> sign A X:parts (spies evs) +--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" +apply (clarify, simp add: sign_def, frule parts.Snd) +apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def]) +done + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/P2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/P2.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,576 @@ +(****************************************************************************** +from G. Karjoth, N. Asokan and C. Gulcu +"Protecting the computation results of free-roaming agents" +Mobiles Agents 1998, LNCS 1477 + +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{*Protocol P2*} + +theory P2 = Guard_Public + List_Msg: + +subsection{*Protocol Definition*} + + +text{*Like P1 except the definitions of @{text chain}, @{text shop}, + @{text next_shop} and @{text nonce}*} + +subsubsection{*offer chaining: +B chains his offer for A with the head offer of L for sending it to C*} + +constdefs chain :: "agent => nat => agent => msg => agent => msg" +"chain B ofr A L C == +let m1= sign B (Nonce ofr) in +let m2= Hash {|head L, Agent C|} in +{|Crypt (pubK A) m1, m2|}" + +declare Let_def [simp] + +lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C') += (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')" +by (auto simp: chain_def Let_def) + +lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" +by (auto simp: chain_def sign_def) + +subsubsection{*agent whose key is used to sign an offer*} + +consts shop :: "msg => msg" + +recdef shop "measure size" +"shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')" + +lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" +by (simp add: chain_def sign_def) + +subsubsection{*nonce used in an offer*} + +consts nonce :: "msg => msg" + +recdef nonce "measure size" +"nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr" + +lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" +by (simp add: chain_def sign_def) + +subsubsection{*next shop*} + +consts next_shop :: "msg => agent" + +recdef next_shop "measure size" +"next_shop {|m1,Hash {|headL,Agent C|}|} = C" + +lemma "next_shop (chain B ofr A L C) = C" +by (simp add: chain_def sign_def) + +subsubsection{*anchor of the offer list*} + +constdefs anchor :: "agent => nat => agent => msg" +"anchor A n B == chain A n A (cons nil nil) B" + +lemma anchor_inj [iff]: + "(anchor A n B = anchor A' n' B') = (A=A' & n=n' & B=B')" +by (auto simp: anchor_def) + +lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}" +by (auto simp: anchor_def) + +lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A" +by (simp add: anchor_def) + +subsubsection{*request event*} + +constdefs reqm :: "agent => nat => nat => msg => agent => msg" +"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I), +cons (anchor A n B) nil|}" + +lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B') += (A=A' & r=r' & n=n' & I=I' & B=B')" +by (auto simp: reqm_def) + +lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}" +by (auto simp: reqm_def) + +constdefs req :: "agent => nat => nat => msg => agent => event" +"req A r n I B == Says A B (reqm A r n I B)" + +lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B') += (A=A' & r=r' & n=n' & I=I' & B=B')" +by (auto simp: req_def) + +subsubsection{*propose event*} + +constdefs prom :: "agent => nat => agent => nat => msg => msg => +msg => agent => msg" +"prom B ofr A r I L J C == {|Agent A, Number r, +app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}" + +lemma prom_inj [dest]: "prom B ofr A r I L J C = prom B' ofr' A' r' I' L' J' C' +==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" +by (auto simp: prom_def) + +lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}" +by (auto simp: prom_def) + +constdefs pro :: "agent => nat => agent => nat => msg => msg => + msg => agent => event" +"pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)" + +lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C' +==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" +by (auto simp: pro_def dest: prom_inj) + +subsubsection{*protocol*} + +consts p2 :: "event list set" + +inductive p2 +intros + +Nil: "[]:p2" + +Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2" + +Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2" + +Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; +I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); +Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2" + +subsubsection{*valid offer lists*} + +consts valid :: "agent => nat => agent => msg set" + +inductive "valid A n B" +intros +Request [intro]: "cons (anchor A n B) nil:valid A n B" + +Propose [intro]: "L:valid A n B +==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" + +subsubsection{*basic properties of valid*} + +lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" +by (erule valid.cases, auto) + +lemma valid_pos_len: "L:valid A n B ==> 0 < len L" +by (erule valid.induct, auto) + +subsubsection{*list of offers*} + +consts offers :: "msg => msg" + +recdef offers "measure size" +"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" +"offers other = nil" + + +subsection{*Properties of Protocol P2*} + +text{*same as @{text P1_Prop} except that publicly verifiable forward +integrity is replaced by forward privacy*} + +subsection{*strong forward integrity: +except the last one, no offer can be modified*} + +lemma strong_forward_integrity: "ALL L. Suc i < len L +--> L:valid A n B --> repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,xa,l'a|}:valid A n B") +apply (ind_cases "{|x,M,l'a|}:valid A n B") +apply (simp add: chain_def) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +by (drule_tac x=l' in spec, simp, blast) + +subsection{*insertion resilience: +except at the beginning, no offer can be inserted*} + +lemma chain_isnt_head [simp]: "L:valid A n B ==> +head L ~= chain (next_shop (head L)) ofr A L C" +by (erule valid.induct, auto simp: chain_def sign_def anchor_def) + +lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L +--> ins (L,Suc i,M) ~:valid A n B" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B", simp) +apply (ind_cases "{|x,M,l'|}:valid A n B", clarsimp) +apply (ind_cases "{|head l',l'|}:valid A n B", simp, simp) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B") +apply (frule len_not_empty, clarsimp) +by (drule_tac x=l' in spec, clarsimp) + +subsection{*truncation resilience: +only shop i can truncate at offer i*} + +lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L +--> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" +apply (induct i) +(* i = 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|M,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp, simp) +(* i > 0 *) +apply clarify +apply (frule len_not_empty, clarsimp) +apply (ind_cases "{|x,l'|}:valid A n B") +apply (frule len_not_empty, clarsimp) +by (drule_tac x=l' in spec, clarsimp) + +subsection{*declarations for tactics*} + +declare knows_Spy_partsEs [elim] +declare Fake_parts_insert [THEN subsetD, dest] +declare initState.simps [simp del] + +subsection{*get components of a message*} + +lemma get_ML [dest]: "Says A' B {|A,R,I,M,L|}:set evs ==> +M:parts (spies evs) & L:parts (spies evs)" +by blast + +subsection{*general properties of p2*} + +lemma reqm_neq_prom [iff]: +"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C" +by (auto simp: reqm_def prom_def) + +lemma prom_neq_reqm [iff]: +"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B" +by (auto simp: reqm_def prom_def) + +lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C" +by (auto simp: req_def pro_def) + +lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B" +by (auto simp: req_def pro_def) + +lemma p2_has_no_Gets: "evs:p2 ==> ALL A X. Gets A X ~:set evs" +by (erule p2.induct, auto simp: req_def pro_def) + +lemma p2_is_Gets_correct [iff]: "Gets_correct p2" +by (auto simp: Gets_correct_def dest: p2_has_no_Gets) + +lemma p2_is_one_step [iff]: "one_step p2" +by (unfold one_step_def, clarify, ind_cases "ev#evs:p2", auto) + +lemma p2_has_only_Says' [rule_format]: "evs:p2 ==> +ev:set evs --> (EX A B X. ev=Says A B X)" +by (erule p2.induct, auto simp: req_def pro_def) + +lemma p2_has_only_Says [iff]: "has_only_Says p2" +by (auto simp: has_only_Says_def dest: p2_has_only_Says') + +lemma p2_is_regular [iff]: "regular p2" +apply (simp only: regular_def, clarify) +apply (erule_tac p2.induct) +apply (simp_all add: initState.simps knows.simps pro_def prom_def +req_def reqm_def anchor_def chain_def sign_def) +by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans) + +subsection{*private keys are safe*} + +lemma priK_parts_Friend_imp_bad [rule_format,dest]: + "[| evs:p2; Friend B ~= A |] + ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)" +apply (erule p2.induct) +apply (simp_all add: initState.simps knows.simps pro_def prom_def + req_def reqm_def anchor_def chain_def sign_def, blast) +apply (blast dest: no_Key_in_agl) +apply (auto del: parts_invKey disjE dest: parts_trans + simp add: no_Key_in_appdel) +done + +lemma priK_analz_Friend_imp_bad [rule_format,dest]: + "[| evs:p2; Friend B ~= A |] +==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)" +by auto + +lemma priK_notin_knows_max_Friend: + "[| evs:p2; A ~:bad; A ~= Friend C |] + ==> Key (priK A) ~:analz (knows_max (Friend C) evs)" +apply (rule not_parts_not_analz, simp add: knows_max_def, safe) +apply (drule_tac H="spies' evs" in parts_sub) +apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) +apply (drule_tac H="spies evs" in parts_sub) +by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend) + +subsection{*general guardedness properties*} + +lemma agl_guard [intro]: "I:agl ==> I:guard n Ks" +by (erule agl.induct, auto) + +lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs; +Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" +by (auto dest: Says_to_knows_max') + +lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs; +Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" +by (auto dest: Says_from_knows_max') + +lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs; +Nonce n ~:used evs |] ==> L:guard n Ks" +by (drule not_used_not_parts, auto) + +subsection{*guardedness of messages*} + +lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}" +by (case_tac "ofr=n", auto simp: chain_def sign_def) + +lemma chain_guard_Nonce_neq [intro]: "n ~= ofr +==> chain B ofr A' L C:guard n {priK A}" +by (auto simp: chain_def sign_def) + +lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}" +by (case_tac "n'=n", auto simp: anchor_def) + +lemma anchor_guard_Nonce_neq [intro]: "n ~= n' +==> anchor A' n' B:guard n {priK A}" +by (auto simp: anchor_def) + +lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}" +by (case_tac "n'=n", auto simp: reqm_def) + +lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |] +==> reqm A' r n' I B:guard n {priK A}" +by (auto simp: reqm_def) + +lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |] +==> prom B ofr A r I L J C:guard n {priK A}" +by (auto simp: prom_def) + +lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl; +L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}" +by (auto simp: prom_def) + +subsection{*Nonce uniqueness*} + +lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr" +by (auto simp: chain_def sign_def) + +lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n" +by (auto simp: anchor_def chain_def sign_def) + +lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B}; +I:agl |] ==> k=n" +by (auto simp: reqm_def dest: no_Nonce_in_agl) + +lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C}; +I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr" +by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel) + +subsection{*requests are guarded*} + +lemma req_imp_Guard [rule_format]: "[| evs:p2; A ~:bad |] ==> +req A r n I B:set evs --> Guard n {priK A} (spies evs)" +apply (erule p2.induct, simp) +apply (simp add: req_def knows.simps, safe) +apply (erule in_synth_Guard, erule Guard_analz, simp) +by (auto simp: req_def pro_def dest: Says_imp_knows_Spy) + +lemma req_imp_Guard_Friend: "[| evs:p2; A ~:bad; req A r n I B:set evs |] +==> Guard n {priK A} (knows_max (Friend C) evs)" +apply (rule Guard_knows_max') +apply (rule_tac H="spies evs" in Guard_mono) +apply (rule req_imp_Guard, simp+) +apply (rule_tac B="spies' evs" in subset_trans) +apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) +by (rule knows'_sub_knows) + +subsection{*propositions are guarded*} + +lemma pro_imp_Guard [rule_format]: "[| evs:p2; B ~:bad; A ~:bad |] ==> +pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)" +apply (erule p2.induct) (* +3 subgoals *) +(* Nil *) +apply simp +(* Fake *) +apply (simp add: pro_def, safe) (* +4 subgoals *) +(* 1 *) +apply (erule in_synth_Guard, drule Guard_analz, simp, simp) +(* 2 *) +apply simp +(* 3 *) +apply (simp, simp add: req_def pro_def, blast) +(* 4 *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) +(* 5 *) +apply simp +apply safe (* +1 subgoal *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard) +(* 6 *) +apply (simp add: pro_def) +apply (blast dest: Says_imp_knows_Spy) +(* Request *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) +(* Propose *) +apply simp +apply safe (* +1 subgoal *) +(* 1 *) +apply (simp add: pro_def) +apply (blast dest: prom_inj Says_Nonce_not_used_guard) +(* 2 *) +apply (simp add: pro_def) +by (blast dest: Says_imp_knows_Spy) + +lemma pro_imp_Guard_Friend: "[| evs:p2; B ~:bad; A ~:bad; +pro B ofr A r I (cons M L) J C:set evs |] +==> Guard ofr {priK A} (knows_max (Friend D) evs)" +apply (rule Guard_knows_max') +apply (rule_tac H="spies evs" in Guard_mono) +apply (rule pro_imp_Guard, simp+) +apply (rule_tac B="spies' evs" in subset_trans) +apply (rule_tac p=p2 in knows_max'_sub_spies', simp+) +by (rule knows'_sub_knows) + +subsection{*data confidentiality: +no one other than the originator can decrypt the offers*} + +lemma Nonce_req_notin_spies: "[| evs:p2; req A r n I B:set evs; A ~:bad |] +==> Nonce n ~:analz (spies evs)" +by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) + +lemma Nonce_req_notin_knows_max_Friend: "[| evs:p2; req A r n I B:set evs; +A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)" +apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+) +apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) +by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) + +lemma Nonce_pro_notin_spies: "[| evs:p2; B ~:bad; A ~:bad; +pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)" +by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) + +lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p2; B ~:bad; A ~:bad; +A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |] +==> Nonce ofr ~:analz (knows_max (Friend D) evs)" +apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+) +apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) +by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) + +subsection{*forward privacy: +only the originator can know the identity of the shops*} + +lemma forward_privacy_Spy: "[| evs:p2; B ~:bad; A ~:bad; +pro B ofr A r I (cons M L) J C:set evs |] +==> sign B (Nonce ofr) ~:analz (spies evs)" +by (auto simp:sign_def dest: Nonce_pro_notin_spies) + +lemma forward_privacy_Friend: "[| evs:p2; B ~:bad; A ~:bad; A ~= Friend D; +pro B ofr A r I (cons M L) J C:set evs |] +==> sign B (Nonce ofr) ~:analz (knows_max (Friend D) evs)" +by (auto simp:sign_def dest:Nonce_pro_notin_knows_max_Friend ) + +subsection{*non repudiability: an offer signed by B has been sent by B*} + +lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'" +by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl) + +lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C}; +I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}" +apply (simp add: prom_def anchor_def chain_def sign_def) +by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel) + +lemma Crypt_safeness: "[| evs:p2; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs) +--> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})" +apply (erule p2.induct) +(* Nil *) +apply simp +(* Fake *) +apply clarsimp +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (erule disjE) +apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) +(* Request *) +apply (simp add: req_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (erule disjE) +apply (frule Crypt_reqm, simp, clarify) +apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast) +(* Propose *) +apply (simp add: pro_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) +apply (rotate_tac -1, erule disjE) +apply (frule Crypt_prom, simp, simp) +apply (rotate_tac -1, erule disjE) +apply (rule_tac x=C in exI) +apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast) +apply (subgoal_tac "cons M L:parts (spies evsp)") +apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast) +apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj) +apply (drule parts.Snd, drule parts.Snd, drule parts.Snd) +by auto + +lemma Crypt_Hash_imp_sign: "[| evs:p2; A ~:bad |] ==> +Crypt (priK A) (Hash X):parts (spies evs) +--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" +apply (erule p2.induct) +(* Nil *) +apply simp +(* Fake *) +apply clarsimp +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (erule disjE) +apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) +(* Request *) +apply (simp add: req_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (erule disjE) +apply (frule Crypt_reqm, simp+) +apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI) +apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl) +apply (simp add: chain_def sign_def, blast) +(* Propose *) +apply (simp add: pro_def, clarify) +apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) +apply simp +apply (rotate_tac -1, erule disjE) +apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel) +apply (simp add: chain_def sign_def) +apply (rotate_tac -1, erule disjE) +apply (rule_tac x=C in exI) +apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI) +apply (simp add: prom_def chain_def sign_def) +apply (erule impE) +apply (blast dest: get_ML parts_sub) +apply (blast del: MPair_parts)+ +done + +lemma sign_safeness: "[| evs:p2; A ~:bad |] ==> sign A X:parts (spies evs) +--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" +apply (clarify, simp add: sign_def, frule parts.Snd) +apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def]) +done + +end \ No newline at end of file diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Proto.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Proto.thy Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,601 @@ +(****************************************************************************** +date: april 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{*Other Protocol-Independent Results*} + +theory Proto = Guard_Public: + +subsection{*protocols*} + +types rule = "event set * event" + +syntax msg' :: "rule => msg" + +translations "msg' R" == "msg (snd R)" + +types proto = "rule set" + +constdefs wdef :: "proto => bool" +"wdef p == ALL R k. R:p --> Number k:parts {msg' R} +--> Number k:parts (msg`(fst R))" + +subsection{*substitutions*} + +record subs = + agent :: "agent => agent" + nonce :: "nat => nat" + nb :: "nat => msg" + key :: "key => key" + +consts apm :: "subs => msg => msg" + +primrec +"apm s (Agent A) = Agent (agent s A)" +"apm s (Nonce n) = Nonce (nonce s n)" +"apm s (Number n) = nb s n" +"apm s (Key K) = Key (key s K)" +"apm s (Hash X) = Hash (apm s X)" +"apm s (Crypt K X) = ( +if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X) +else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X) +else Crypt (key s K) (apm s X))" +"apm s {|X,Y|} = {|apm s X, apm s Y|}" + +lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}" +apply (erule parts.induct, simp_all, blast) +apply (erule parts.Fst) +apply (erule parts.Snd) +by (erule parts.Body)+ + +lemma Nonce_apm [rule_format]: "Nonce n:parts {apm s X} ==> +(ALL k. Number k:parts {X} --> Nonce n ~:parts {nb s k}) --> +(EX k. Nonce k:parts {X} & nonce s k = n)" +by (induct X, simp_all, blast) + +lemma wdef_Nonce: "[| Nonce n:parts {apm s X}; R:p; msg' R = X; wdef p; +Nonce n ~:parts (apm s `(msg `(fst R))) |] ==> +(EX k. Nonce k:parts {X} & nonce s k = n)" +apply (erule Nonce_apm, unfold wdef_def) +apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) +apply (drule_tac x=x in bspec, simp) +apply (drule_tac Y="msg x" and s=s in apm_parts, simp) +by (blast dest: parts_parts) + +consts ap :: "subs => event => event" + +primrec +"ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)" +"ap s (Gets A X) = Gets (agent s A) (apm s X)" +"ap s (Notes A X) = Notes (agent s A) (apm s X)" + +syntax +ap' :: "rule => msg" +apm' :: "rule => msg" +priK' :: "subs => agent => key" +pubK' :: "subs => agent => key" + +translations +"ap' s R" == "ap s (snd R)" +"apm' s R" == "apm s (msg' R)" +"priK' s A" == "priK (agent s A)" +"pubK' s A" == "pubK (agent s A)" + +subsection{*nonces generated by a rule*} + +constdefs newn :: "rule => nat set" +"newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}" + +lemma newn_parts: "n:newn R ==> Nonce (nonce s n):parts {apm' s R}" +by (auto simp: newn_def dest: apm_parts) + +subsection{*traces generated by a protocol*} + +constdefs ok :: "event list => rule => subs => bool" +"ok evs R s == ((ALL x. x:fst R --> ap s x:set evs) +& (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))" + +consts tr :: "proto => event list set" + +inductive "tr p" intros + +Nil [intro]: "[]:tr p" + +Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |] +==> Says Spy B X # evsf:tr p" + +Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p" + +subsection{*general properties*} + +lemma one_step_tr [iff]: "one_step (tr p)" +apply (unfold one_step_def, clarify) +by (ind_cases "ev # evs:tr p", auto) + +constdefs has_only_Says' :: "proto => bool" +"has_only_Says' p == ALL R. R:p --> is_Says (snd R)" + +lemma has_only_Says'D: "[| R:p; has_only_Says' p |] +==> (EX A B X. snd R = Says A B X)" +by (unfold has_only_Says'_def is_Says_def, blast) + +lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)" +apply (unfold has_only_Says_def) +apply (rule allI, rule allI, rule impI) +apply (erule tr.induct) +apply (auto simp: has_only_Says'_def ok_def) +by (drule_tac x=a in spec, auto simp: is_Says_def) + +lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \ tr p |] +==> (EX A B X. ev = Says A B X)" +by (drule has_only_Says_tr, auto) + +lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s; +ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))" +apply (unfold ok_def, clarsimp) +apply (drule_tac x=x in spec, drule_tac x=x in spec) +by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) + +lemma ok_is_Says: "[| evs' @ ev # evs:tr p; ok evs R s; has_only_Says' p; +R:p; x:fst R |] ==> is_Says x" +apply (unfold ok_def is_Says_def, clarify) +apply (drule_tac x=x in spec, simp) +apply (subgoal_tac "one_step (tr p)") +apply (drule trunc, simp, drule one_step_Cons, simp) +apply (drule has_only_SaysD, simp+) +by (clarify, case_tac x, auto) + +subsection{*types*} + +types keyfun = "rule => subs => nat => event list => key set" + +types secfun = "rule => nat => subs => key set => msg" + +subsection{*introduction of a fresh guarded nonce*} + +constdefs fresh :: "proto => rule => subs => nat => key set => event list +=> bool" +"fresh p R s n Ks evs == (EX evs1 evs2. evs = evs2 @ ap' s R # evs1 +& Nonce n ~:used evs1 & R:p & ok evs1 R s & Nonce n:parts {apm' s R} +& apm' s R:guard n Ks)" + +lemma freshD: "fresh p R s n Ks evs ==> (EX evs1 evs2. +evs = evs2 @ ap' s R # evs1 & Nonce n ~:used evs1 & R:p & ok evs1 R s +& Nonce n:parts {apm' s R} & apm' s R:guard n Ks)" +by (unfold fresh_def, blast) + +lemma freshI [intro]: "[| Nonce n ~:used evs1; R:p; Nonce n:parts {apm' s R}; +ok evs1 R s; apm' s R:guard n Ks |] +==> fresh p R s n Ks (list @ ap' s R # evs1)" +by (unfold fresh_def, blast) + +lemma freshI': "[| Nonce n ~:used evs1; (l,r):p; +Nonce n:parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r):guard n Ks |] +==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)" +by (drule freshI, simp+) + +lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |] +==> Nonce n:used evs" +apply (unfold fresh_def, clarify) +apply (drule has_only_Says'D) +by (auto intro: parts_used_app) + +lemma fresh_newn: "[| evs' @ ap' s R # evs:tr p; wdef p; has_only_Says' p; +Nonce n ~:used evs; R:p; ok evs R s; Nonce n:parts {apm' s R} |] +==> EX k. k:newn R & nonce s k = n" +apply (drule wdef_Nonce, simp+) +apply (frule ok_not_used, simp+) +apply (clarify, erule ok_is_Says, simp+) +apply (clarify, rule_tac x=k in exI, simp add: newn_def) +apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) +apply (drule ok_not_used, simp+) +apply (clarify, erule ok_is_Says, simp+) +by blast + +lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs; +Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev" +apply (drule trunc, simp, ind_cases "ev # evs:tr p", simp) +by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+) + +lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs <= Ks; wdef p; +has_only_Says' p; evs:tr p; ALL R k s. nonce s k = n --> Nonce n:used evs --> +R:p --> k:newn R --> Nonce n:parts {apm' s R} --> apm' s R:guard n Ks --> +apm' s R:parts (spies evs) --> keys R s n evs <= Ks --> P |] ==> P" +apply (frule fresh_used, simp) +apply (unfold fresh_def, clarify) +apply (drule_tac x=R' in spec) +apply (drule fresh_newn, simp+, clarify) +apply (drule_tac x=k in spec) +apply (drule_tac x=s' in spec) +apply (subgoal_tac "apm' s' R':parts (spies (evs2 @ ap' s' R' # evs1))") +apply (case_tac R', drule has_only_Says'D, simp, clarsimp) +apply (case_tac R', drule has_only_Says'D, simp, clarsimp) +apply (rule_tac Y="apm s' X" in parts_parts, blast) +by (rule parts.Inj, rule Says_imp_spies, simp, blast) + +subsection{*safe keys*} + +constdefs safe :: "key set => msg set => bool" +"safe Ks G == ALL K. K:Ks --> Key K ~:analz G" + +lemma safeD [dest]: "[| safe Ks G; K:Ks |] ==> Key K ~:analz G" +by (unfold safe_def, blast) + +lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G" +by (unfold safe_def, blast) + +lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n ~:analz G" +by (blast dest: Guard_invKey) + +subsection{*guardedness preservation*} + +constdefs preserv :: "proto => keyfun => nat => key set => bool" +"preserv p keys n Ks == (ALL evs R' s' R s. evs:tr p --> +Guard n Ks (spies evs) --> safe Ks (spies evs) --> fresh p R' s' n Ks evs --> +keys R' s' n evs <= Ks --> R:p --> ok evs R s --> apm' s R:guard n Ks)" + +lemma preservD: "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs); +safe Ks (spies evs); fresh p R' s' n Ks evs; R:p; ok evs R s; +keys R' s' n evs <= Ks |] ==> apm' s R:guard n Ks" +by (unfold preserv_def, blast) + +lemma preservD': "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs); +safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X):p; +ok evs (l,Says A B X) s; keys R' s' n evs <= Ks |] ==> apm s X:guard n Ks" +by (drule preservD, simp+) + +subsection{*monotonic keyfun*} + +constdefs monoton :: "proto => keyfun => bool" +"monoton p keys == ALL R' s' n ev evs. ev # evs:tr p --> +keys R' s' n evs <= keys R' s' n (ev # evs)" + +lemma monotonD [dest]: "[| keys R' s' n (ev # evs) <= Ks; monoton p keys; +ev # evs:tr p |] ==> keys R' s' n evs <= Ks" +by (unfold monoton_def, blast) + +subsection{*guardedness theorem*} + +lemma Guard_tr [rule_format]: "[| evs:tr p; has_only_Says' p; +preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==> +safe Ks (spies evs) --> fresh p R' s' n Ks evs --> keys R' s' n evs <= Ks --> +Guard n Ks (spies evs)" +apply (erule tr.induct) +(* Nil *) +apply simp +(* Fake *) +apply (clarify, drule freshD, clarsimp) +apply (case_tac evs2) +(* evs2 = [] *) +apply (frule has_only_Says'D, simp) +apply (clarsimp, blast) +(* evs2 = aa # list *) +apply (clarsimp, rule conjI) +apply (blast dest: safe_insert) +(* X:guard n Ks *) +apply (rule in_synth_Guard, simp, rule Guard_analz) +apply (blast dest: safe_insert) +apply (drule safe_insert, simp add: safe_def) +(* Proto *) +apply (clarify, drule freshD, clarify) +apply (case_tac evs2) +(* evs2 = [] *) +apply (frule has_only_Says'D, simp) +apply (frule_tac R=R' in has_only_Says'D, simp) +apply (case_tac R', clarsimp, blast) +(* evs2 = ab # list *) +apply (frule has_only_Says'D, simp) +apply (clarsimp, rule conjI) +apply (drule Proto, simp+, blast dest: safe_insert) +(* apm s X:guard n Ks *) +apply (frule Proto, simp+) +apply (erule preservD', simp+) +apply (blast dest: safe_insert) +apply (blast dest: safe_insert) +by (blast, simp, simp, blast) + +subsection{*useful properties for guardedness*} + +lemma newn_neq_used: "[| Nonce n:used evs; ok evs R s; k:newn R |] +==> n ~= nonce s k" +by (auto simp: ok_def) + +lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x:fst R; is_Says x |] +==> apm s (msg x):parts (spies evs) & apm s (msg x):guard n Ks" +apply (unfold ok_def is_Says_def, clarify) +apply (drule_tac x="Says A B X" in spec, simp) +by (drule Says_imp_spies, auto intro: parts_parts) + +lemma ok_parts_not_new: "[| Y:parts (spies evs); Nonce (nonce s n):parts {Y}; +ok evs R s |] ==> n ~:newn R" +by (auto simp: ok_def dest: not_used_not_spied parts_parts) + +subsection{*unicity*} + +constdefs uniq :: "proto => secfun => bool" +"uniq p secret == ALL evs R R' n n' Ks s s'. R:p --> R':p --> +n:newn R --> n':newn R' --> nonce s n = nonce s' n' --> +Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} --> +apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks --> +evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) --> +secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) --> +secret R n s Ks = secret R' n' s' Ks" + +lemma uniqD: "[| uniq p secret; evs: tr p; R:p; R':p; n:newn R; n':newn R'; +nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs); +Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'}; +secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs); +apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==> +secret R n s Ks = secret R' n' s' Ks" +by (unfold uniq_def, blast) + +constdefs ord :: "proto => (rule => rule => bool) => bool" +"ord p inf == ALL R R'. R:p --> R':p --> ~ inf R R' --> inf R' R" + +lemma ordD: "[| ord p inf; ~ inf R R'; R:p; R':p |] ==> inf R' R" +by (unfold ord_def, blast) + +constdefs uniq' :: "proto => (rule => rule => bool) => secfun => bool" +"uniq' p inf secret == ALL evs R R' n n' Ks s s'. R:p --> R':p --> +inf R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' --> +Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} --> +apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks --> +evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) --> +secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) --> +secret R n s Ks = secret R' n' s' Ks" + +lemma uniq'D: "[| uniq' p inf secret; evs: tr p; inf R R'; R:p; R':p; n:newn R; +n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs); +Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'}; +secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs); +apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==> +secret R n s Ks = secret R' n' s' Ks" +by (unfold uniq'_def, blast) + +lemma uniq'_imp_uniq: "[| uniq' p inf secret; ord p inf |] ==> uniq p secret" +apply (unfold uniq_def) +apply (rule allI)+ +apply (case_tac "inf R R'") +apply (blast dest: uniq'D) +by (auto dest: ordD uniq'D intro: sym) + +subsection{*Needham-Schroeder-Lowe*} + +constdefs +a :: agent "a == Friend 0" +b :: agent "b == Friend 1" +a' :: agent "a' == Friend 2" +b' :: agent "b' == Friend 3" +Na :: nat "Na == 0" +Nb :: nat "Nb == 1" + +consts +ns :: proto +ns1 :: rule +ns2 :: rule +ns3 :: rule + +translations +"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))" + +"ns2" == "({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})}, +Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))" + +"ns3" == "({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}), +Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})}, +Says a b (Crypt (pubK b) (Nonce Nb)))" + +inductive ns intros +[iff]: "ns1:ns" +[iff]: "ns2:ns" +[iff]: "ns3:ns" + +syntax +ns3a :: msg +ns3b :: msg + +translations +"ns3a" => "Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})" +"ns3b" => "Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})" + +constdefs keys :: "keyfun" +"keys R' s' n evs == {priK' s' a, priK' s' b}" + +lemma "monoton ns keys" +by (simp add: keys_def monoton_def) + +constdefs secret :: "secfun" +"secret R n s Ks == +(if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|}) +else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}) +else Number 0)" + +constdefs inf :: "rule => rule => bool" +"inf R R' == (R=ns1 | (R=ns2 & R'~=ns1) | (R=ns3 & R'=ns3))" + +lemma inf_is_ord [iff]: "ord ns inf" +apply (unfold ord_def inf_def) +apply (rule allI)+ +by (rule impI, erule ns.cases, simp_all)+ + +subsection{*general properties*} + +lemma ns_has_only_Says' [iff]: "has_only_Says' ns" +apply (unfold has_only_Says'_def) +apply (rule allI, rule impI) +by (erule ns.cases, auto) + +lemma newn_ns1 [iff]: "newn ns1 = {Na}" +by (simp add: newn_def) + +lemma newn_ns2 [iff]: "newn ns2 = {Nb}" +by (auto simp: newn_def Na_def Nb_def) + +lemma newn_ns3 [iff]: "newn ns3 = {}" +by (auto simp: newn_def) + +lemma ns_wdef [iff]: "wdef ns" +by (auto simp: wdef_def elim: ns.cases) + +subsection{*guardedness for NSL*} + +lemma "uniq ns secret ==> preserv ns keys n Ks" +apply (unfold preserv_def) +apply (rule allI)+ +apply (rule impI, rule impI, rule impI, rule impI, rule impI) +apply (erule fresh_ruleD, simp, simp, simp, simp) +apply (rule allI)+ +apply (rule impI, rule impI, rule impI) +apply (erule ns.cases) +(* fresh with NS1 *) +apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI) +apply (erule ns.cases) +(* NS1 *) +apply clarsimp +apply (frule newn_neq_used, simp, simp) +apply (rule No_Nonce, simp) +(* NS2 *) +apply clarsimp +apply (frule newn_neq_used, simp, simp) +apply (case_tac "nonce sa Na = nonce s Na") +apply (frule Guard_safe, simp) +apply (frule Crypt_guard_invKey, simp) +apply (frule ok_Guard, simp, simp, simp, clarsimp) +apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) +apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) +apply (simp add: secret_def, simp add: secret_def, force, force) +apply (simp add: secret_def keys_def, blast) +apply (rule No_Nonce, simp) +(* NS3 *) +apply clarsimp +apply (case_tac "nonce sa Na = nonce s Nb") +apply (frule Guard_safe, simp) +apply (frule Crypt_guard_invKey, simp) +apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) +apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) +apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) +apply (simp add: secret_def, simp add: secret_def, force, force) +apply (simp add: secret_def, rule No_Nonce, simp) +(* fresh with NS2 *) +apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI) +apply (erule ns.cases) +(* NS1 *) +apply clarsimp +apply (frule newn_neq_used, simp, simp) +apply (rule No_Nonce, simp) +(* NS2 *) +apply clarsimp +apply (frule newn_neq_used, simp, simp) +apply (case_tac "nonce sa Nb = nonce s Na") +apply (frule Guard_safe, simp) +apply (frule Crypt_guard_invKey, simp) +apply (frule ok_Guard, simp, simp, simp, clarsimp) +apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) +apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) +apply (simp add: secret_def, simp add: secret_def, force, force) +apply (simp add: secret_def, rule No_Nonce, simp) +(* NS3 *) +apply clarsimp +apply (case_tac "nonce sa Nb = nonce s Nb") +apply (frule Guard_safe, simp) +apply (frule Crypt_guard_invKey, simp) +apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) +apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) +apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) +apply (simp add: secret_def, simp add: secret_def, force, force) +apply (simp add: secret_def keys_def, blast) +apply (rule No_Nonce, simp) +(* fresh with NS3 *) +by simp + +subsection{*unicity for NSL*} + +lemma "uniq' ns inf secret" +apply (unfold uniq'_def) +apply (rule allI)+ +apply (rule impI, erule ns.cases) +(* R = ns1 *) +apply (rule impI, erule ns.cases) +(* R' = ns1 *) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, erule tr.induct) +(* Nil *) +apply (simp add: secret_def) +(* Fake *) +apply (clarify, simp add: secret_def) +apply (drule notin_analz_insert) +apply (drule Crypt_insert_synth, simp, simp, simp) +apply (drule Crypt_insert_synth, simp, simp, simp, simp) +(* Proto *) +apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule ns.cases) +(* ns1 *) +apply (clarify, simp add: secret_def) +apply (erule disjE, erule disjE, clarsimp) +apply (drule ok_parts_not_new, simp, simp, simp) +apply (clarify, drule ok_parts_not_new, simp, simp, simp) +(* ns2 *) +apply (simp add: secret_def) +(* ns3 *) +apply (simp add: secret_def) +(* R' = ns2 *) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, erule tr.induct) +(* Nil *) +apply (simp add: secret_def) +(* Fake *) +apply (clarify, simp add: secret_def) +apply (drule notin_analz_insert) +apply (drule Crypt_insert_synth, simp, simp, simp) +apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) +(* Proto *) +apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule ns.cases) +(* ns1 *) +apply (clarify, simp add: secret_def) +apply (drule_tac s=sa and n=Na in ok_parts_not_new, simp, simp, simp) +(* ns2 *) +apply (clarify, simp add: secret_def) +apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) +(* ns3 *) +apply (simp add: secret_def) +(* R' = ns3 *) +apply simp +(* R = ns2 *) +apply (rule impI, erule ns.cases) +(* R' = ns1 *) +apply (simp only: inf_def, blast) +(* R' = ns2 *) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, rule impI, rule impI, rule impI) +apply (rule impI, erule tr.induct) +(* Nil *) +apply (simp add: secret_def) +(* Fake *) +apply (clarify, simp add: secret_def) +apply (drule notin_analz_insert) +apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp) +apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) +(* Proto *) +apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule ns.cases) +(* ns1 *) +apply (simp add: secret_def) +(* ns2 *) +apply (clarify, simp add: secret_def) +apply (erule disjE, erule disjE, clarsimp, clarsimp) +apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) +apply (erule disjE, clarsimp) +apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) +by (simp_all add: secret_def) + +end diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/README.html Wed Aug 21 15:53:30 2002 +0200 @@ -0,0 +1,59 @@ + +HOL/Auth/Guard/README.html + +

Protocol-Independent Secrecy Results

+ +date: april 2002 +author: Frederic Blanqui +email: blanqui@lri.fr +webpage: + +

The current development is built above the HOL (Higher-Order Logic) +Isabelle theory and the formalization of protocols introduced by Larry Paulson. More details are +in his paper +The Inductive approach +to verifying cryptographic protocols (J. Computer Security 6, pages +85-128, 1998). + +

+This directory contains a number of files: + +

+ +
+

Last modified 20 August 2002 + +

+Frederic Blanqui, +blanqui@lri.fr +
+ diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/Guard/Yahalom.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Yahalom.thy Wed Aug 21 15:53:30 2002 +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 Yahalom = Guard_Shared: + +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 febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/README.html --- a/src/HOL/Auth/README.html Sat Aug 17 14:55:08 2002 +0200 +++ b/src/HOL/Auth/README.html Wed Aug 21 15:53:30 2002 +0200 @@ -1,13 +1,16 @@ HOL/Auth/README -

Auth--The Inductive Approach to Verifying Security Protocols

+

Auth--The Inductive Approach to Verifying Security Protocols

Cryptographic protocols are of major importance, especially with the -growing use of the Internet. This directory demonstrates a new -proof method. The operational semantics of protocol participants is -defined inductively. The directory contains proofs concerning +growing use of the Internet. This directory demonstrates a new proof method, +which is described in various +papers. The operational semantics of protocol participants is defined +inductively. + +

This directory contains proofs concerning

-

Last modified 30 Jan 1998 +

Last modified 20 August 2002

-lcp@cl.cam.ac.uk +Larry Paulson, +lcp@cl.cam.ac.uk
diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Sat Aug 17 14:55:08 2002 +0200 +++ b/src/HOL/Auth/ROOT.ML Wed Aug 21 15:53:30 2002 +0200 @@ -25,3 +25,11 @@ time_use_thy "NS_Public_Bad"; time_use_thy "NS_Public"; time_use_thy "TLS"; + +(*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"; diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Aug 17 14:55:08 2002 +0200 +++ b/src/HOL/IsaMakefile Wed Aug 21 15:53:30 2002 +0200 @@ -367,7 +367,13 @@ Auth/TLS.thy Auth/WooLam.thy \ Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \ Auth/KerberosIV.ML Auth/KerberosIV.thy \ - Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy + Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \ + 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/P1.thy Auth/Guard/P2.thy \ + Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy @$(ISATOOL) usedir $(OUT)/HOL Auth diff -r febb8e5d2a9d -r 890d736b93a5 src/HOL/List.thy --- a/src/HOL/List.thy Sat Aug 17 14:55:08 2002 +0200 +++ b/src/HOL/List.thy Wed Aug 21 15:53:30 2002 +0200 @@ -555,6 +555,11 @@ lemma in_listsI [intro!]: "\x\set xs. x \ A ==> xs \ lists A" by (rule in_lists_conv_set [THEN iffD2]) +lemma finite_list: "finite A ==> EX l. set l = A" +apply (erule finite_induct, auto) +apply (rule_tac x="x#l" in exI, auto) +done + subsection {* @{text mem} *}