diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 386 |
1 files changed, 326 insertions, 60 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 448f287..42c5150 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -9,6 +9,8 @@ ------------------------------------------------------------------------ import Aesop +import Mathlib.Data.Bool.AllAny +import Mathlib.Data.Multiset.Basic import Mathlib.Data.Prod.Basic import Mathlib.Tactic.LibrarySearch import Std.Data.List.Basic @@ -19,14 +21,28 @@ inductive MatchResult where | is_match : MatchResult | no_match : MatchResult | indeterminate : MatchResult -deriving BEq, Repr +deriving DecidableEq, BEq, Repr + +instance : LawfulBEq MatchResult 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 inductive Decision where | permit : Decision | deny : Decision | indeterminate : Decision | not_applicable : Decision -deriving BEq, Repr +deriving DecidableEq, BEq, Repr -- This type is used to implement the semantics described in § 7.10 (Extended -- Indeterminate). It is only relevant to combining algorithms. @@ -38,11 +54,21 @@ inductive Decision' where | indeterminate_p : Decision' | indeterminate_dp : Decision' | not_applicable : Decision' -deriving BEq, Repr +deriving DecidableEq, BEq, Repr instance : LawfulBEq Decision' where - eq_of_beq := by sorry - rfl := by sorry + 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 Decision'.downcast : Decision' → Decision | Decision'.permit => Decision.permit @@ -59,7 +85,7 @@ instance : Coe Decision' Decision where inductive EffectType where | permit : EffectType | deny : EffectType -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace EffectType def to_decision (e : EffectType) : Decision := @@ -108,14 +134,14 @@ inductive XmlType | rfc822Name : XmlType | ipAddress : XmlType | dnsName : XmlType -deriving BEq, Repr +deriving DecidableEq, BEq, Repr instance : LawfulBEq XmlType where eq_of_beq := by intros a b h induction a all_goals induction b - all_goals + all_goals first | rfl | contradiction @@ -125,9 +151,9 @@ instance : LawfulBEq XmlType where all_goals rfl def Primitive : Type := XmlType × String -deriving BEq, Repr +deriving DecidableEq, BEq, Repr -theorem Prod.beq_iff_fst_eq_snd_eq +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 @@ -149,7 +175,7 @@ instance : LawfulBEq Primitive where intro a rw [Prod.beq_iff_fst_eq_snd_eq] apply And.intro - all_goals simp + all_goals simp def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner) @@ -175,21 +201,44 @@ instance : Coe (Option Primitive) Primitive where structure Bag where contents: List Primitive -deriving Repr +deriving BEq, DecidableEq, Repr + +-- def Bag.beq (b₁ b₂ : Bag) : Bool := +-- b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x) -def Bag.beq (b₁ b₂ : Bag) : Bool := - b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x) +#check {1, 2, 3} instance : BEq Bag where beq := Bag.beq +-- instance : LawfulBEq Bag where +-- eq_of_beq := by +-- intros a b h + +-- rfl := by sorry + inductive Value where | primitive (p : Primitive) : Value | bag (b : Bag) : Value -deriving BEq, Repr +deriving DecidableEq, BEq, Repr instance : LawfulBEq Value where - eq_of_beq := by sorry + eq_of_beq := by + intros a b h + cases a with + | primitive pa => + cases b with + | primitive pb => + simp + exact (beq_iff_eq pa pb).mp h + | bag bb => contradiction + | bag ba => + cases b with + | primitive pb => contradiction + | bag bb => + simp + sorry + -- exact (beq_iff_eq ba bb).mp h rfl := by sorry instance : Coe (Option Value) Value where @@ -225,7 +274,7 @@ structure Attribute where identifier : String issuer : Option String value : Primitive -deriving BEq, Repr +deriving DecidableEq, BEq, Repr instance : LawfulBEq Attribute where eq_of_beq := by sorry @@ -241,7 +290,7 @@ deriving Repr --- def Identifier : Type := String -deriving BEq, Repr +deriving DecidableEq, BEq, Repr inductive RuleCombinatorAlgorithm where | deny_overrides : RuleCombinatorAlgorithm @@ -382,7 +431,7 @@ inductive StatusCode | missing_attribute : StatusCode | syntax_error : StatusCode | processing_error : StatusCode -deriving BEq, Repr +deriving DecidableEq, BEq, Repr structure AttributeDesignator where category : String @@ -390,7 +439,7 @@ structure AttributeDesignator where type : XmlType issuer : Option String must_be_present : Bool -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace AttributeDesignator -- A named attribute SHALL match an attribute if the values of their @@ -467,7 +516,7 @@ def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop := | _ => False def FunctionID : Type := String -deriving BEq, Repr +deriving DecidableEq, BEq, Repr -- "The <Expression> element is not used directly in a policy. The <Expression> -- element signifies that an element that extends the ExpressionType and is a @@ -490,7 +539,7 @@ inductive Expression where | attribute_designator (inner : AttributeDesignator) : Expression | attribute_value (inner : Value) : Expression | function (function : FunctionID) : Expression -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace Expression def apply_eval (name : FunctionID) (args : List Value) : Option Value := @@ -537,13 +586,29 @@ structure Match where function : Identifier designator : AttributeDesignator value : Value -deriving BEq, Repr +deriving DecidableEq, BEq, Repr def AllOf : Type := List Match -deriving BEq, Repr +deriving DecidableEq, BEq, Repr def AnyOf : Type := List AllOf -deriving BEq, Repr +deriving DecidableEq, BEq, Repr def Target : Type := List AnyOf -deriving BEq, Repr +deriving DecidableEq, BEq, Repr + +instance : Membership AllOf AnyOf where + mem := fun x y => y.contains x + +instance : LawfulBEq Match where + eq_of_beq := by sorry + rfl := by sorry +instance : LawfulBEq AllOf where + eq_of_beq := by sorry + rfl := by sorry +instance : LawfulBEq AnyOf where + eq_of_beq := by sorry + rfl := by sorry +instance : LawfulBEq Target where + eq_of_beq := by sorry + rfl := by sorry namespace Match -- The evaluation semantics for a matching element is as follows. @@ -618,7 +683,7 @@ namespace AllOf result.elem (Value.primitive (XmlType.boolean, "Indeterminate")) then MatchResult.indeterminate else MatchResult.no_match - end AllOf +end AllOf namespace AnyOf def eval (disj : AnyOf) (context : Request) : MatchResult := @@ -639,6 +704,113 @@ namespace AnyOf else MatchResult.no_match end AnyOf +theorem elem_imp_nonempty + {α : Type} + (x : α) (xs : List α) : + x ∈ xs → xs.isEmpty = false := by + induction xs with + | nil => simp + | cons _ _ _ => simp [List.isEmpty] + +theorem elem_map + {α β : Type} + [BEq α] [LawfulBEq α] + [BEq β] [LawfulBEq β] + (x : α) (xs : List α) (f : α → β) : + List.elem x xs → List.elem (f x) (List.map f xs) := by + induction xs with + | nil => simp + | cons hd tl ih => + intro h + simp [List.elem_cons] at * + cases h with + | inl h => + apply Or.intro_left + exact congrArg f h + | inr h => + apply Or.intro_right + simp [List.contains] at * + apply ih h + +theorem elem_imp_forall_not + {α β : Type} + [BEq α] [LawfulBEq α] + [BEq β] [LawfulBEq β] + (y : β) (xs : List α) (f : α → β) : + (∀ (x : α), x ∈ xs → f x ≠ y) → + List.elem y (List.map f xs) = false := by + induction xs with + | nil => simp + | cons x xs ih => + simp + intros hy h_no_y + apply And.intro + { rw [eq_comm] + exact hy } + { apply ih h_no_y } + +theorem table_1_target_match_table₁ (disj : List AllOf) (context : Request) : + (∃ (conj : AllOf), conj ∈ disj ∧ conj.eval context = MatchResult.is_match) + → AnyOf.eval disj context = MatchResult.is_match := by + intro h + unfold AnyOf.eval + simp + intro _ h₂ + apply False.elim + let ⟨x, hx⟩ := h + have hc₁ : ¬AllOf.eval x context = MatchResult.is_match := by + apply h₂ + exact hx.left + have hc₂ : AllOf.eval x context = MatchResult.is_match := by + exact hx.right + contradiction + +theorem table_1_target_match_table₂ (disj : List AllOf) (context : Request) : + (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.is_match) + → (∃ (conj : AllOf), conj ∈ disj ∧ conj.eval context = MatchResult.indeterminate) + → AnyOf.eval disj context = MatchResult.indeterminate := by + intros h_no_match h_indet + simp [AnyOf.eval] + + let ⟨x, hx⟩ := h_indet + + have hbranch : + List.elem MatchResult.indeterminate + (List.map (fun x => AllOf.eval x context) disj) + = true := by + have hx' : AllOf.eval x context = MatchResult.indeterminate := by + exact hx.right + rw [←hx'] + apply elem_map x disj (fun y => y.eval context) + apply List.elem_eq_true_of_mem hx.left + have hnonempty : List.isEmpty disj = false := by + apply elem_imp_nonempty _ _ hx.left + simp [hnonempty, hbranch] + intros x hx + apply h_no_match + exact hx + +theorem table_1_target_match_table₃ (disj : List AllOf) (context : Request) : + (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.is_match) + → (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.indeterminate) + → disj.isEmpty = false + → AnyOf.eval disj context = MatchResult.no_match := by + intros h_no_match h_no_indet h_nonempty + simp [AnyOf.eval] + + simp [h_nonempty] + have h_no_match : + ¬ ∃ a, a ∈ disj ∧ AllOf.eval a context = MatchResult.is_match := by + simp + apply h_no_match + have h_no_indet : + List.elem MatchResult.indeterminate + (List.map (fun x => AllOf.eval x context) disj) + = false := by + apply elem_imp_forall_not + apply h_no_indet + simp [h_no_match, h_no_indet] + namespace Target def eval (target : Target) (context : Request) : MatchResult := match target with @@ -661,19 +833,19 @@ end Target structure Obligation where assignments : List Attribute identifier : String -deriving BEq, Repr +deriving DecidableEq, BEq, Repr structure Advice where assignments : List Attribute identifier : String -deriving BEq, Repr +deriving DecidableEq, BEq, Repr structure AttributeAssignmentExpression where category : String identifier : String issuer : Option String expression : Expression -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace AttributeAssignmentExpression def eval (assignment : AttributeAssignmentExpression) (context : Request) : Option Attribute := @@ -691,7 +863,7 @@ structure ObligationExpression where assignments : List AttributeAssignmentExpression identifier : String fulfill_on : Decision -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace ObligationExpression def eval (obligation : ObligationExpression) (context : Request) : Option Obligation := @@ -707,7 +879,7 @@ structure AdviceExpression where assignments : List AttributeAssignmentExpression identifier : String applies_to : Decision -deriving BEq, Repr +deriving DecidableEq, BEq, Repr namespace AdviceExpression def eval (advice : AdviceExpression) (context : Request) : Option Advice := @@ -723,13 +895,13 @@ structure ResultAuxiliary where status : Option (List StatusCode) obligations : List Obligation advice : List Advice -deriving BEq, Repr +deriving DecidableEq, BEq, Repr structure ResultAuxiliary' where status : Option (List StatusCode) obligations : List ObligationExpression advice : List AdviceExpression -deriving BEq, Repr +deriving DecidableEq, BEq, Repr structure MissingAttributeDetail where category : String @@ -737,7 +909,7 @@ structure MissingAttributeDetail where issuer : Option String value : Option Value type : XmlType -deriving BEq, Repr +deriving DecidableEq, BEq, Repr def Result : Type := Decision' × (Option ResultAuxiliary) def Result' : Type := Decision' × (Option ResultAuxiliary') @@ -1022,7 +1194,7 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary := (advice₁ ++ advice₂) def Choice : Type := List (Decision × ResultAuxiliary) -deriving BEq, Repr +deriving DecidableEq, BEq, Repr 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")))]]] [] []))) @@ -1059,15 +1231,15 @@ theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BE intro h simp [ih] at * cases h with - | inl h' => + | inl h' => apply Or.intro_left apply congrArg f assumption - | inr h' => + | inr h' => apply Or.intro_right apply ih h' -theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) : +theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) : attrs.contains (XmlType.string, s) → List.contains (List.map @@ -1079,13 +1251,13 @@ theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request attrs) (Value.primitive (XmlType.boolean, "True")) := by rw_local - (some (Value.primitive (XmlType.boolean, "True"))) = + (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 + by rw [eq_comm] simp apply string_equal_self @@ -1105,14 +1277,14 @@ 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 + 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 with - | Sum.inl (Value.primitive p) => + | Sum.inl (Value.primitive p) => simp sorry -- contradiction by designator_always_returns_bag | Sum.inl (Value.bag b) => sorry @@ -1658,7 +1830,7 @@ theorem separation_of_duty_imp_other_role_not_in_req' (req : Request) (s₁ 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₂ + 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')) @@ -1709,7 +1881,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : value := Value.primitive (XmlType.string, "Receive") }]]], condition := none, effect := EffectType.permit, obligations := [], advice := [] }) [] with - | (Decision'.permit, _) => + | (Decision'.permit, _) => simp [PolicyElement.eval, PolicySet.eval] match Target.eval [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1718,7 +1890,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Student") }]]] req with - | MatchResult.is_match => + | MatchResult.is_match => simp [Target.eval] simp [Policy.eval, Target.eval] simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] @@ -1742,7 +1914,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Student") }]]] req with - | MatchResult.is_match => + | MatchResult.is_match => simp [Target.eval] simp [Policy.eval, Target.eval] simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] @@ -1757,7 +1929,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : all_goals { intro hbad simp [hbad] at h } | MatchResult.indeterminate => sorry - | (Decision'.not_applicable, _) => + | (Decision'.not_applicable, _) => simp [PolicyElement.eval, PolicySet.eval] match Target.eval [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1766,7 +1938,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Student") }]]] req with - | MatchResult.is_match => + | MatchResult.is_match => simp [Target.eval] simp [Policy.eval, Target.eval] simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] @@ -1790,7 +1962,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') : 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') : + 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 @@ -1799,10 +1971,14 @@ theorem not_applicable_no_effect (xs : List Decision') : | nil => simp [h] | cons head tail ih => simp [List.contains_cons] + -- match (x == head) with + -- | true => simp + -- | false => simp + cases Classical.em (x == head) with - | inl h' => + | inl h' => simp [h'] - | inr h => + | inr h => simp [h] apply ih simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] @@ -1832,10 +2008,10 @@ theorem pr' : (ElementTree.eval' req compiled_RPSStudent100_element []).1, (ElementTree.eval' req compiled_RPSFaculty100_element []).1] := by intros req hsod hwf hres - cases Classical.em + 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 => + | inl h => rw_local (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable by apply student_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by simp) h) @@ -1861,7 +2037,7 @@ theorem pr : → (ElementTree.eval req compiled_RPSlist100_element).fst == (ElementTree.eval req compiled_RPSlist100_element').fst := by intros req hsod hwf h simp [compiled_RPSlist100_element, compiled_RPSlist100_element'] - + rw_local compiled_RPSlist100_metadata' = compiled_RPSlist100_metadata by rfl @@ -1871,13 +2047,103 @@ theorem pr : rw_local compiled_RPSStudent100_element' = compiled_RPSStudent100_element by rfl - + simp [ElementTree.eval, ElementTree.eval', PolicyElement.eval] simp [compiled_RPSlist100_metadata] simp [PolicySet.eval, Target.eval] apply pr' req hsod hwf h -#check ElementTree.Node - (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 [] [])) - [ElementTree.Node - (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 xml_of_decision (decision : Decision) := + match decision with + | Decision.permit => "<Decision>Permit</Decision>" + | Decision.deny => "<Decision>Deny</Decision>" + | Decision.indeterminate => "<Decision>Indeterminate</Decision>" + | Decision.not_applicable => "<Decision>NotApplicable</Decision>" + +def string_of_status_code (code : StatusCode) := + match code with + | StatusCode.ok => "urn:oasis:names:tc:xacml:1.0:status:ok" + | StatusCode.missing_attribute => "urn:oasis:names:tc:xacml:1.0:status:missing-attribute" + | StatusCode.syntax_error => "urn:oasis:names:tc:xacml:1.0:status:syntax-error" + | StatusCode.processing_error => "urn:oasis:names:tc:xacml:1.0:status:processing-error" + +def xml_of_status (status : List StatusCode) := + match status with + | primary :: rest => String.join ["<Status Value=\"", string_of_status_code primary, "\">", xml_of_status rest, "</Status>"] + | _ => "" + +def xml_of_xmltype : XmlType -> String + | XmlType.string => "http://www.w3.org/2001/XMLSchema#string" + | XmlType.boolean => "http://www.w3.org/2001/XMLSchema#boolean" + | XmlType.integer => "http://www.w3.org/2001/XMLSchema#integer" + | XmlType.double => "http://www.w3.org/2001/XMLSchema#double" + | XmlType.time => "http://www.w3.org/2001/XMLSchema#time" + | XmlType.date => "http://www.w3.org/2001/XMLSchema#date" + | XmlType.dateTime => "http://www.w3.org/2001/XMLSchema#dateTime" + | XmlType.dayTimeDuration => "http://www.w3.org/2001/XMLSchema#dayTimeDuration" + | XmlType.yearMonthDuration => "http://www.w3.org/2001/XMLSchema#yearMonthDuration" + | XmlType.anyURI => "http://www.w3.org/2001/XMLSchema#anyURI" + | XmlType.hexBinary => "http://www.w3.org/2001/XMLSchema#hexBinary" + | XmlType.base64Binary => "http://www.w3.org/2001/XMLSchema#base64Binary" + | XmlType.rfc822Name => "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name" + | XmlType.x500Name => "urn:oasis:names:tc:xacml:1.0:data-type:x500Name" + | XmlType.ipAddress => "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress" + | XmlType.dnsName => "urn:oasis:names:tc:xacml:2.0:data-type:dnsName" + +def xml_of_attribute_assignment (assignment : Attribute) := + String.join [ + "<AttributeAssignment AttributeId=\"", + assignment.identifier, + "\" DataType=\"", + xml_of_xmltype assignment.value.fst, + "\" Category=\"", + assignment.category, + (match assignment.issuer with + | some issuer => String.join ["\" Category=\"", assignment.category] + | none => ""), + "\">", + "</AttributeAssignment>" + ] + +def xml_of_obligation (obligation : Obligation) := + String.join [ + "<Obligation ObligationId=\"", + obligation.identifier, + "\">", + String.join (List.map xml_of_attribute_assignment obligation.assignments), + "</Obligation>" + ] + +def xml_of_obligations (obligations : List Obligation) := + String.join ["<Obligations>", String.join (List.map xml_of_obligation obligations), "</Obligations>"] + +def xml_of_advice (advice : Advice) := + String.join [ + "<Advice AdviceId=\"", + advice.identifier, + "\">", + String.join (List.map xml_of_attribute_assignment advice.assignments), + "</Advice>" + ] + +def xml_of_advices (advices : List Advice) := + String.join ["<AssociatedAdvice>", String.join (List.map xml_of_advice advices), "</AssociatedAdvices>"] + +def xml_of_response (response : Result) := + String.join [ + "<Response>", + xml_of_decision response.fst, + (match response.snd with + | some {status, obligations, advice} => + String.join [ + (match status with + | some status => xml_of_status status + | none => ""), + xml_of_obligations obligations, + xml_of_advices advice + ] + | none => ""), + "</Response>"] + +def request := ([(Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject" "urn:oasis:names:tc:xacml:1.0:subject:subject-id" none (XmlType.rfc822Name, "bs@simpsons.com")), (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "urn:oasis:names:tc:xacml:1.0:resource:resource-id" none (XmlType.anyURI, "file://example/med/record/patient/BartSimpson")), (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "urn:oasis:names:tc:xacml:1.0:action:action-id" none (XmlType.string, "read"))]) +#eval xml_of_response (Decision'.not_applicable, none) |