Introduce XacmlValue

1 files changed, 129 insertions, 34 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index b8381e1..7c5ece5 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -1,8 +1,35 @@
+inductive XacmlType
+  | string            : XacmlType
+  | boolean           : XacmlType
+  | integer           : XacmlType
+  | double            : XacmlType
+  | time              : XacmlType
+  | date              : XacmlType
+  | dateTime          : XacmlType
+  | anyURI            : XacmlType
+  | hexBinary         : XacmlType
+  | base64Binary      : XacmlType
+  | dayTimeDuration   : XacmlType
+  | yearMonthDuration : XacmlType
+  | x500Name          : XacmlType
+  | rfc822Name        : XacmlType
+  | ipAddress         : XacmlType
+  | dnsName           : XacmlType
+  | xpathExpression   : XacmlType
+deriving BEq, Repr
+
+def XacmlValue : Type := XacmlType × String
+deriving BEq, Repr
+
+def XacmlValue.mk (type : XacmlType) (inner : String) : XacmlValue := (type, inner)
+
+---
+
 structure Attribute where
   category : String
   identifier: String
   issuer : Option String
-  value : List String
+  value : List XacmlValue
 deriving Repr
 
 def Request : Type := List Attribute
@@ -11,10 +38,13 @@ deriving Repr
 ---
 
 inductive Decision where
-  | permit : Decision
-  | deny : Decision
-  | indeterminate : Decision
-  | not_applicable : Decision
+  | permit           : Decision
+  | deny             : Decision
+  | indeterminate    : Decision
+  | indeterminate_d  : Decision
+  | indeterminate_p  : Decision
+  | indeterminate_dp : Decision
+  | not_applicable   : Decision
 deriving Repr
 
 def Response : Type := Decision
@@ -22,6 +52,9 @@ deriving Repr
 
 ---
 
+def Identifier : Type := String
+deriving BEq
+
 inductive CombinatorAlgorithm where
   | deny_overrides                  : CombinatorAlgorithm
   | ordered_deny_overrides          : CombinatorAlgorithm
@@ -36,35 +69,33 @@ inductive CombinatorAlgorithm where
   | legacy_permit_overrides         : CombinatorAlgorithm
   | legacy_ordered_permit_overrides : CombinatorAlgorithm
 
-inductive MatchAlgorithm where
-  | x500Name_match          : MatchAlgorithm
-  | rfc822Name_match        : MatchAlgorithm
-  | string_regexp_match     : MatchAlgorithm
-  | anyURI_regexp_match     : MatchAlgorithm
-  | ipAddress_regexp_match  : MatchAlgorithm
-  | dnsName_regexp_match    : MatchAlgorithm
-  | rfc822Name_regexp_match : MatchAlgorithm
-  | x500Name_regexp_match   : MatchAlgorithm
-  | xpath_node_count        : MatchAlgorithm
-  | xpath_node_equal        : MatchAlgorithm
-  | xpath_node_match        : MatchAlgorithm
-
 structure AttributeDesignator where
   category        : String
   identifier      : String
-  type            : String
+  type            : XacmlType
   issuer          : Option String
   must_be_present : Bool
+deriving BEq
 
 def FunctionID : Type := String
 
+inductive Expression where
+  | apply                (function : FunctionID) (args: List Expression) : Expression
+  | attribute_designator (inner : AttributeDesignator)                   : Expression
+  | attribute_value      (inner : XacmlValue)                            : Expression
+  | function             (function : FunctionID)                         : Expression
+
 structure Match where
-  function : MatchAlgorithm
+  function : Identifier
   designator: AttributeDesignator
-  value: List String
+  value: List XacmlValue
+deriving BEq
 def AllOf : Type  := List Match -- TODO: Should restrict nonempty.
+deriving BEq
 def AnyOf : Type  := List AllOf -- TODO: Should restrict nonempty.
+deriving BEq
 def Target : Type := List AnyOf
