Frederic Blanqui's new "guard" examples

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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

--- /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: [e-mail]
+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 \<in> 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

--- /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 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/Auth/Guard/README.html</TITLE></HEAD><BODY>
+
+<H1>Protocol-Independent Secrecy Results</H1>
+
+date: april 2002
+author: Frederic Blanqui
+email: [e-mail]
+webpage: 
+
+<P>The current development is built above the HOL (Higher-Order Logic)
+Isabelle theory and the formalization of protocols introduced by <A
+HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>.  More details are
+in his paper <A
+HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf">
+The Inductive approach
+to verifying cryptographic protocols</A> (J. Computer Security 6, pages
+85-128, 1998).
+
+<P>
+This directory contains a number of files:
+
+<UL>
+<LI>Extensions.thy contains extensions of Larry Paulson's files with many useful
+lemmas.
+
+<LI>Analz contains an important theorem about the decomposition of analz
+between pparts (pairs) and kparts (messages that are not pairs).
+
+<LI>Guard contains the protocol-independent secrecy theorem for nonces.
+<LI>GuardK is the same for keys.
+<LI>Guard_Public extends Guard and GuardK for public-key protocols.
+<LI>Guard_Shared extends Guard and GuardK for symmetric-key protocols.
+
+<LI>List_Msg contains definitions on lists (inside messages).
+
+<LI>P1 contains the definition of the protocol P1 and the proof of its
+properties (strong forward integrity, insertion resilience, truncation
+resilience, data confidentiality and non-repudiability)
+
+<LI>P2 is the same for the protocol P2
+
+<LI>NS_Public is for Needham-Schroeder-Lowe
+<LI>OtwayRees is for Otway-Rees
+<LI>Yahalom is for Yahalom
+
+<LI>Proto contains a more precise formalization of protocols with rules
+and a protocol-independent theorem for proving guardness from a preservation
+property. It also contains the proofs for Needham-Schroeder as an example.
+</UL>
+
+<HR>
+<P>Last modified 20 August 2002
+
+<ADDRESS>
+<A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
+<A HREF="mailto:[e-mail]">[e-mail]</A>
+</ADDRESS>
+</BODY></HTML>

--- /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: [e-mail]
+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

--- 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 @@
 <!-- $Id$ -->
 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
 
-<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
+<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
 
 <P>Cryptographic protocols are of major importance, especially with the
-growing use of the Internet.  This directory demonstrates a <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new
-proof method</A>.  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 <A
+HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
+papers</A>.  The operational semantics of protocol participants is defined
+inductively.  
+
+<P>This directory contains proofs concerning
 
 <UL>
 <LI>three versions of the Otway-Rees protocol
@@ -26,9 +29,11 @@
 </UL>
 
 <HR>
-<P>Last modified 30 Jan 1998
+<P>Last modified 20 August 2002
 
 <ADDRESS>
-<A NAME="[e-mail]" HREF="mailto:[e-mail]">[e-mail]</A>
+<A
+HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
+<A HREF="mailto:[e-mail]">[e-mail]</A>
 </ADDRESS>
 </BODY></HTML>

--- 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";

--- 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
 
 

--- 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!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> 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} *}