This file proves that verifyIsAuthorized queries are well-behaved.

def Cedar.Thm.bothAllowOrBothDeny (r₁ r₂ : Spec.Response) : Bool

Equations

• Cedar.Thm.bothAllowOrBothDeny r₁ r₂ = decide (r₁.decision = r₂.decision)

theorem Cedar.Thm.verifyEquivalent_wbaq : WellBehavedIsAuthorizedQuery SymCC.Factory.eq bothAllowOrBothDeny

def Cedar.Thm.atLeastOneDenies (r₁ r₂ : Spec.Response) : Bool

Equations

• Cedar.Thm.atLeastOneDenies r₁ r₂ = !(decide (r₁.decision = Cedar.Spec.Decision.allow) && decide (r₂.decision = Cedar.Spec.Decision.allow))

theorem Cedar.Thm.verifyDisjoint_wbaq : WellBehavedIsAuthorizedQuery SymCC.verifyDisjoint.disjoint atLeastOneDenies

def Cedar.Thm.ifFirstAllowsSoDoesSecond (r₁ r₂ : Spec.Response) : Bool

Equations

• Cedar.Thm.ifFirstAllowsSoDoesSecond r₁ r₂ = (r₁.decision != Cedar.Spec.Decision.allow || decide (r₂.decision = Cedar.Spec.Decision.allow))

theorem Cedar.Thm.verifyImplies_wbaq : WellBehavedIsAuthorizedQuery SymCC.Factory.implies ifFirstAllowsSoDoesSecond

def Cedar.Thm.denies (r₁ : Spec.Response) : Bool

Equations

• Cedar.Thm.denies r₁ = decide (r₁.decision = Cedar.Spec.Decision.deny)

theorem Cedar.Thm.isAuthorized_empty_denies (env : Spec.Env) : (Spec.isAuthorized env.request env.entities []).decision = Spec.Decision.deny

theorem Cedar.Thm.denies_eq_implies_false (r₁ : Spec.Response) (env : Spec.Env) : denies r₁ = ifFirstAllowsSoDoesSecond r₁ (Spec.isAuthorized env.request env.entities [])

theorem Cedar.Thm.swf_εnv_for_empty_policies {εnv : SymCC.SymEnv} : εnv.StronglyWellFormed → εnv.StronglyWellFormedForPolicies []

theorem Cedar.Thm.swf_env_for_empty_policies {env : Spec.Env} : env.StronglyWellFormed → env.StronglyWellFormedForPolicies []

def Cedar.Thm.allows (r₁ : Spec.Response) : Bool

Equations

• Cedar.Thm.allows r₁ = decide (r₁.decision = Cedar.Spec.Decision.allow)

theorem Cedar.Thm.isAuthorized_allowAll_allows (env : Spec.Env) : (Spec.isAuthorized env.request env.entities [SymCC.verifyAlwaysAllows.allowAll]).decision = Spec.Decision.allow

theorem Cedar.Thm.allows_eq_allowAll_implies (r₁ : Spec.Response) (env : Spec.Env) : allows r₁ = ifFirstAllowsSoDoesSecond (Spec.isAuthorized env.request env.entities [SymCC.verifyAlwaysAllows.allowAll]) r₁

theorem Cedar.Thm.swf_εnv_for_allowAll_policies {εnv : SymCC.SymEnv} : εnv.StronglyWellFormed → εnv.StronglyWellFormedForPolicies [SymCC.verifyAlwaysAllows.allowAll]

theorem Cedar.Thm.swf_env_for_allowAll_policies {env : Spec.Env} : env.StronglyWellFormed → env.StronglyWellFormedForPolicies [SymCC.verifyAlwaysAllows.allowAll]