Verify Always Denies is sound
Cedar.Thm.verifyAlwaysDenies_is_sound
Plain-language statement
The verifyAlwaysDenies analysis is sound: if the assertions verifyAlwaysDenies ps₁ εnv are unsatisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then the authorizer will return deny when applied to ps₁ and any strongly well-formed concrete environment env ∈ᵢ εnv.
Exact Lean statement
theorem verifyAlwaysDenies_is_sound {ps₁ : Policies} {εnv : SymEnv} {asserts : Asserts} :
εnv.StronglyWellFormedForPolicies ps₁ →
verifyAlwaysDenies ps₁ εnv = .ok asserts →
εnv ⊭ asserts →
∀ env,
env ∈ᵢ εnv →
env.StronglyWellFormedForPolicies ps₁ →
denies (Spec.isAuthorized env.request env.entities ps₁)Formal artifact
Lean source
theorem verifyAlwaysDenies_is_sound {ps₁ : Policies} {εnv : SymEnv} {asserts : Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → verifyAlwaysDenies ps₁ εnv = .ok asserts → εnv ⊭ asserts → ∀ env, env ∈ᵢ εnv → env.StronglyWellFormedForPolicies ps₁ → denies (Spec.isAuthorized env.request env.entities ps₁):= by intro hwε₁ hvc hsat env hin hwe₁ unfold verifyAlwaysDenies at hvc rw [denies_eq_implies_false _ env] exact verifyIsAuthorized_is_sound verifyImplies_wbaq hwε₁ (swf_εnv_for_empty_policies hwε₁.left) hvc hsat env hin hwe₁ (swf_env_for_empty_policies hwe₁.left)- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/Verification.lean:588-602
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.