This file contains basic theorems about Cedar's authorizer.

def Cedar.Thm.PolicyIdsUnique (policies : Spec.Policies) : Prop

Equations

• Cedar.Thm.PolicyIdsUnique policies = ∀ (p₁ : Cedar.Spec.Policy), p₁ ∈ policies → ∀ (p₂ : Cedar.Spec.Policy), p₂ ∈ policies → p₁.id = p₂.id → p₁ = p₂

def Cedar.Thm.HasSatisfiedEffect (effect : Spec.Effect) (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : Prop

Equations

• Cedar.Thm.HasSatisfiedEffect effect request entities policies = ∃ (policy : Cedar.Spec.Policy), policy ∈ policies ∧ policy.effect = effect ∧ Cedar.Spec.satisfied policy request entities = true

theorem Cedar.Thm.satisfied_iff_satisfiedPolicies_non_empty {effect : Spec.Effect} {request : Spec.Request} {entities : Spec.Entities} {policies : Spec.Policies} : HasSatisfiedEffect effect request entities policies ↔ (Spec.satisfiedPolicies effect policies request entities).isEmpty = false

def Cedar.Thm.IsExplicitlyForbidden (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : Prop

A request is explicitly forbidden when there is at least one satisfied forbid policy.

Equations

• Cedar.Thm.IsExplicitlyForbidden = Cedar.Thm.HasSatisfiedEffect Cedar.Spec.Effect.forbid

theorem Cedar.Thm.explicitly_forbidden_iff_satisfying_forbid {req : Spec.Request} {entities : Spec.Entities} {policies : Spec.Policies} : IsExplicitlyForbidden req entities policies ↔ (Spec.satisfiedPolicies Spec.Effect.forbid policies req entities).isEmpty = false

def Cedar.Thm.IsExplicitlyPermitted (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : Prop

A request is explicitly permitted when there is at least one satisfied permit policy. Note that there may still be satisfied forbid policies leading to a deny decisions.

Equations

• Cedar.Thm.IsExplicitlyPermitted = Cedar.Thm.HasSatisfiedEffect Cedar.Spec.Effect.permit

theorem Cedar.Thm.explicitly_permitted_iff_satisfying_permit {req : Spec.Request} {entities : Spec.Entities} {policies : Spec.Policies} : IsExplicitlyPermitted req entities policies ↔ (Spec.satisfiedPolicies Spec.Effect.permit policies req entities).isEmpty = false

theorem Cedar.Thm.forbid_trumps_permit (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : IsExplicitlyForbidden request entities policies → (Spec.isAuthorized request entities policies).decision = Spec.Decision.deny

Forbid trumps permit: if a forbid policy is satisfied, the request is denied.

theorem Cedar.Thm.allowed_only_if_explicitly_permitted (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : (Spec.isAuthorized request entities policies).decision = Spec.Decision.allow → IsExplicitlyPermitted request entities policies

A request is allowed only if it is explicitly permitted.

theorem Cedar.Thm.default_deny (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : ¬IsExplicitlyPermitted request entities policies → (Spec.isAuthorized request entities policies).decision = Spec.Decision.deny

Default deny: if not explicitly permitted, the request is denied. This is contrapositive of allowed_only_if_explicitly_permitted.

theorem Cedar.Thm.allowed_iff_explicitly_permitted_and_not_denied (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : IsExplicitlyPermitted request entities policies ∧ ¬IsExplicitlyForbidden request entities policies ↔ (Spec.isAuthorized request entities policies).decision = Spec.Decision.allow

A request is allowed if and only if it is explicitly permitted and is not explicitly forbidden.

theorem Cedar.Thm.denied_iff_explicitly_denied_or_not_permitted (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : IsExplicitlyForbidden request entities policies ∨ ¬IsExplicitlyPermitted request entities policies ↔ (Spec.isAuthorized request entities policies).decision = Spec.Decision.deny

A request is denied if and only if it is explicitly denied or it is not explicitly permitted.

theorem Cedar.Thm.order_and_dup_independent (request : Spec.Request) (entities : Spec.Entities) (policies₁ policies₂ : Spec.Policies) : policies₁ ≡ policies₂ → Spec.isAuthorized request entities policies₁ = Spec.isAuthorized request entities policies₂

Order and duplicate independence: isAuthorized produces the same result regardless of policy order or duplicates.

theorem Cedar.Thm.unchanged_allow_when_add_permit (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) (policy₂ : Spec.Policy) : policy₂.effect = Spec.Effect.permit → (Spec.isAuthorized request entities policies).decision = Spec.Decision.allow → (Spec.isAuthorized request entities (policy₂ :: policies)).decision = Spec.Decision.allow

Adding a permit policy won't change an Allow decision.

theorem Cedar.Thm.unchanged_deny_when_add_forbid (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) (policy₂ : Spec.Policy) : policy₂.effect = Spec.Effect.forbid → (Spec.isAuthorized request entities policies).decision = Spec.Decision.deny → (Spec.isAuthorized request entities (policy₂ :: policies)).decision = Spec.Decision.deny

Adding a forbid policy won't change a Deny decision.

theorem Cedar.Thm.determiningPolicies_of (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : have auth := Spec.isAuthorized request entities policies; auth.determiningPolicies = Spec.satisfiedPolicies (if auth.decision = Spec.Decision.allow then Spec.Effect.permit else Spec.Effect.forbid) policies request entities

The determining policies of a allow/deny decision are exactly the satisfied policies of permit/forbid resp.

theorem Cedar.Thm.unchanged_determining_when_add_policy_and_decision_unchanged (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) (policy₀ : Spec.Policy) : have auth := Spec.isAuthorized request entities policies; have auth' := Spec.isAuthorized request entities (policy₀ :: policies); auth.decision = auth'.decision → auth.determiningPolicies ⊆ auth'.determiningPolicies

If P is a determining policy, then adding a new policy resulting in the same decision won't change that.

theorem Cedar.Thm.unchanged_erroring_when_add_policy (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) (policy₀ : Spec.Policy) : (Spec.isAuthorized request entities policies).erroringPolicies ⊆ (Spec.isAuthorized request entities (policy₀ :: policies)).erroringPolicies

If P is an erroring policy, then adding another policy won’t change that (even if the decision changes).

theorem Cedar.Thm.determining_erroring_disjoint_when_unique_ids (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : PolicyIdsUnique policies → ((Spec.isAuthorized request entities policies).determiningPolicies ∩ (Spec.isAuthorized request entities policies).erroringPolicies).isEmpty = true

Determining policies and erroring policies of an isAuthorized response are disjoint when input policy IDs are unique.