def
Cedar.Thm.ResidualPoliciesEquiv
(policies : List Spec.Policy)
(residuals : List TPE.ResidualPolicy)
(req : Spec.Request)
(es : Spec.Entities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.isValidAndConsistent_env
{schema : Validation.Schema}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
:
theorem
Cedar.Thm.evaluatePolicies_residuals_equiv
{schema : Validation.Schema}
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
(hv : TPE.isValidAndConsistent schema req es preq pes = Except.ok ())
(h : TPE.isAuthorized.evaluatePolicies schema policies preq pes = Except.ok rps)
:
ResidualPoliciesEquiv policies rps req es
theorem
Cedar.Thm.reauthorize_satisfied_policies_equiv
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{residuals : List TPE.ResidualPolicy}
(h_auth : ResidualPoliciesEquiv policies residuals req es)
(effect : Spec.Effect)
:
TPE.Response.reauthorize.satisfiedPolicies effect residuals req es = Spec.satisfiedPolicies effect policies req es
theorem
Cedar.Thm.reauthorize_error_policies_equiv
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{residuals : List TPE.ResidualPolicy}
(h_auth : ResidualPoliciesEquiv policies residuals req es)
:
theorem
Cedar.Thm.no_satisfied_effect_if_empty_satisfied_and_residual_policies
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{effect : Spec.Effect}
(h₃ : ResidualPoliciesEquiv policies rps req es)
(h_satisfied_empty : (TPE.isAuthorizedFromResiduals.satisfiedPolicies effect rps).isEmpty = true)
(h_residual_empty : (TPE.isAuthorizedFromResiduals.residualPolicies effect rps).isEmpty = true)
:
¬HasSatisfiedEffect effect req es policies
theorem
Cedar.Thm.satisfied_effect_if_non_empty_satisfied_policies
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{effect : Spec.Effect}
(h₃ : ResidualPoliciesEquiv policies rps req es)
(h_non_empty : ¬(TPE.isAuthorizedFromResiduals.satisfiedPolicies effect rps).isEmpty = true)
:
HasSatisfiedEffect effect req es policies
theorem
Cedar.Thm.residuals_decision_agrees
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{d : Spec.Decision}
(h₃ : ResidualPoliciesEquiv policies rps req es)
(h_dec : (TPE.isAuthorizedFromResiduals rps).decision = some d)
:
theorem
Cedar.Thm.partial_authorize_error_policies_is_sound
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
(effect : Spec.Effect)
(h₁ : ResidualPoliciesEquiv policies rps req es)
:
TPE.isAuthorizedFromResiduals.errorPolicies effect rps ⊆ (Spec.isAuthorized req es policies).erroringPolicies
theorem
Cedar.Thm.partial_authorize_satisfied_policies_is_sound
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
(effect : Spec.Effect)
(h₁ : ResidualPoliciesEquiv policies rps req es)
:
TPE.isAuthorizedFromResiduals.satisfiedPolicies effect rps ⊆ Spec.satisfiedPolicies effect policies req es
theorem
Cedar.Thm.partial_authorize_satisfied_forbids_is_sound
{response : TPE.Response}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
:
TPE.isAuthorized schema policies preq pes = Except.ok response →
TPE.isValidAndConsistent schema req es preq pes = Except.ok () →
response.satisfiedForbids ⊆ Spec.satisfiedPolicies Spec.Effect.forbid policies req es
theorem
Cedar.Thm.partial_authorize_satisfied_permits_is_sound
{response : TPE.Response}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
:
TPE.isAuthorized schema policies preq pes = Except.ok response →
TPE.isValidAndConsistent schema req es preq pes = Except.ok () →
response.satisfiedPermits ⊆ Spec.satisfiedPolicies Spec.Effect.permit policies req es