diff options
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 99 |
1 files changed, 33 insertions, 66 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 378d3aa..6623c4c 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -1485,7 +1485,8 @@ theorem attribute_designator_eval (attr : Attribute) (s : String) (req : List At rw [←h'] assumption -theorem match_eval (attr : Attribute) (s : String) (req : Request) : +def match_eval (req : Request) := + ∀ (attr : Attribute) (s : String), attr.value = (XmlType.string, s) → req.elem attr → Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1496,51 +1497,13 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) : 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 - 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) => - simp - sorry -- contradiction by designator_always_returns_bag - | Sum.inl (Value.bag (Bag.mk attrs)) => - simp - let f := ((fun x => - match x with - | none => Value.primitive (#<XmlType.boolean,"Indeterminate">) - | some a => a) ∘ - fun attr => - Expression.eval - (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" - [Value.primitive (XmlType.string, s), Value.primitive attr]) - req) - have h_asdf : attr.value ∈ attrs := by - apply attribute_designator_eval - apply h₁ - apply h₂ - sorry - sorry - -- have h_branch : - -- List.elem (Value.primitive (#<XmlType.boolean,"True">)) - -- (List.map f attrs) = - -- true := by - - -- | nil => contradiction - | Sum.inr _ => sorry - -- wts: eval results in a list with the attribute in it - -- wts: streq map containing attribute contains true + req = some (Value.primitive (XmlType.boolean, "True")) -- 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")) + match_eval 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, "InternalGrades")) → AllOf.eval [{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1554,7 +1517,7 @@ theorem pr₂_lemma₀ (req : Request) : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Assign") }] req = MatchResult.is_match := by - intros h₁ h₂ + intros hme h₁ h₂ simp [AllOf.eval] rw_local Match.eval @@ -1566,9 +1529,8 @@ theorem pr₂_lemma₀ (req : Request) : 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₂' + apply hme attr "InternalGrades" (by rfl) h₂' rw_local Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1579,12 +1541,12 @@ theorem pr₂_lemma₀ (req : Request) : 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₁' + apply hme attr "Assign" (by rfl) 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")) + match_eval 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, "InternalGrades")) → Target.eval [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1628,7 +1590,7 @@ theorem pr₂_lemma₁ (req : Request) : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "View") }]]] req = MatchResult.is_match := by - intros h₂ h₃ + intros hme h₂ h₃ simp [Target.eval, AnyOf.eval] cases (AllOf.eval [{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal", @@ -1661,13 +1623,14 @@ theorem pr₂_lemma₁ (req : Request) : must_be_present := true }, value := Value.primitive (XmlType.string, "Assign") }] req = MatchResult.is_match - by apply pr₂_lemma₀ req h₂ h₃ + by apply pr₂_lemma₀ req hme 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")) + match_eval 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, "InternalGrades")) → (ElementTree.eval' req compiled_facassignviewgrades_element []).fst = Decision'.permit := by - intros h₂ h₃ + intros hme h₂ h₃ simp [compiled_facassignviewgrades_element, compiled_facassignviewgrades_metadata] simp [ElementTree.eval, ElementTree.eval', @@ -1716,11 +1679,12 @@ theorem pr₂_lemma₂ (req : Request) : 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₃ + by apply pr₂_lemma₁ req hme 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")) + match_eval req + → 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 := @@ -1728,7 +1692,7 @@ theorem pr₂_lemma₃ (req : Request) : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Faculty") }] req = MatchResult.is_match := by - intro h₁ + intro hme h₁ simp [AllOf.eval] rw_local Match.eval @@ -1742,10 +1706,11 @@ theorem pr₂_lemma₃ (req : Request) : 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₂' + apply hme attr "Faculty" 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")) + match_eval req + → 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 := @@ -1753,7 +1718,7 @@ theorem pr₂_lemma₄ (req : Request) : type := XmlType.string, issuer := none, must_be_present := true }, value := Value.primitive (XmlType.string, "Faculty") }]]] req = MatchResult.is_match := by - intros h₁ + intros hme h₁ simp [Target.eval, AnyOf.eval] rw_local (AllOf.eval @@ -1763,14 +1728,15 @@ theorem pr₂_lemma₄ (req : Request) : 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₁ + by apply pr₂_lemma₃ req hme 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")) + match_eval req + → 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₃ + intros hme h₁ h₂ h₃ simp [compiled_fac100_element, compiled_fac100_metadata] simp [ElementTree.eval, ElementTree.eval', @@ -1785,19 +1751,20 @@ theorem pr₂_lemma₅ (req : Request) : 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₁ + by apply pr₂_lemma₄ req hme 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₃ + by apply pr₂_lemma₂ req hme 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")) + match_eval req + → 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₃ + intros hme h₁ h₂ h₃ simp [compiled_college100_element, compiled_college100_metadata, ElementTree.eval, @@ -1808,7 +1775,7 @@ theorem pr₂ (req : Request) : PolicyCombinatorAlgorithm.eval_legacy_permit_overrides] rw_local (ElementTree.eval' req compiled_fac100_element []).fst = Decision'.permit - by apply pr₂_lemma₅ req h₁ h₂ h₃ + by apply pr₂_lemma₅ req hme h₁ h₂ h₃ -- Pr1: There do not exist members of Student who can Assign ExternalGrades. (This is violated, so we show a counterexample.) |