Cedar.Thm.TPE

This file defines the main theorem of TPE soundness for authorization.

Significant lemmas proving soundness of policy and expression evaluation are in Cedar.Thm.TPE.Policy and Cedar.Thm.TPE.Soundness.

source

theorem Cedar.Thm.reauthorize_is_sound {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

TPE.isValidAndConsistent schema req es preq pes = Except.ok () → TPE.isAuthorized schema policies preq pes = Except.ok response → response.reauthorize req es = Spec.isAuthorized req es policies

Main re-authorization soundness theorem: The result of reauthorizing a partial authorization response with concrete request and entities is equivalent to directly authorizing with the concrete request and entities.

source

theorem Cedar.Thm.partial_authorize_decision_is_sound {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} {decision : Spec.Decision} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → response.decision = some decision → (Spec.isAuthorized req es policies).decision = decision

Main partial authorization soundness theorem: If partial authorization returns a decision, then concrete authorization will reach the same.

source

theorem Cedar.Thm.partial_re_authorize_decision_eq {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} {decision : Spec.Decision} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → response.decision = some decision → (response.reauthorize req es).decision = decision

Trivial composition of the first two soundness theorems directly relating the decision of partial authorization and subsequent re-authorization.

source

theorem Cedar.Thm.partial_authorize_erroring_policies_is_sound {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → response.errorForbids ∪ response.errorPermits ⊆ (Spec.isAuthorized req es policies).erroringPolicies

All policies reported as erroring after partial authorization will appear in the set of erroring policies after concrete authorization.

source

theorem Cedar.Thm.partial_authorize_allow_determining_policies_is_sound {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → (Spec.isAuthorized req es policies).decision = Spec.Decision.allow → response.satisfiedPermits ⊆ (Spec.isAuthorized req es policies).determiningPolicies

If the result of concrete authorization is allow, then all permit policies satisfied after partial authorization are determining policies.

source

theorem Cedar.Thm.partial_authorize_satisfied_permits_not_determining_if_deny {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → (Spec.isAuthorized req es policies).decision = Spec.Decision.deny → PolicyIdsUnique policies → (response.satisfiedPermits ∩ (Spec.isAuthorized req es policies).determiningPolicies).isEmpty = true

If the result of concrete authorization is deny, then any permit policies satisfied after partial authorization cannot be determining policies.

source

theorem Cedar.Thm.partial_authorize_satisfied_forbid_is_determining {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

TPE.isAuthorized schema policies preq pes = Except.ok response → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → response.satisfiedForbids ⊆ (Spec.isAuthorized req es policies).determiningPolicies

Like partial_authorize_allow_determining_policies_is_sound for forbid policies, but we can prove a stronger theorem because of forbid_trumps_permit. Any forbid policy satisfied after partial evaluation will always be determining.

source

theorem Cedar.Thm.partial_authorize_no_satisfied_forbids_if_allow {schema : Validation.Schema} {policies : List Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {response : TPE.Response} :

Like partial_authorize_satisfied_permits_not_determining_if_deny for forbid policies, but we can prove a stronger theorem because any satisfied forbid causes the decision to be deny. If the result of concrete authorization is allow, then there can be no satisfied forbid policies after partial authorization.