diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 83 |
1 files changed, 80 insertions, 3 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 8464aa0..8a7a40e 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -14,6 +14,19 @@ inductive MatchResult where | indeterminate : MatchResult deriving BEq, Repr +def MatchResult.or : MatchResult -> MatchResult -> MatchResult + | MatchResult.indeterminate , _ => MatchResult.indeterminate + | _ , MatchResult.indeterminate => MatchResult.indeterminate + | MatchResult.is_match , _ => MatchResult.is_match + | _ , MatchResult.is_match => MatchResult.is_match + | MatchResult.no_match , MatchResult.no_match => MatchResult.no_match + +def MatchResult.and : MatchResult -> MatchResult -> MatchResult + | MatchResult.indeterminate , _ => MatchResult.indeterminate + | _ , MatchResult.indeterminate => MatchResult.indeterminate + | MatchResult.is_match , MatchResult.is_match => MatchResult.is_match + | _ , _ => MatchResult.no_match + inductive Decision where | permit : Decision | deny : Decision @@ -147,6 +160,13 @@ instance : Coe (Option Value) Value where | Option.none => Value.primitive (#<XmlType.boolean, "Indeterminate">) | Option.some a => a +instance : Coe (Option Value) MatchResult where + coe b := + match b with + | Option.some (Value.primitive (XmlType.boolean, "True")) => MatchResult.is_match + | Option.some (Value.primitive (XmlType.boolean, "False")) => MatchResult.no_match + | _ => MatchResult.indeterminate + ------------------------------------------------------------------------ ---- Attributes--------------------------------------------------------- ------------------------------------------------------------------------ @@ -324,23 +344,80 @@ namespace Match do let result <- designator.eval context let results := match result with + -- Otherwise, the MatchId function SHALL be applied between the + -- <AttributeValue> and each element of the bag returned from the + -- <AttributeDesignator> or <AttributeSelector> element. | (Value.bag (Bag.mk attrs)) => - attrs.map - fun attr => + attrs.map fun attr => let args := [value, Value.primitive attr] (Expression.apply fn args).eval context | (Value.primitive attr) => + -- TODO: Prove that this case is impossible. let args := [value, Value.primitive attr] [(Expression.apply fn args).eval context] let results := results.map (fun (x : Option Value) => (x : Value)) + -- If at least one of those function applications were to evaluate to + -- "True", then the result of the entire expression SHALL be "True". if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then (Value.primitive (#<XmlType.boolean, "True">)) + -- Otherwise, if at least one of the function applications results in + -- "Indeterminate", then the result SHALL be "Indeterminate". else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then (Value.primitive (#<XmlType.boolean, "Indeterminate">)) - else Value.primitive (#<XmlType.boolean, "False">) + -- The `else` arm handles the following cases: + -- + -- If the <AttributeDesignator> or <AttributeSelector> element were to + -- evaluate to an empty bag, then the result of the expression SHALL + -- be "False". + -- + -- Finally, if all function applications evaluate to "False", then the + -- result of the entire expression SHALL be "False". + else + Value.primitive (#<XmlType.boolean, "False">) + -- If an operational error were to occur while evaluating the + -- <AttributeDesignator> or <AttributeSelector> element, then the result + -- of the entire expression SHALL be "Indeterminate". + -- + -- In our case, this is handled by the Option monad, since the assignment + -- to `result` would fail. end Match +namespace AllOf + -- There is no section specifying the semantics of `AllOf`. + def eval (conj : AllOf) (context : Request) : MatchResult := + (conj.map (fun m => m.eval context)).foldl + MatchResult.and + MatchResult.no_match +end AllOf + +namespace AnyOf + -- There is no section specifying the semantics of `AnyOf`. + def eval (disj : AnyOf) (context : Request) : MatchResult := + (disj.map (fun conj => conj.eval context)).foldl + MatchResult.or + MatchResult.is_match +end AnyOf + +namespace Target + def eval (target : Target) (context : Request) : MatchResult := + match target with + -- An empty target matches any request. + | [] => MatchResult.is_match + | xs => + let results := xs.map (fun disj => disj.eval context) + -- Otherwise the target value SHALL be "Match" if all the AnyOf + -- specified in the target match values in the request context. + if results.all (fun result => result == MatchResult.is_match) then + MatchResult.is_match + -- Otherwise, if any one of the AnyOf specified in the target is “No + -- Match”, then the target SHALL be “No Match”. + else if results.any (fun result => result == MatchResult.no_match) then + MatchResult.no_match + -- Otherwise, the target SHALL be “Indeterminate”. + else MatchResult.indeterminate +end Target + structure AttributeAssignment where category : String identifier : String |