diff options
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 374 |
1 files changed, 330 insertions, 44 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 10fe136..2a8b8a4 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -9,8 +9,12 @@ ------------------------------------------------------------------------ import Aesop +import Mathlib.Data.Prod.Basic +import Mathlib.Tactic.LibrarySearch import Std.Data.List.Basic +macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint) + inductive MatchResult where | is_match : MatchResult | no_match : MatchResult @@ -102,9 +106,47 @@ inductive XmlType | dnsName : XmlType deriving BEq, Repr +instance : LawfulBEq XmlType where + eq_of_beq := by + intros a b h + induction a + all_goals induction b + all_goals + first + | rfl + | contradiction + rfl := by + intro a + induction a + all_goals rfl + def Primitive : Type := XmlType × String deriving BEq, Repr +theorem Prod.beq_iff_fst_eq_snd_eq + {α β : Type} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] + (a b : α × β) : + a == b ↔ a.fst == b.fst ∧ a.snd == b.snd := by + apply Iff.intro + { simp_all only [beq_iff_eq] + intro _ + trivial } + { intro h + simp_all only [beq_iff_eq, Prod.eq_iff_fst_eq_snd_eq] } + +instance : LawfulBEq Primitive where + eq_of_beq := by + intros a b h + rw [Prod.eq_iff_fst_eq_snd_eq] + rw [Prod.beq_iff_fst_eq_snd_eq] at h + simp [beq_iff_eq] at h + assumption + rfl := by + intro a + rw [Prod.beq_iff_fst_eq_snd_eq] + apply And.intro + all_goals simp + def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner) notation:65 "#<" lhs:65 "," rhs:66 ">" => Primitive.mk lhs rhs @@ -142,6 +184,10 @@ inductive Value where | bag (b : Bag) : Value deriving BEq, Repr +instance : LawfulBEq Value where + eq_of_beq := by sorry + rfl := by sorry + instance : Coe (Option Value) Value where coe b := match b with @@ -373,6 +419,38 @@ namespace AttributeDesignator else Sum.inl $ Value.bag (Bag.mk found) end AttributeDesignator +theorem designator_always_returns_bag + (designator : AttributeDesignator) (context : List Attribute) (p : Primitive) : + designator.eval context ≠ Sum.inl (Value.primitive p) := by + simp [AttributeDesignator.eval] + match designator with + | { must_be_present := true, category, identifier, type, issuer .. } => + simp + let check := + List.map (fun x => x.value) + (List.filter + (fun attr => + decide + ((attr.category == category) = true ∧ + (attr.identifier == identifier) = true ∧ + (attr.value.1 == type) = true ∧ ((attr.issuer == none) = true ∨ (attr.issuer == issuer) = true))) + context) + rw_local + List.map (fun x => x.value) + (List.filter + (fun attr => + decide + ((attr.category == category) = true ∧ + (attr.identifier == identifier) = true ∧ + (attr.value.1 == type) = true ∧ ((attr.issuer == none) = true ∨ (attr.issuer == issuer) = true))) + context) = check + by rfl + match check with + | List.nil => simp + | List.cons a b => simp + | { must_be_present := false, .. } => + simp + def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop := designator.category == attr.category ∧ designator.identifier == attr.identifier ∧ @@ -951,21 +1029,61 @@ def compiled_sturecieveextgrades_element := ((ElementTree.Node compiled_sturecie def compiled_stu100_element := ((ElementTree.Node compiled_stu100_metadata [compiled_sturecieveextgrades_element])) def compiled_college100_element := ((ElementTree.Node compiled_college100_metadata [compiled_fac100_element, compiled_stu100_element])) -theorem filter_attr (req : Request) (attr : Attribute): - req.contains attr → - AttributeDesignator.eval - { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, - must_be_present := true } - req = Sum.inl (Value.bag (Bag.mk [attr.value])) := by sorry +#eval Expression.eval (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" [Value.primitive (XmlType.string, "test"), Value.primitive (XmlType.string, "test")]) [] -theorem self_eq_self (s : String) (req : Request) : +theorem string_equal_self (s : String) (req : Request) : Expression.eval (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" [Value.primitive (XmlType.string, s), Value.primitive (XmlType.string, s)]) req = some (Value.primitive (XmlType.boolean, "True")) := by - sorry + simp [Expression.eval, Expression.apply_eval, Primitive.mk] -macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint) +-- #check List.contains_cons +-- theorem ssdf' {α β : Type} [BEq α] [BEq β] (x y : α) (xs : List α) (f : α → β) : x = y → (x == y) = true := by +-- intro h +-- apply? + +theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (x : α) (xs : List α) (f : α → β) : + xs.contains x → (List.map f xs).contains (f x) := by + induction xs with + | nil => + intro h + contradiction + | cons x₁ xs₁ ih => + intro h + simp [ih] at * + cases h with + | inl h' => + apply Or.intro_left + apply congrArg f + assumption + | inr h' => + apply Or.intro_right + apply ih h' + +theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) : + attrs.contains (XmlType.string, s) → + List.contains + (List.map + (fun attr_1 => + Expression.eval + (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" + [Value.primitive (XmlType.string, s), Value.primitive attr_1]) + req) + attrs) + (Value.primitive (XmlType.boolean, "True")) := by + rw_local + (some (Value.primitive (XmlType.boolean, "True"))) = + ((fun attr_1 => + Expression.eval + (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" + [Value.primitive (XmlType.string, s), Value.primitive attr_1]) + req) (XmlType.string, s)) + by + rw [eq_comm] + simp + apply string_equal_self + apply contains_implies_map_contains theorem match_eval (attr : Attribute) (s : String) (req : Request) : attr.value = (XmlType.string, s) → @@ -981,21 +1099,20 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) : req = some (Value.primitive (XmlType.boolean, "True")) := by intros h₁ h₂ simp [Match.eval] - rw_local - AttributeDesignator.eval + rw_local + attr.value = (XmlType.string, s) + by apply h₁ + match AttributeDesignator.eval { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, must_be_present := true } - req = Sum.inl (Value.bag (Bag.mk [attr.value])) - by apply filter_attr _ _ h₂ - - rw [h₁] - rw_local - Expression.eval - (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" - [Value.primitive (XmlType.string, s), Value.primitive (XmlType.string, s)]) - req = some (Value.primitive (XmlType.boolean, "True")) - by apply self_eq_self _ _ - rfl + req with + | Sum.inl (Value.primitive p) => + simp + sorry -- contradiction by designator_always_returns_bag + | Sum.inl (Value.bag b) => sorry + | Sum.inr _ => sorry + -- wts: eval results in a list with the attribute in it + -- wts: streq map containing attribute contains true -- Pr2: All members of Faculty can Assign both InternalGrades and ExternalGrades. @@ -1405,31 +1522,31 @@ def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metada def compiled_gradeAsgnAssigngrades_metadata' := ((PolicyElement.Rule (Rule.mk [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Assign")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "InternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Assign")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "View")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "InternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "View")))]]] none EffectType.permit [] []))) def compiled_Assignp100_metadata' := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.legacy_permit_overrides [] [] []))) def compiled_PPSFaculty100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) -def compiled_gradeAsgnAssigngrades_element' := ((ElementTree.Node compiled_gradeAsgnAssigngrades_metadata [])) -def compiled_Assignp100_element' := ((ElementTree.Node compiled_Assignp100_metadata [compiled_gradeAsgnAssigngrades_element])) -def compiled_PPSFaculty100_element' := ((ElementTree.Node compiled_PPSFaculty100_metadata [compiled_Assignp100_element])) --- root element: compiled_PPSFaculty100_element +def compiled_gradeAsgnAssigngrades_element' := ((ElementTree.Node compiled_gradeAsgnAssigngrades_metadata' [])) +def compiled_Assignp100_element' := ((ElementTree.Node compiled_Assignp100_metadata' [compiled_gradeAsgnAssigngrades_element'])) +def compiled_PPSFaculty100_element' := ((ElementTree.Node compiled_PPSFaculty100_metadata' [compiled_Assignp100_element'])) +-- root element: compiled_PPSFaculty100_element' def compiled_gradedViewgrades_metadata' := ((PolicyElement.Rule (Rule.mk [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Receive")))]]] none EffectType.permit [] []))) def compiled_gradedp100_metadata' := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.legacy_permit_overrides [] [] []))) def compiled_PPSStudent100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) -def compiled_gradedViewgrades_element' := ((ElementTree.Node compiled_gradedViewgrades_metadata [])) -def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metadata [compiled_gradedViewgrades_element])) -def compiled_PPSStudent100_element' := ((ElementTree.Node compiled_PPSStudent100_metadata [compiled_gradedp100_element])) --- root element: compiled_PPSStudent100_element +def compiled_gradedViewgrades_element' := ((ElementTree.Node compiled_gradedViewgrades_metadata' [])) +def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metadata' [compiled_gradedViewgrades_element'])) +def compiled_PPSStudent100_element' := ((ElementTree.Node compiled_PPSStudent100_metadata' [compiled_gradedp100_element'])) +-- root element: compiled_PPSStudent100_element' def compiled_PPSTA100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) -def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element])) --- root element: compiled_PPSTA100_element +def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element'])) +-- root element: compiled_PPSTA100_element' def compiled_RPSFaculty100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" XmlType.string none True) (Value.primitive (XmlType.string, "Faculty")))]]] [] []))) -def compiled_RPSFaculty100_element' := ((ElementTree.Node compiled_RPSFaculty100_metadata [compiled_PPSFaculty100_element])) --- root element: compiled_RPSFaculty100_element +def compiled_RPSFaculty100_element' := ((ElementTree.Node compiled_RPSFaculty100_metadata' [compiled_PPSFaculty100_element'])) +-- root element: compiled_RPSFaculty100_element' def compiled_RPSStudent100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" XmlType.string none True) (Value.primitive (XmlType.string, "Student")))]]] [] []))) -def compiled_RPSStudent100_element' := ((ElementTree.Node compiled_RPSStudent100_metadata [compiled_PPSStudent100_element])) --- root element: compiled_RPSStudent100_element +def compiled_RPSStudent100_element' := ((ElementTree.Node compiled_RPSStudent100_metadata' [compiled_PPSStudent100_element'])) +-- root element: compiled_RPSStudent100_element' def compiled_RPSTA100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" XmlType.string none True) (Value.primitive (XmlType.string, "TA")))]]] [] []))) def compiled_RPSTA100_element' := ((ElementTree.Node compiled_RPSTA100_metadata' [compiled_PPSTA100_element'])) --- root element: compiled_RPSTA100_element +-- root element: compiled_RPSTA100_element' def compiled_RPSlist100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) -def compiled_RPSlist100_element' := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element, compiled_RPSTA100_element'])) +def compiled_RPSlist100_element' := ((ElementTree.Node compiled_RPSlist100_metadata' [compiled_RPSFaculty100_element', compiled_RPSStudent100_element', compiled_RPSTA100_element'])) -- root element: compiled_RPSlist100_element def separation_of_duty (req : Request) := @@ -1439,15 +1556,184 @@ def separation_of_duty (req : Request) := req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role')) ↔ role = role' +-- 2a3 +-- > -- root element: compiled_PPSTA100_element +-- 4a6 +-- > -- root element: compiled_RPSTA100_element +-- 11a14,15 +-- > def compiled_PPSTA100_element := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element])) +-- > def compiled_PPSTA100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) +-- 16c20,22 +-- < def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element])) +-- --- +-- > def compiled_RPSTA100_element := ((ElementTree.Node compiled_RPSTA100_metadata' [compiled_PPSTA100_element'])) +-- > def compiled_RPSTA100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" XmlType.string none True) (Value.primitive (XmlType.string, "TA")))]]] [] []))) +-- > def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element, compiled_RPSTA100_element'])) + +-- Difference lies solely in compiled_RPSlist100_element. + +theorem compiled_RPSFaculty100_element_unchanged : + compiled_RPSFaculty100_element = compiled_RPSFaculty100_element' := by rfl + +theorem asdf (req : Request) (s₁ s₂ : String) : + separation_of_duty req + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, s₁)) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, s₂)) + → s₁ = s₂ + := by + intros hsod hs₁ hs₂ + have hint₁ : + ∀ (role' : String), + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role')) + ↔ s₁ = role' := by apply hsod s₁ hs₁ + apply (Iff.mp (hint₁ s₂)) hs₂ + +theorem student_not_applicable (req : Request) : + ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) + → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable := by + sorry + -- simp [ElementTree.eval', compiled_RPSStudent100_element, compiled_RPSStudent100_metadata, compiled_PPSStudent100_element, compiled_PPSStudent100_metadata, compiled_gradedp100_element, compiled_gradedp100_metadata, PolicyElement.eval, compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata, PolicySet.eval] + -- intro h + -- rw_local + -- Target.eval + -- [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + -- designator := + -- { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role", + -- type := XmlType.string, issuer := none, must_be_present := true }, + -- value := Value.primitive (XmlType.string, "Student") }]]] + -- req = MatchResult.no_match + -- by sorry + +theorem faculty_not_applicable (req : Request) : + ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + → (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable := by + sorry + +theorem ta_not_applicable (req : Request) : + ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA")) + → (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable := by + sorry + +theorem ta_external_grades_not_applicable (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + → (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable := by + sorry + + +theorem not_applicable_no_effect (xs : List Decision') : + PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs = + PolicyCombinatorAlgorithm.eval_legacy_permit_overrides (xs ++ [Decision'.not_applicable]) := by + have append_no_effect (x : Decision') (xs : List Decision') : + (x == Decision'.not_applicable) = false + → List.contains (xs ++ [Decision'.not_applicable]) x + = List.contains xs x := by + intro h + induction xs with + | nil => simp [h] + | cons head tail ih => + simp [List.contains_cons] + cases Classical.em (x == head) with + | inl h' => + simp [h'] + | inr h => + simp [h] + apply ih + simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] + rw_local + List.contains (xs ++ [Decision'.not_applicable]) Decision'.permit + = List.contains xs Decision'.permit + by apply append_no_effect Decision'.permit xs (by rfl) + rw_local + List.contains (xs ++ [Decision'.not_applicable]) Decision'.deny + = List.contains xs Decision'.deny + by apply append_no_effect Decision'.deny xs (by rfl) + rw_local + List.contains (xs ++ [Decision'.not_applicable]) Decision'.indeterminate + = List.contains xs Decision'.indeterminate + by apply append_no_effect Decision'.indeterminate xs (by rfl) + +theorem pr' : + ∀ (req : Request), + separation_of_duty req + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + → PolicyCombinatorAlgorithm.eval_legacy_permit_overrides + [(ElementTree.eval' req compiled_RPSStudent100_element []).1, + (ElementTree.eval' req compiled_RPSFaculty100_element []).1] + = PolicyCombinatorAlgorithm.eval_legacy_permit_overrides + [(ElementTree.eval' req compiled_RPSStudent100_element []).1, + (ElementTree.eval' req compiled_RPSFaculty100_element []).1, + (ElementTree.eval' req compiled_RPSTA100_element []).1] := by + intros req hsod hres + cases Classical.em + (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))) + with + | inl h => + have hint_student : + ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by + apply by_contradiction + intro hcont' + simp at hcont' + have hcont : "TA" = "Student" := by + apply asdf req "TA" "Student" hsod + all_goals assumption + contradiction + rw_local + (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable + by apply student_not_applicable req hint_student + + have hint_faculty : + ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) := by + apply by_contradiction + intro hcont' + simp at hcont' + have hcont : "TA" = "Faculty" := by + apply asdf req "TA" "Faculty" hsod + all_goals assumption + contradiction + rw_local + (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable + by apply faculty_not_applicable req hint_faculty + + rw_local + (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable + by apply ta_external_grades_not_applicable req h hres + rw [not_applicable_no_effect] + simp + | inr h => + rw_local + (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable + by sorry + + + -- cases (ElementTree.eval' req compiled_RPSStudent100_element []).1 + -- all_goals cases (ElementTree.eval' req compiled_RPSFaculty100_element []).1 + theorem pr : ∀ (req : Request), separation_of_duty req → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) → (ElementTree.eval req compiled_RPSlist100_element).fst == (ElementTree.eval req compiled_RPSlist100_element').fst := by intros req hsod h - cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))) with - | inl h' => - cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"))) with - | inl h'' => sorry - | inr h'' => sorry - | inr h' => sorry + simp [compiled_RPSlist100_element, compiled_RPSlist100_element'] + + rw_local + compiled_RPSlist100_metadata' = compiled_RPSlist100_metadata + by rfl + rw_local + compiled_RPSFaculty100_element' = compiled_RPSFaculty100_element + by rfl + rw_local + compiled_RPSStudent100_element' = compiled_RPSStudent100_element + by rfl + + simp [ElementTree.eval, ElementTree.eval', PolicyElement.eval] + simp [compiled_RPSlist100_metadata] + simp [PolicySet.eval] + + -- cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))) with + -- | inl h' => + -- cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"))) with + -- | inl h'' => sorry + -- | inr h'' => sorry + -- | inr h' => sorry |