+deriving BEq
 
 structure Rule where
   target : Target
@@ -88,16 +119,10 @@ inductive PolicySetChild where
 structure Policy where
   combinator : CombinatorAlgorithm
   target : Target
-  children : List Rule
+  rules : List Rule
   -- TODO: ObligationExpressions
   -- TODO: AdviceExpressions
 
-inductive Expression where
-  | apply                (function : FunctionID) (args: List Expression) : Expression
-  | attribute_designator (inner : AttributeDesignator)                   : Expression
-  | attribute_value      (inner : String)                                : Expression
-  | function             (function : FunctionID)                         : Expression
-
 ---
 
 def example_4_1_policy :=
@@ -106,14 +131,14 @@ def example_4_1_policy :=
     []
     [Rule.mk
       [[[Match.mk
-          MatchAlgorithm.rfc822Name_match
+          "rfc822Name_match"
           (AttributeDesignator.mk
             "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
             "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
-            "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"
+            XacmlType.rfc822Name
             Option.none
             false)
-          ["med.example.com"]]]]
+          [XacmlValue.mk XacmlType.string "med.example.com"]]]]
       Option.none
       Decision.permit]
 
@@ -121,14 +146,84 @@ def example_4_1_request :=
   [Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
                 "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
                 Option.none
-                ["bs@simpsons.com"],
+                [XacmlValue.mk XacmlType.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"
                 Option.none
-                ["file://example/med/record/patient/BartSimpson"],
+                [XacmlValue.mk XacmlType.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"
                 Option.none
-                ["read"]]
+                [XacmlValue.mk XacmlType.string "read"]]
 
 def example_4_1_response := Decision.not_applicable
+
+---
+
+def example_4_2_policy :=
+  Policy.mk
+    CombinatorAlgorithm.deny_overrides
+    []
+    [Rule.mk
+      [[[Match.mk
+          "anyURI_equal"
+          (AttributeDesignator.mk
+            "urn:oasis:names:tc:xacml:3.0:subject-category:resource"
+            "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
+            XacmlType.rfc822Name
+            Option.none
+            false)
+          [XacmlValue.mk XacmlType.anyURI "urn:example:med:schemas:record"],
+        Match.mk
+          "xpath_node_match"
+          (AttributeDesignator.mk
+            "urn:oasis:names:tc:xacml:3.0:subject-category:resource"
+            "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
+            XacmlType.xpathExpression
+            Option.none
+            false)
+          [XacmlValue.mk XacmlType.xpathExpression "md:record"]],
+        [Match.mk
+          "string_equal"
+          (AttributeDesignator.mk
+            "urn:oasis:names:tc:xacml:3.0:subject-category:action"
+            "urn:oasis:names:tc:xacml:1.0:action:action-id"
+            XacmlType.string
+            Option.none
+            false)
+          [XacmlValue.mk XacmlType.string "read"]]]]
+      (Expression.apply
+        "urn:oasis:names:tc:xacml:1.0:function:string-equal"
+        [Expression.apply
+          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
+          [Expression.attribute_designator
+            (AttributeDesignator.mk
+              "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
+              "urn:oasis:names:tc:xacml:3.0:example:attribute:patient-number"
+              XacmlType.string
+              Option.none
+              false)],
+          Expression.apply
+          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
+          [Expression.attribute_designator
+            (AttributeDesignator.mk
+              "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
+              "md:record/md:patient/md:patient-number/text()"
+              XacmlType.string
+              Option.none
+              false)]])
+      Decision.permit]
+
+---
+
+def Choice : Type := List Decision
+
+def evaluate_rule (rule : Rule) (context : Request) : Choice :=
+  if rule.target == [] then [rule.effect] else []
+
+def evaluate_policy (policy : Policy) (context : Request) : Choice :=
+  match policy.rules with
+    | [rule₁] => evaluate_rule rule₁ context
+    | _ => []
+
+#eval evaluate_policy example_4_1_policy example_4_1_request