Is Authorized is complete
Cedar.Thm.isAuthorized_is_complete
Project documentation
Let ps be Cedar policies and εnv a symbolic environment, where ps and εnv are a well-formed input to the symbolic authorizer, i.e., εnv.WellFormedForPolicies ps. Let t the outcome of symbolically authorizing ps with respect to εnv, and d a concrete authorization decision represented by t. Then, the completeness theorem says that there...
Exact Lean statement
theorem isAuthorized_is_complete {ps : Policies} {εnv : SymEnv} {t : Term.Outcome εnv} {decision : Spec.Decision} :
εnv.WellFormedForPolicies ps →
SymCC.isAuthorized ps εnv = .ok t →
decision ∈ₒ t →
∃ (env : Env),
env.WellFormedForPolicies ps ∧
env ∈ᵢ εnv ∧
Spec.isAuthorized env.request env.entities ps ∼ decisionFormal artifact
Lean source
theorem isAuthorized_is_complete {ps : Policies} {εnv : SymEnv} {t : Term.Outcome εnv} {decision : Spec.Decision} : εnv.WellFormedForPolicies ps → SymCC.isAuthorized ps εnv = .ok t → decision ∈ₒ t → ∃ (env : Env), env.WellFormedForPolicies ps ∧ env ∈ᵢ εnv ∧ Spec.isAuthorized env.request env.entities ps ∼ decision:= by intro hεnv hok hinₒ replace ⟨I, hI, hinₒ⟩ := hinₒ have ⟨env, heq, henv⟩ := exists_wf_env_for_policies hεnv hI exists env simp only [henv, true_and] constructor · exists I · replace heq := isAuthorized_bisimulation hεnv henv hI heq hok exact same_decision_and_response_implies_same_decision hinₒ heq- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/SymbolicCompilation.lean:183-200
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.