Partial authorize no satisfied forbids if allow
Cedar.Thm.partial_authorize_no_satisfied_forbids_if_allow
Project documentation
Like partial_authorize_satisfied_permits_not_determining_if_deny for forbid policies, but we can prove a stronger theorem because any satisfied forbid causes the decision to be deny. If the result of concrete authorization is allow, then there can be no satisfied forbid policies after partial authorization.
Exact Lean statement
theorem partial_authorize_no_satisfied_forbids_if_allow
{schema : Schema}
{policies : List Policy}
{req : Request}
{es : Entities}
{preq : PartialRequest}
{pes : PartialEntities}
{response : TPE.Response} :
TPE.isAuthorized schema policies preq pes = Except.ok response →
isValidAndConsistent schema req es preq pes = Except.ok () →
(Spec.isAuthorized req es policies).decision = .allow →
response.satisfiedForbids.isEmptyFormal artifact
Lean source
theorem partial_authorize_no_satisfied_forbids_if_allow {schema : Schema} {policies : List Policy} {req : Request} {es : Entities} {preq : PartialRequest} {pes : PartialEntities} {response : TPE.Response} : TPE.isAuthorized schema policies preq pes = Except.ok response → isValidAndConsistent schema req es preq pes = Except.ok () → (Spec.isAuthorized req es policies).decision = .allow → response.satisfiedForbids.isEmpty:= by intro h₁ h₂ h₃ rw [←allowed_iff_explicitly_permitted_and_not_denied] at h₃ apply Set.superset_empty_subset_empty (partial_authorize_satisfied_forbids_is_sound h₁ h₂) simpa [explicitly_forbidden_iff_satisfying_forbid] using h₃.right- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/TPE.lean:265-281
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Find? ext
Cedar.Data.Map.find?_ext
Plain-language statement
Two well-formed maps are equal if they have the same find? for every key.
Source project: Cedar Specification
Person-level attribution pending.
Find? notmem keys
Cedar.Data.Map.find?_notmem_keys
Plain-language statement
Inverse of find?_mem_toList, except that this requires wf
Source project: Cedar Specification
Person-level attribution pending.
Find? some iff in values
Cedar.Data.Map.find?_some_iff_in_values
Plain-language statement
The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above
Source project: Cedar Specification
Person-level attribution pending.