theorem
Cedar.Thm.reauthorize_satisfied_policies_equiv
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{residuals : List TPE.ResidualPolicy}
(hv : TPE.isValidAndConsistent schema req es preq pes = Except.ok ())
(h_auth :
List.Forall₂
(fun (x : Spec.Policy) (y : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk x.id x.effect <$> TPE.evaluatePolicy schema x preq pes = Except.ok y)
policies residuals)
(effect : Spec.Effect)
:
TPE.Response.reauthorize.satisfiedPolicies effect residuals req es = Spec.satisfiedPolicies effect policies req es
theorem
Cedar.Thm.reauthorize_error_policies_equiv
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{residuals : List TPE.ResidualPolicy}
(hv : TPE.isValidAndConsistent schema req es preq pes = Except.ok ())
(h_auth :
List.Forall₂
(fun (x : Spec.Policy) (y : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk x.id x.effect <$> TPE.evaluatePolicy schema x preq pes = Except.ok y)
policies residuals)
:
theorem
Cedar.Thm.no_satisfied_effect_if_empty_satisfied_and_residual_policies
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{rps : List TPE.ResidualPolicy}
{effect : Spec.Effect}
(h₂ : TPE.isValidAndConsistent schema req es preq pes = Except.ok ())
(h₃ :
List.Forall₂
(fun (p : Spec.Policy) (rp : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk p.id p.effect <$> TPE.evaluatePolicy schema p preq pes = Except.ok rp)
policies rps)
(h_satisfied_empty : (TPE.isAuthorized.satisfiedPolicies effect rps).isEmpty = true)
(h_residual_empty : (TPE.isAuthorized.residualPolicies effect rps).isEmpty = true)
:
¬HasSatisfiedEffect effect req es policies
theorem
Cedar.Thm.satisfied_effect_if_non_empty_satisfied_policies
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{rps : List TPE.ResidualPolicy}
{effect : Spec.Effect}
(h₂ : TPE.isValidAndConsistent schema req es preq pes = Except.ok ())
(h₃ :
List.Forall₂
(fun (p : Spec.Policy) (rp : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk p.id p.effect <$> TPE.evaluatePolicy schema p preq pes = Except.ok rp)
policies rps)
(h_non_empty : ¬(TPE.isAuthorized.satisfiedPolicies effect rps).isEmpty = true)
:
HasSatisfiedEffect effect req es policies
theorem
Cedar.Thm.partial_authorize_error_policies_is_sound
{rps : List TPE.ResidualPolicy}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
(effect : Spec.Effect)
:
List.Forall₂
(fun (p : Spec.Policy) (rp : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk p.id p.effect <$> TPE.evaluatePolicy schema p preq pes = Except.ok rp)
policies rps →
TPE.isValidAndConsistent schema req es preq pes = Except.ok () →
TPE.isAuthorized.errorPolicies effect rps ⊆ (Spec.isAuthorized req es policies).erroringPolicies
theorem
Cedar.Thm.partial_authorize_satisfied_policies_is_sound
{rps : List TPE.ResidualPolicy}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
(effect : Spec.Effect)
:
List.Forall₂
(fun (p : Spec.Policy) (rp : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk p.id p.effect <$> TPE.evaluatePolicy schema p preq pes = Except.ok rp)
policies rps →
TPE.isValidAndConsistent schema req es preq pes = Except.ok () →
TPE.isAuthorized.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