This file connects soundness theorems in Cedar.Thm.Verification with policy validation.

We prove that if validation of a policy (set) succeeds in the sense of wellTypedPolicy/wellTypedPolicies), then various verification tasks would produce a symbolic encoding without errors, and is sound with respect to concrete Envs.

theorem Cedar.Thm.verifyNeverErrors_is_ok_and_sound {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverErrors p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p' → Except.isOk (Spec.evaluate p.toExpr env.request env.entities) = true)

Concrete version of verifyNeverErrors_is_sound.

NOTE: This theorem and many of the following soundness theorems use env.StronglyWellFormedForPolicy p' in the conclusion rather than env.StronglyWellFormedForPolicy p.

One can obtain a weaker version with env.StronglyWellFormedForPolicy p, using the lemma wellTypedPolicy_preserves_StronglyWellFormedForPolicy.

theorem Cedar.Thm.verifyNeverErrors_is_ok_and_complete {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverErrors p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p' ∧ ¬Except.isOk (Spec.evaluate p.toExpr env.request env.entities) = true)

Concrete version of verifyNeverErrors_is_complete.

theorem Cedar.Thm.verifyAlwaysMatches_is_ok_and_sound {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p' → Spec.evaluate p.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyAlwaysMatches_is_sound.

theorem Cedar.Thm.verifyAlwaysMatches_is_ok_and_complete {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p' ∧ Spec.evaluate p.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyAlwaysMatches_is_complete.

theorem Cedar.Thm.verifyNeverMatches_is_ok_and_sound {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p' → Spec.evaluate p.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyNeverMatches_is_sound.

theorem Cedar.Thm.verifyNeverMatches_is_ok_and_complete {p p' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p Γ = Except.ok p' → ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p' ∧ Spec.evaluate p.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyNeverMatches_is_complete.

theorem Cedar.Thm.verifyMatchesEquivalent_is_ok_and_sound {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesEquivalent p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p₁' → env.StronglyWellFormedForPolicy p₂' → (Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))) = (Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))))

Concrete version of verifyMatchesEquivalent_is_sound.

theorem Cedar.Thm.verifyMatchesEquivalent_is_ok_and_complete {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesEquivalent p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p₁' ∧ env.StronglyWellFormedForPolicy p₂' ∧ (Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))) ≠ (Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))))

Concrete version of verifyMatchesEquivalent_is_complete.

theorem Cedar.Thm.verifyMatchesImplies_is_ok_and_sound {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesImplies p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p₁' → env.StronglyWellFormedForPolicy p₂' → Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) → Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyMatchesImplies_is_sound.

theorem Cedar.Thm.verifyMatchesImplies_is_ok_and_complete {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesImplies p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p₁' ∧ env.StronglyWellFormedForPolicy p₂' ∧ Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyMatchesImplies_is_complete.

theorem Cedar.Thm.verifyMatchesDisjoint_is_ok_and_sound {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesDisjoint p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicy p₁' → env.StronglyWellFormedForPolicy p₂' → ¬(Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))))

Concrete version of verifyMatchesDisjoint_is_sound.

theorem Cedar.Thm.verifyMatchesDisjoint_is_ok_and_complete {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁' → SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesDisjoint p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicy p₁' ∧ env.StronglyWellFormedForPolicy p₂' ∧ Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

Concrete version of verifyMatchesDisjoint_is_complete.

theorem Cedar.Thm.verifyEquivalent_is_ok_and_sound {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyEquivalent ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicies ps₁' → env.StronglyWellFormedForPolicies ps₂' → bothAllowOrBothDeny (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyEquivalent_is_sound.

theorem Cedar.Thm.verifyEquivalent_is_ok_and_complete {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyEquivalent ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicies ps₁' ∧ env.StronglyWellFormedForPolicies ps₂' ∧ ¬bothAllowOrBothDeny (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyEquivalent_is_complete.

theorem Cedar.Thm.verifyDisjoint_is_ok_and_sound {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyDisjoint ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicies ps₁' → env.StronglyWellFormedForPolicies ps₂' → atLeastOneDenies (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyDisjoint_is_sound.

theorem Cedar.Thm.verifyDisjoint_is_ok_and_complete {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyDisjoint ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicies ps₁' ∧ env.StronglyWellFormedForPolicies ps₂' ∧ ¬atLeastOneDenies (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyDisjoint_is_complete.

theorem Cedar.Thm.verifyImplies_is_ok_and_sound {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyImplies ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicies ps₁' → env.StronglyWellFormedForPolicies ps₂' → ifFirstAllowsSoDoesSecond (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyImplies_is_sound.

theorem Cedar.Thm.verifyImplies_is_ok_and_complete {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂' → ∃ (asserts : SymCC.Asserts), SymCC.verifyImplies ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicies ps₁' ∧ env.StronglyWellFormedForPolicies ps₂' ∧ ¬ifFirstAllowsSoDoesSecond (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true)

Concrete version of verifyImplies_is_complete.

theorem Cedar.Thm.verifyAlwaysDenies_is_ok_and_sound {ps₁ ps₁' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysDenies ps₁' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicies ps₁' → denies (Spec.isAuthorized env.request env.entities ps₁) = true)

Concrete version of verifyAlwaysDenies_is_sound.

theorem Cedar.Thm.verifyAlwaysDenies_is_ok_and_complete {ps₁ ps₁' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysDenies ps₁' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicies ps₁' ∧ ¬denies (Spec.isAuthorized env.request env.entities ps₁) = true)

Concrete version of verifyAlwaysDenies_is_complete.

theorem Cedar.Thm.verifyAlwaysAllows_is_ok_and_sound {ps₁ ps₁' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysAllows ps₁' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊭ asserts → ∀ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ → env.StronglyWellFormedForPolicies ps₁' → allows (Spec.isAuthorized env.request env.entities ps₁) = true)

Concrete version of verifyAlwaysAllows_is_sound.

theorem Cedar.Thm.verifyAlwaysAllows_is_ok_and_complete {ps₁ ps₁' : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁' → ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysAllows ps₁' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts ∧ (SymCC.SymEnv.ofEnv Γ ⊧ asserts → ∃ (env : Spec.Env), InstanceOfWellFormedEnvironment env.request env.entities Γ ∧ env.StronglyWellFormedForPolicies ps₁' ∧ ¬allows (Spec.isAuthorized env.request env.entities ps₁) = true)

Concrete version of verifyAlwaysAllows_is_complete.