diff options
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 85 |
1 files changed, 71 insertions, 14 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 3e7b1eb..378d3aa 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -2533,11 +2533,56 @@ theorem not_applicable_no_effect (xs : List Decision') : = List.contains xs Decision'.indeterminate by apply append_no_effect Decision'.indeterminate xs (by rfl) +def separation_of_duty' (req : Request) := + Match.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, "TA") } + req = some (Value.primitive (XmlType.boolean, "True")) + → Match.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, "Faculty") } + req = some (Value.primitive (XmlType.boolean, "False")) + ∧ Match.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 = some (Value.primitive (XmlType.boolean, "False")) + +def well_formed_sub (req : Request) := + ¬(Match.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, "TA") } + req = some (Value.primitive (XmlType.boolean, "True"))) + → Match.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, "TA") } + req = some (Value.primitive (XmlType.boolean, "False")) + theorem pr' : ∀ (req : Request), - separation_of_duty req - → well_formed req - → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + separation_of_duty' req + → well_formed_sub req + → Match.eval + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:resource", identifier := "resource-class", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "InternalGrades") } + req = some (Value.primitive (XmlType.boolean, "False")) → PolicyCombinatorAlgorithm.eval_legacy_permit_overrides [(ElementTree.eval' req compiled_RPSStudent100_element []).1, (ElementTree.eval' req compiled_RPSFaculty100_element []).1] @@ -2545,35 +2590,47 @@ theorem pr' : [(ElementTree.eval' req compiled_RPSTA100_element' []).1, (ElementTree.eval' req compiled_RPSStudent100_element []).1, (ElementTree.eval' req compiled_RPSFaculty100_element []).1] := by - intros req hsod hwf hres + intros req hsod hwf_sub h_not_internal_grades cases Classical.em - (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))) + (Match.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, "TA") } + req = some (Value.primitive (XmlType.boolean, "True"))) with | inl h => rw_local (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable - by apply student_not_applicable req hsod hwf (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by exact (bne_iff_ne "TA" "Student").mp rfl) h) + by apply student_not_applicable req ((hsod h).right) rw_local (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable - by apply faculty_not_applicable req hsod hwf (separation_of_duty_imp_other_role_not_in_req req "TA" "Faculty" hsod (by exact (bne_iff_ne "TA" "Faculty").mp rfl) h) + by apply faculty_not_applicable req ((hsod h).left) rw_local (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable - by apply ta_external_grades_not_applicable req h hres + by apply ta_external_grades_not_applicable req h h_not_internal_grades rw [not_applicable_no_effect] simp | inr h => rw_local (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable - by apply ta_not_applicable req hsod hwf h + by apply ta_not_applicable req (hwf_sub h) rw [not_applicable_no_effect'] theorem pr : ∀ (req : Request), - separation_of_duty req - → well_formed req - → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + separation_of_duty' req + → well_formed_sub req + → Match.eval + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:resource", identifier := "resource-class", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "InternalGrades") } + req = some (Value.primitive (XmlType.boolean, "False")) → (ElementTree.eval req compiled_RPSlist100_element).fst == (ElementTree.eval req compiled_RPSlist100_element').fst := by - intros req hsod hwf h + intros req hsod hwf_sub hwf simp [compiled_RPSlist100_element, compiled_RPSlist100_element'] rw_local @@ -2589,7 +2646,7 @@ theorem pr : simp [ElementTree.eval, ElementTree.eval', PolicyElement.eval] simp [compiled_RPSlist100_metadata] simp [PolicySet.eval, Target.eval] - apply pr' req hsod hwf h + apply pr' req hsod hwf_sub hwf def xml_of_decision (decision : Decision) := match decision with |