From 31e726c52f850a2e4bf4cab8328317a4bb6397bf Mon Sep 17 00:00:00 2001 From: Jakob L. Kreuze Date: Thu, 21 Dec 2023 13:10:22 -0500 Subject: Check-in 2023-12-06 --- xacml-proofs/lean/Xacml.lean | 566 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 545 insertions(+), 21 deletions(-) diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index a210c47..10fe136 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -8,6 +8,9 @@ -- ------------------------------------------------------------------------ +import Aesop +import Std.Data.List.Basic + inductive MatchResult where | is_match : MatchResult | no_match : MatchResult @@ -33,16 +36,17 @@ inductive Decision' where | not_applicable : Decision' deriving BEq, Repr +def Decision'.downcast : Decision' → Decision + | Decision'.permit => Decision.permit + | Decision'.deny => Decision.deny + | Decision'.indeterminate => Decision.indeterminate + | Decision'.indeterminate_d => Decision.indeterminate + | Decision'.indeterminate_p => Decision.indeterminate + | Decision'.indeterminate_dp => Decision.indeterminate + | Decision'.not_applicable => Decision.not_applicable + instance : Coe Decision' Decision where - coe b := - match b with - | Decision'.permit => Decision.permit - | Decision'.deny => Decision.deny - | Decision'.indeterminate => Decision.indeterminate - | Decision'.indeterminate_d => Decision.indeterminate - | Decision'.indeterminate_p => Decision.indeterminate - | Decision'.indeterminate_dp => Decision.indeterminate - | Decision'.not_applicable => Decision.not_applicable + coe := Decision'.downcast inductive EffectType where | permit : EffectType @@ -412,6 +416,12 @@ namespace Expression Value.primitive (XmlType.rfc822Name, rhs)] => Value.primitive (lhs == rhs) | _ => Value.primitive (#) + else if name == "urn:oasis:names:tc:xacml:1.0:function:string-equal" then + match args with + | [Value.primitive (XmlType.string, lhs), + Value.primitive (XmlType.string, rhs)] => + Value.primitive (lhs == rhs) + | _ => Value.primitive (#) else Option.none def eval (expression : Expression) (context : Request) : Option Value := @@ -528,16 +538,21 @@ namespace AllOf namespace AnyOf def eval (disj : AnyOf) (context : Request) : MatchResult := - match disj with - | [] => MatchResult.is_match - | List.cons x xs => match x.eval context with - | MatchResult.is_match => MatchResult.is_match - | MatchResult.no_match => - let rest := AnyOf.eval xs context - if rest == MatchResult.is_match then MatchResult.no_match else rest - | MatchResult.indeterminate => - let rest := AnyOf.eval xs context - if rest == MatchResult.no_match then MatchResult.indeterminate else rest + -- match disj with + -- | [] => MatchResult.is_match + -- | List.cons x xs => match x.eval context with + -- | MatchResult.is_match => MatchResult.is_match + -- | MatchResult.no_match => + -- let rest := AnyOf.eval xs context + -- if rest == MatchResult.no_match then MatchResult.no_match else rest + -- | MatchResult.indeterminate => + -- let rest := AnyOf.eval xs context + -- if rest == MatchResult.no_match then MatchResult.indeterminate else rest + if disj.isEmpty then MatchResult.is_match else + let result := disj.map (fun x => x.eval context) + if result.any (fun x => x == MatchResult.is_match) then MatchResult.is_match + else if result.elem MatchResult.indeterminate then MatchResult.indeterminate + else MatchResult.no_match end AnyOf namespace Target @@ -925,5 +940,514 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary := def Choice : Type := List (Decision × ResultAuxiliary) deriving BEq, Repr -def 2asdf := 2 -#check 1-2 +def compiled_facassignviewgrades_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_fac100_metadata := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.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_sturecieveextgrades_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_stu100_metadata := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.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_college100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] []))) +def compiled_facassignviewgrades_element := ((ElementTree.Node compiled_facassignviewgrades_metadata [])) +def compiled_fac100_element := ((ElementTree.Node compiled_fac100_metadata [compiled_facassignviewgrades_element])) +def compiled_sturecieveextgrades_element := ((ElementTree.Node compiled_sturecieveextgrades_metadata [])) +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 + +theorem self_eq_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 + +macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint) + +theorem match_eval (attr : Attribute) (s : String) (req : Request) : + attr.value = (XmlType.string, s) → + req.contains attr → + Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", + designator := + { category := attr.category, + identifier := attr.identifier, + type := XmlType.string, + issuer := none, + must_be_present := true }, + value := Value.primitive attr.value } + req = some (Value.primitive (XmlType.boolean, "True")) := by + intros h₁ h₂ + simp [Match.eval] + rw_local + 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 + +-- Pr2: All members of Faculty can Assign both InternalGrades and ExternalGrades. + +theorem pr₂_lemma₀ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + → 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.is_match := by + intros h₁ h₂ + simp [AllOf.eval] + rw_local + 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, "True")) + by + let attr := (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + have hint : attr.value = (XmlType.string, "InternalGrades") := by rfl + have h₂' : req.contains attr := by apply h₂ + apply match_eval attr "InternalGrades" req hint h₂' + rw_local + Match.eval + { 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 = some (Value.primitive (XmlType.boolean, "True")) + by + let attr := ({ category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", issuer := none, value := (XmlType.string, "Assign") } : Attribute) + have hint : attr.value = (XmlType.string, "Assign") := by rfl + have h₁' : req.contains attr := by apply h₁ + apply match_eval attr "Assign" req hint h₁' + +theorem pr₂_lemma₁ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + → 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, "ExternalGrades") }, + { 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, "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, "ExternalGrades") }, + { 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") }], + [{ 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.is_match := by + intros h₂ h₃ + simp [Target.eval, AnyOf.eval] + cases (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, "ExternalGrades") }, + { 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) + with + | is_match => simp + | _ => + simp + rw_local + 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.is_match + by apply pr₂_lemma₀ req h₂ h₃ + +theorem pr₂_lemma₂ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + → (ElementTree.eval' req compiled_facassignviewgrades_element []).fst = Decision'.permit := by + intros h₂ h₃ + simp [compiled_facassignviewgrades_element, compiled_facassignviewgrades_metadata] + simp [ElementTree.eval, + ElementTree.eval', + PolicyElement.eval, + Rule.eval] + 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:resource", + identifier := "resource-class", type := XmlType.string, issuer := none, must_be_present := true }, + value := Value.primitive (XmlType.string, "ExternalGrades") }, + { 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, "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, "ExternalGrades") }, + { 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") }], + [{ 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.is_match + by apply pr₂_lemma₁ req h₂ h₃ + simp [Primitive.mk] + +theorem pr₂_lemma₃ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + → 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, "Faculty") }] + req = MatchResult.is_match := by + intro h₁ + simp [AllOf.eval] + rw_local + 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, "True")) + by + let attr := (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + have hint : attr.value = (XmlType.string, "Faculty") := by rfl + have h₂' : req.contains attr := by apply h₁ + apply match_eval attr "Faculty" req hint h₂' + +theorem pr₂_lemma₄ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + → 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, "Faculty") }]]] + req = MatchResult.is_match := by + intros h₁ + simp [Target.eval, AnyOf.eval] + rw_local + (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, "Faculty") }] + req = MatchResult.is_match) + by apply pr₂_lemma₃ req h₁ + +theorem pr₂_lemma₅ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + → (ElementTree.eval' req compiled_fac100_element []).fst = Decision'.permit := by + intros h₁ h₂ h₃ + simp [compiled_fac100_element, compiled_fac100_metadata] + simp [ElementTree.eval, + ElementTree.eval', + PolicyElement.eval] + + simp [Policy.eval] + 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, "Faculty") }]]] + req = MatchResult.is_match + by apply pr₂_lemma₄ req h₁ + + simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides] + rw_local + (ElementTree.eval' req compiled_facassignviewgrades_element []).fst = Decision'.permit + by apply pr₂_lemma₂ req h₂ h₃ + +theorem pr₂ (req : Request) : + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades")) + → (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by + intros h₁ h₂ h₃ + simp [compiled_college100_element, + compiled_college100_metadata, + ElementTree.eval, + ElementTree.eval', + PolicyElement.eval, + PolicySet.eval, + Target.eval, + PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] + rw_local + (ElementTree.eval' req compiled_fac100_element []).fst = Decision'.permit + by apply pr₂_lemma₅ req h₁ h₂ h₃ + +-- Pr1: There do not exist members of Student who can Assign ExternalGrades. (This is violated, so we show a counterexample.) + +def bad_req := + [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")] + +theorem pr₁ : + ∃ (req : Request), + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by + have h₁ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by + { simp } + have h₂ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) := by + { simp } + have h₃ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by + { simp } + + apply Exists.intro bad_req + apply And.intro + { apply h₁ } + apply And.intro + { apply h₂ } + apply And.intro + { apply h₃ } + rfl + +-- Pr3: No combination of roles exists such that a user with those roles can both Receive and Assign the resource ExternalGrades. + +def roles (req : Request) := + req.filter + (fun attr => + match attr with + | { category, identifier, .. } => identifier = "role" && category = "urn:oasis:names:tc:xacml:3.0:attribute-category:subject") + +def bad_req₀ := + [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")] + +def bad_req₁ := + [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")] + +theorem pr₃ : + ∃ (user_roles : List Attribute), + ((∃ (req : Request), + user_roles ⊆ roles req + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive")) + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit) + ∧ (∃ (req : Request), + user_roles ⊆ roles req + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) + ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) + ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit)) + := by + let bad_roles := + ([Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"), + Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")]) + + apply Exists.intro bad_roles + apply And.intro + { apply Exists.intro bad_req₀ + + have h₁ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by + { simp } + have h₂ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive")) := by + { simp } + have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by + { simp } + + apply And.intro + { rw_local + roles bad_req₀ = bad_roles + by rfl } + apply And.intro + { apply h₁ } + apply And.intro + { apply h₂ } + rfl} + { apply Exists.intro bad_req₁ + + have h₁ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by + { simp } + have h₂ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) := by + { simp } + have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by + { simp } + + apply And.intro + { rw_local + roles bad_req₁ = bad_roles + by rfl } + apply And.intro + { apply h₁ } + apply And.intro + { apply h₂ } + rfl} + +--- Property: Adding TAs should not affect ExternalGrades in any way. + +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_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_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_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_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])) +-- 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_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_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_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_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_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_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 +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'])) +-- root element: compiled_RPSlist100_element + +def separation_of_duty (req : Request) := + ∀ (role : String), + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role)) + → ∀ (role' : String), + req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role')) + ↔ role = role' + +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 -- cgit v1.3