(***************************************************************************** * ESPL --- an embedded security protocol logic * http://people.inf.ethz.ch/meiersi/espl/ * * Copyright (c) 2009-2011, Simon Meier, ETH Zurich, Switzerland * * Extension to compromising adversaries: * * Copyright (c) 2010-2011, Martin Schaub, ETH Zurich, Switzerland * * All rights reserved. See file LICENCE for more information. ******************************************************************************) theory InferenceRules imports HOL_ext Hints ExplicitModel begin section{* Inference Rules *} subsection{* Role Order *} definition roleMap :: "threadpool \ tid \ role" where "roleMap pool \ (\(done,todo,skipped). Some (done @ todo)) \\<^sub>m pool" lemma roleMap_empty [simp]: "roleMap empty = empty" by(simp add: roleMap_def) lemma dom_roleMap [simp]: "dom (roleMap r) = dom r" by(auto simp: dom_def roleMap_def map_comp_def split: option.splits) lemma roleMap_upd [simp]: "roleMap (pool(i \ (done,todo,skipped))) = (roleMap pool)(i \ (done@todo))" by(rule ext, simp add: roleMap_def map_comp_def) lemma roleMap_SomeD: "roleMap r i = Some R \ \ todo done skipped. r i = Some (done, todo, skipped) \ R = done@todo" by(auto simp: roleMap_def map_comp_def split: option.splits) lemma roleMap_SomeI: "\ r i = Some (done, todo, skipped); R = done @ todo \ \ roleMap r i = Some R" by(auto simp: roleMap_def map_comp_def split: option.splits) lemma roleMap_SomeE: assumes role_exists: "roleMap r i = Some R" obtains "done" todo skipped where "r i = Some (done, todo, skipped)" and "R = done @ todo" using role_exists by (auto simp: roleMap_def map_comp_def split: option.splits) lemma roleMap_le_roleMapI [intro!]: assumes roleMap_leD: "\ i done todo skipped. r i = Some (done, todo, skipped) \ \ done' todo' skipped'. r' i = Some (done', todo', skipped') \ done@todo = done'@todo'" shows "roleMap r \\<^sub>m roleMap r'" by(auto simp: roleMap_def map_comp_def split: option.splits intro!: map_leI dest!: roleMap_leD) lemma (in reachable_thread) roleMap: "roleMap r i = Some (done@todo)" by(fast intro!: thread_exists roleMap_SomeI) subsection{* Prefix Close *} definition prefixClose :: "store \ explicit_trace \ role \ rolestep \ tid \ bool" where "prefixClose s t R step i = (\ st st'. (nextRel (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step]) st st') \ ((recvStep st \ (\ m. Some m = inst s i (stepPat st) \ predOrd t (Ln m) (St (i, st)))) \ predOrd t (St (i, st)) (St (i, st'))) )" context reachable_state begin lemma note_filtered_done[iff]: "Note l ty pt \ set (filter (\ x. \ (noteStep x)) done)" by auto lemma take_while_is_done: assumes facts: "r i = Some(done, step # todo, skipped)" "roleMap r i = Some R" shows isDone: "(takeWhile (\ x. x \ step) R) = done" using facts proof - interpret reachable_thread P t r s i "done" "step#todo" skipped using facts by unfold_locales auto hence "step \ set (step # todo)" by auto hence "step \ set done" using facts by (fastsimp dest!: todo_notin_doneD) hence "(takeWhile (\ x. x \ step) done) = done" by auto hence "(takeWhile (\ x. x \ step) (done @ (step # todo))) = done" by auto moreover have "R = (done @ (step # todo))" using facts by (fastsimp dest: roleMap_SomeD) ultimately show ?thesis by auto qed lemma note_filtered_role: "Note l ty pt \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step]) \ step = (Note l ty pt)" by auto lemma note_filtered_revRole: "Note l ty pt \ set (step# rev (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R))) \ step = (Note l ty pt)" by auto lemma filtered_role_conv: assumes filtered: "st \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step])" shows "(st \ set R \ st \ (Note l ty pt)) \ (st = step)" proof - have "st \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R)) \ (st = step)" using filtered by auto moreover { assume inFilter: "st \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R)) \ (st \ step)" hence "st \ set (takeWhile (\ x. x \ step) R) \ (st \ step)" by auto hence "st \ set R \ (st \ step)" by (auto dest: set_takeWhileD) hence "st \ set R" by auto moreover have "st \ (Note l ty pt)" using inFilter by (auto dest: note_filtered_role) ultimately have ?thesis by auto } ultimately show ?thesis by auto qed lemma filtered_done_conv: assumes isThread: "r i = Some(done, step # todo, skipped)" "roleMap r i = Some R" and filtered: "st \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step])" shows "(st \ set done \ st \ (Note l ty pt)) \ (st = step)" proof - have "(st \ set R \ st \ (Note l ty pt)) \ (st = step)" using filtered by (fastsimp dest: filtered_role_conv) moreover have "(takeWhile (\ x. x \ step) R) = done" using isThread by (fastsimp dest: take_while_is_done) ultimately show ?thesis using isThread and filtered by fastsimp qed lemma filtered_in_done: assumes step: "(i, step) \ steps t" and role_exists: "roleMap r i = Some R \ r i = Some(done, todo, skipped)" and inFiltered: "st \ set (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step])" shows "st \ set done" proof - interpret this_thread: reachable_thread P t r s i "done" todo skipped using role_exists by unfold_locales auto hence "step \ set done" using step by (auto dest: this_thread.in_steps_in_done) moreover then obtain prefix suffix where done_split: "done = prefix @ step # suffix \ step \ set prefix" by (auto dest!: split_list_first) hence "takeWhile (\x. x \ step) (prefix@step#suffix@todo) = prefix" by (subst takeWhile_append2) auto hence "takeWhile (\x. x \ step) R = prefix" using role_exists done_split by (auto elim!: roleMap_SomeE) moreover { assume "st \ step \ takeWhile (\x. x \ step) R = prefix" hence "st \ set prefix" using inFiltered by auto hence ?thesis using done_split by fastsimp } moreover { assume "st = step \ step \ set done" hence ?thesis by auto } ultimately show ?thesis by auto qed lemma recv_roleOrd_imp_predOrd: assumes step: "(i, step) \ steps t" and role_exists: "roleMap r i = Some R" and role_ord: "listOrd R (Recv l pt) step" shows "St (i, (Recv l pt)) \ St (i, step)" proof - from role_exists obtain "done" todo skipped where "R = done @ todo" and "r i = Some (done, todo, skipped)" by (auto elim!: roleMap_SomeE) then interpret this_thread: reachable_thread P t r s i "done" todo skipped by unfold_locales auto show ?thesis using step role_ord `R = done @ todo` by (fast intro!: listOrd_imp_predOrd this_thread.listOrd_recv_role_imp_listOrd_trace) qed lemma send_roleOrd_imp_predOrd: assumes step: "(i, step) \ steps t" and role_exists: "roleMap r i = Some R" and role_ord: "listOrd R (Send l pt) step" shows "St (i, (Send l pt)) \ St (i, step)" proof - from role_exists obtain "done" todo skipped where "R = done @ todo" and "r i = Some (done, todo, skipped)" by (auto elim!: roleMap_SomeE) then interpret this_thread: reachable_thread P t r s i "done" todo skipped by unfold_locales auto show ?thesis using step role_ord `R = done @ todo` by (fast intro!: listOrd_imp_predOrd this_thread.listOrd_send_role_imp_listOrd_trace) qed lemmas roleOrd_imp_predOrd' = send_roleOrd_imp_predOrd[OF in_steps_predOrd1, rule_format] recv_roleOrd_imp_predOrd[OF in_steps_predOrd1, rule_format] lemmas roleOrd_imp_step = in_steps_predOrd1[OF send_roleOrd_imp_predOrd, rule_format] in_steps_predOrd1[OF recv_roleOrd_imp_predOrd, rule_format] lemmas roleOrd_imp_step' = roleOrd_imp_step[OF in_steps_predOrd1, rule_format] lemma prefixClose_rawI: assumes "\ st st'. \ nextRel (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step]) st st'; recvStep st \ \ \ m. Some m = inst s i (stepPat st) \ Ln m \ St (i, st)" and "\ st st'. \ nextRel (filter (\ x. \ (noteStep x)) (takeWhile (\ x. x \ step) R) @ [step]) st st' \ \ St (i, st) \ St (i, st')" shows "prefixClose s t R step i" using prems by (auto simp: prefixClose_def) lemma prefixCloseI: assumes step: "(i, step) \ steps t" and role_exists: "roleMap r i = Some R" shows "prefixClose s t R step i" proof - from role_exists obtain "done" todo skipped where R_split: "R = done @ todo" and "r i = Some (done, todo,skipped)" by (auto elim!: roleMap_SomeE) moreover then interpret this_thread: reachable_thread P t r s i "done" todo skipped by unfold_locales auto from step have "step \ set done" by (rule this_thread.in_steps_in_done) then obtain prefix suffix where done_split: "done = prefix @ step # suffix \ step \ set prefix" by (auto dest!: split_list_first) moreover hence "takeWhile (\x. x \ step) (prefix@step#suffix@todo) = prefix" by (subst takeWhile_append2) auto moreover { fix st st' assume nextRel: "nextRel (step#rev (filter (\ x. \ (noteStep x)) prefix)) st' st" hence in_nextRel: "st' \ set (step#rev (filter (\ x. \ (noteStep x)) prefix)) \ st \ set (step#rev (filter (\ x. \ (noteStep x)) prefix))" by(auto dest: in_set_nextRel1 in_set_nextRel2) hence "st \ set done" and "st' \ set done" using done_split step role_exists nextRel by (auto dest: in_set_nextRel1 in_set_nextRel2 filtered_in_done) hence "st \ set done \ st \ skipped" and "st' \ set done \ st' \ skipped" using step in_nextRel apply - apply(rule conjI, assumption) apply(case_tac "st = step") apply(fastsimp dest: this_thread.in_steps_conv_done_skipped[THEN iffD1]) apply(fastsimp dest!: this_thread.note_in_skipped note_filtered_revRole) apply(rule conjI, assumption) apply(case_tac "st' = step") apply(fastsimp dest: this_thread.in_steps_conv_done_skipped[THEN iffD1]) by(fastsimp dest!: this_thread.note_in_skipped note_filtered_revRole) hence steps: "(i, st) \ steps t" "(i, st') \ steps t" by(auto dest: this_thread.in_steps_conv_done_skipped[THEN iffD1]) { assume "recvStep st" then obtain l pt where "st = Recv l pt" by (cases st) auto hence "\ m. Some m = inst s i (stepPat st) \ Ln m \ St (i, st)" using steps by(auto intro!: Ln_before_inp) } note input = this have "listOrd R st st'" using nextRel and R_split and done_split by(fastsimp dest: nextRel_imp_listOrd listOrd_rev[THEN iffD1] listOrd_filter) hence "St (i, st) \ St (i, st')" using role_exists steps R_split apply - apply(drule this_thread.in_steps_conv_done_skipped[THEN iffD1]) by(fastsimp dest!: this_thread.roleOrd_notSkipped_imp_listOrd_trace dest:listOrd_imp_predOrd)+ note input and this } ultimately show ?thesis by (auto simp: prefixClose_def) qed text{* Support for the "prefix\_close" command. *} lemma ext_prefixClose: "\ (i, step) \ steps t; roleMap r i = Some R \ \ prefixClose s t R step i \ (recvStep step \ (\ m. Some m = inst s i (stepPat step) \ Ln m \ St (i, step)))" by (cases step) (fastsimp intro!: prefixCloseI Ln_before_inp)+ text{* Used for prefix closing assumptions corresponding to a case of an annotation completeness induction proof. *} lemma thread_prefixClose: assumes thread_exists: "r i = Some (step#done, todo, skipped)" and not_skipped: "step \ skipped" shows "(\ st st'. nextRel (step # (filter (\ x. \ (noteStep x)) done)) st st' \ ((recvStep st \ (\ m. Some m = inst s i (stepPat st) \ predOrd t (Ln m) (St (i, st))) ) \ predOrd t (St (i, st)) (St (i, st'))) ) \ (recvStep (last (step#done)) \ (\ m. Some m = inst s i (stepPat (last (step#done))) \ predOrd t (Ln m) (St (i, (last (step#done)))) ) )" (is "?prefix \ ?inp_last") proof - interpret this_thread: reachable_thread P t r s i "step#done" todo skipped using thread_exists by unfold_locales auto { assume recv: "recvStep (last (step#done))" hence last_step: "(i, last (step#done)) \ steps t" proof obtain l pt where recv_eq: "(Recv l pt) = (last (step # done))" using recv by (fastsimp dest!: recvStepD) hence "Recv l pt \ set (step # done)" by auto thus ?thesis using thread_exists recv_eq by(fastsimp dest!: this_thread.in_steps_recv[THEN iffD1]) qed hence "?inp_last" by (cases "last (step # done)") (fastsimp dest!: Ln_before_inp)+ } moreover { fix st st' assume "nextRel (step # (filter (\ x. \ (noteStep x)) done)) st st'" hence listOrd: "listOrd (step # [x\done . \ noteStep x]) st st'" by (auto dest: nextRel_imp_listOrd) hence skipped: "st \ skipped \ st' \ skipped" proof(cases "st = step \ st' \ set done \ \ noteStep st'") case True thus "?thesis" using listOrd not_skipped by (fastsimp dest: this_thread.note_in_skipped) next case False note falseAsms = this thus ?thesis using falseAsms listOrd by (cases "listOrd [x\done . \ noteStep x] st st'") (auto simp add: dest: this_thread.note_in_skipped in_set_listOrd1 in_set_listOrd2 ) qed hence "st \ skipped" "st' \ skipped" by auto hence step_ord: "predOrd t (St (i, st)) (St (i, st'))" proof(cases "st = step \ st' \ set [x\done . \ noteStep x]") case True hence "st' \ set done" by auto thus ?thesis using listOrd skipped True apply - apply(drule conjunct1, drule_tac ?P = "st = step" and ?Q = "st' \ set done" in conjI, assumption) apply(drule_tac ?Q = "listOrd done st st'" and ?P = "st = step \ st' \ set done" in disjI1) apply(drule listOrd.simps(2)[THEN iffD2]) by(fastsimp dest: listOrd_imp_predOrd this_thread.listOrd_done_imp_listOrd_trace) next case False note assms = this thus ?thesis proof(cases "listOrd [x\done . \ noteStep x] st st'") case False thus ?thesis using assms listOrd by auto next case True thus ?thesis using assms listOrd skipped apply - apply(drule listOrd_filter) apply(drule_tac ?Q = "listOrd done st st'" and ?P = "st = step \ st' \ set done" in disjI2) apply(drule listOrd.simps(2)[THEN iffD2]) by (fastsimp dest: listOrd_imp_predOrd this_thread.listOrd_done_imp_listOrd_trace) qed qed hence recv: "recvStep st \ \ m. Some m = inst s i (stepPat st) \ predOrd t (Ln m) (St (i, st))" using this_thread.roleMap by (cases st) (auto intro!: Ln_before_inp dest: in_steps_predOrd1) note step_ord recv } ultimately show ?thesis by fast qed end text{* TODO: Find the right place for this lemma. It is used only in the "prefix\_close" command. *} lemma steps_in_steps: "(i,step) \ steps t \ (i,step) \ steps t" by auto subsection{* Additional Lemmas on Learning Messages *} context reachable_state begin (* TODO: Move *) lemma nothing_before_IK0: "m \ IK0 \ \ y \ Ln m" proof(induct arbitrary: y rule: reachable_induct) case (send t r s i "done" l pt todo m y) then interpret this_state: reachable_state P t r s by unfold_locales show ?case using send by(fastsimp dest: this_state.knows_IK0) next case (decr t r s m k y) then interpret this_state: reachable_state P t r s by unfold_locales show ?case using decr by(fastsimp dest: this_state.knows_IK0) next case (lkr t r s a) then interpret this_state: reachable_state P t r s by unfold_locales show ?case using lkr by(fastsimp dest: this_state.knows_IK0) next case (compr t r s "done" l ty pt todo skipped m y) then interpret this_state: reachable_state P t r s by unfold_locales show ?case using compr by(fastsimp dest: this_state.knows_IK0) qed auto lemmas nothing_before_IK0_iffs [iff] = in_IK0_simps[THEN nothing_before_IK0] end (* rechable_state *) subsubsection{* Resoning about Variable Contents *} context reachable_state begin lemma inst_AVar_ineqs [iff]: "s (AVar v, i) \ Tup x y" "s (AVar v, i) \ Enc m k" "s (AVar v, i) \ Hash m" "s (AVar v, i) \ PK a" "s (AVar v, i) \ SK a" "s (AVar v, i) \ K a b" "s (AVar v, i) \ KShr A" "s (AVar v, i) \ Lit (ENonce n i')" "s (AVar v, i) \ Lit (EConst c)" "s (AVar v, i) \ Lit (EveNonce n)" by (insert inst_AVar_cases[of v i]) (auto simp: Agent_def) declare inst_AVar_cases[iff] declare inst_AVar_ineqs[symmetric, iff] end end