Theory SINVAR_BLPbasic
theory SINVAR_BLPbasic
imports "../TopoS_Helper"
begin
subsection ‹SecurityInvariant Basic Bell LaPadula›
type_synonym security_level = nat
definition default_node_properties :: "security_level"
where "default_node_properties ≡ 0"
fun sinvar :: "'v graph ⇒ ('v ⇒ security_level) ⇒ bool" where
"sinvar G nP = (∀ (e1,e2) ∈ edges G. (nP e1) ≤ (nP e2))"
text‹What we call a @{typ security_level} is also referred to as security label
(or security clearance of subjects and classification of objects) in the literature.
The lowest security level is @{term "0::nat"}, which can be understood as unclassified.
Consequently, 1 = confidential, 2 = secret, 3 = topSecret, ....
The total order of the security levels corresponds to the total order of the natural numbers ‹≤›.
It is important that there is smallest security level (i.e. @{const default_node_properties}),
otherwise, a unique and secure default parameter could not exist.
Hence, it is not possible to extend the security levels to @{typ int} to model unlimited ``un-confidentialness''.
›
definition receiver_violation :: "bool" where "receiver_violation ≡ True"
lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
apply(simp only: SecurityInvariant_withOffendingFlows.sinvar_mono_def)
apply(clarify)
by auto
interpretation SecurityInvariant_preliminaries
where sinvar = sinvar
apply unfold_locales
apply(frule_tac finite_distinct_list[OF wf_graph.finiteE])
apply(erule_tac exE)
apply(rename_tac list_edges)
apply(rule_tac ff="list_edges" in SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono])
apply(auto)[6]
apply(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])
done
lemma BLP_def_unique: "otherbot ≠ 0 ⟹
∃G p i f. wf_graph G ∧ ¬ sinvar G p ∧ f ∈ (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G p) ∧
sinvar (delete_edges G f) p ∧
i ∈ snd ` f ∧ sinvar G (p(i := otherbot)) "
apply(simp)
apply (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
SecurityInvariant_withOffendingFlows.is_offending_flows_def)
apply (simp add:graph_ops)
apply (simp split: prod.split_asm prod.split)
apply(rule_tac x="⦇ nodes=set [vertex_1,vertex_2], edges = set [(vertex_1,vertex_2)] ⦈" in exI, simp)
apply(rule conjI)
apply(simp add: wf_graph_def)
apply(rule_tac x="(λ x. 0)(vertex_1 := 1, vertex_2 := 0)" in exI, simp)
apply(rule_tac x="vertex_2" in exI, simp)
apply(rule_tac x="set [(vertex_1,vertex_2)]" in exI, simp)
done
subsubsection ‹ENF›
lemma zero_default_candidate: "⋀ nP e1 e2. ¬ ((≤)::security_level ⇒ security_level ⇒ bool) (nP e1) (nP e2) ⟹ ¬ (≤) (nP e1) 0"
by simp_all
lemma zero_default_candidate_rule: "⋀ (nP::('v ⇒ security_level)) e1 e2. ¬ (nP e1) ≤ (nP e2) ⟹ ¬ (nP e1) ≤ 0"
by simp_all
lemma privacylevel_refl: "((≤)::security_level ⇒ security_level ⇒ bool) e e"
by(simp_all)
lemma BLP_ENF: "SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form sinvar (≤)"
unfolding SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form_def
by simp
lemma BLP_ENF_refl: "SecurityInvariant_withOffendingFlows.ENF_refl sinvar (≤)"
unfolding SecurityInvariant_withOffendingFlows.ENF_refl_def
apply(rule conjI)
apply(simp add: BLP_ENF)
apply(simp add: privacylevel_refl)
done
definition BLP_offending_set:: "'v graph ⇒ ('v ⇒ security_level) ⇒ ('v × 'v) set set" where
"BLP_offending_set G nP = (if sinvar G nP then
{}
else
{ {e ∈ edges G. case e of (e1,e2) ⇒ (nP e1) > (nP e2)} })"
lemma BLP_offending_set: "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = BLP_offending_set"
apply(simp only: fun_eq_iff SecurityInvariant_withOffendingFlows.ENF_offending_set[OF BLP_ENF] BLP_offending_set_def)
apply(rule allI)+
apply(rename_tac G nP)
apply(auto)
done
interpretation BLPbasic: SecurityInvariant_IFS sinvar default_node_properties
rewrites "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = BLP_offending_set"
unfolding receiver_violation_def
unfolding default_node_properties_def
apply(unfold_locales)
apply(rule ballI)
apply(rule SecurityInvariant_withOffendingFlows.ENF_snds_refl_instance[OF BLP_ENF_refl])
apply(simp_all add: BLP_ENF BLP_ENF_refl)[3]
apply(erule default_uniqueness_by_counterexample_IFS)
apply(fact BLP_def_unique)
apply(fact BLP_offending_set)
done
lemma TopoS_BLPBasic: "SecurityInvariant sinvar default_node_properties receiver_violation"
unfolding receiver_violation_def by unfold_locales
text‹Alternate definition of the @{const sinvar}:
For all reachable nodes, the security level is higher›
lemma sinvar_BLPbasic_tancl:
"wf_graph G ⟹ sinvar G nP = (∀ v ∈ nodes G. ∀v' ∈ succ_tran G v. (nP v) ≤ (nP v'))"
proof(unfold sinvar.simps, rule iffI, goal_cases)
case 1
have "(v, v') ∈ (edges G)⇧+ ⟹ nP v ≤ nP v'" for v v'
proof(induction rule: trancl_induct)
case base thus ?case using 1(2) by fastforce
next
case step thus ?case using 1(2) by fastforce
qed
thus ?case
by(simp add: succ_tran_def)
next
case 2
from 2(1)[simplified wf_graph_def] have f1: "fst ` edges G ⊆ nodes G" by simp
from f1 2(2) have "∀v ∈ (fst ` edges G). ∀v'∈succ_tran G v. nP v ≤ nP v'" by auto
thus ?case unfolding succ_tran_def by fastforce
qed
hide_fact (open) sinvar_mono
hide_fact BLP_def_unique zero_default_candidate zero_default_candidate_rule privacylevel_refl BLP_ENF BLP_ENF_refl
hide_const (open) sinvar receiver_violation default_node_properties
end