diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 304 |
1 files changed, 299 insertions, 5 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index efe86d2..3e7b1eb 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -1943,9 +1943,11 @@ def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metada -- root element: compiled_RPSlist100_element 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_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, "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, "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_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' @@ -1957,7 +1959,7 @@ def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metad 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'])) +def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_gradeAsgnAssigngrades_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'])) @@ -2097,6 +2099,83 @@ theorem target_no_match (req : Request) (role : String) : apply anyof_no_match req role h_not_role simp [hint] +theorem allof_match(req : Request) (role : String) : + 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, role) } + req = some (Value.primitive (XmlType.boolean, "True")) + → AllOf.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, role) }] + req = MatchResult.is_match := by + intro h_not_role + unfold AllOf.eval + simp [h_not_role] + +theorem anyof_match (req : Request) (role : String) : + 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, role) } + req = some (Value.primitive (XmlType.boolean, "True")) + → AnyOf.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, role) }]] + req = MatchResult.is_match := by + intro h_role + unfold AnyOf.eval + simp [List.isEmpty] + have hint : + AllOf.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, role) }] + req = MatchResult.is_match := by + apply allof_match req role h_role + simp [hint] + +theorem target_match (req : Request) (role : String) : + 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, role) } + req = some (Value.primitive (XmlType.boolean, "True")) + → 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, role) }]]] + req = MatchResult.is_match := by + intro h_role + unfold Target.eval + simp + have hint : + AnyOf.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, role) }]] + req = MatchResult.is_match := by + apply anyof_match req role h_role + simp [hint] + theorem student_not_applicable (req : Request) : Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -2169,12 +2248,227 @@ theorem ta_not_applicable (req : Request) : apply target_no_match req "TA" h_not_role simp [hint] +theorem internal_grades_no_match₁ (req : Request) (command : String) : + 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")) + → AllOf.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, command) }] + req = MatchResult.no_match := by + intro hno_internal_grades + simp [AllOf.eval, hno_internal_grades] + intro hcont + contradiction + +theorem internal_grades_no_match₂ (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: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")) + → AnyOf.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "Assign") }], + [{ 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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "View") }]] + req = MatchResult.no_match := by + intro hno_internal_grades + simp [AnyOf.eval] + have hint : + AllOf.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "Assign") }] + req = MatchResult.no_match := + by apply internal_grades_no_match₁ req "Assign" hno_internal_grades + simp [hint] + have hint : + AllOf.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "View") }] + req = MatchResult.no_match := + by apply internal_grades_no_match₁ req "View" hno_internal_grades + simp [hint] + rfl + +theorem internal_grades_no_match (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: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")) + → Target.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "Assign") }], + [{ 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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "View") }]]] + req = MatchResult.no_match := by + intro hno_internal_grades + simp [Target.eval] + have hint : + AnyOf.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "Assign") }], + [{ 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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "View") }]] + req = MatchResult.no_match := by + apply internal_grades_no_match₂ req hno_internal_grades + simp [hint] + theorem ta_external_grades_not_applicable (req : Request) : - well_formed req - → 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")) + 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: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_RPSTA100_element' []).1 = Decision'.not_applicable := by - sorry + intros hta hno_internal_grades + simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval, + compiled_RPSTA100_element', compiled_RPSTA100_metadata'] + have hint : + 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, "TA") }]]] + req = MatchResult.is_match := + (by apply target_match req "TA" hta) + simp [hint] + + have hint : Target.eval [] req = MatchResult.is_match := by simp [Target.eval] + + simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval, hint, + Rule.eval, Policy.eval, + compiled_PPSTA100_element', compiled_PPSTA100_metadata', + compiled_gradeAsgnAssigngrades_element'', compiled_gradeAsgnAssigngrades_metadata''] + have hint : + Target.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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "Assign") }], + [{ 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") }, + { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", + type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "View") }]]] + req = MatchResult.no_match := by + apply internal_grades_no_match req hno_internal_grades + simp [hint] + + simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] theorem not_applicable_no_effect' (xs : List Decision') : PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs = |