This file defines what it means for a policy slice to be sound.

We prove two main theorems:

• Authorization returns the same response for a sound policy slice as for the original collection of policies (isAuthorized_eq_for_sound_policy_slice).
• It is sound to slice policies based on scope constraints (see isAuthorized_eq_for_scope_based_policy_slice). The proof is based on a more general lemma (sound_bound_analysis_produces_sound_slices) that covers all forms of slicing that are based on identifying "bound" principal and resource entities (if any) for a policy, such that the policy evaluates to true on an input only if the request principal and resource are descendents of the corresponding bound entities. Currently, we are extracting bounds only from the scope constraints. The general lemma also covers more sophisticated analyses that can extract bounds from policy conditions as well.

theorem Cedar.Thm.isAuthorized_eq_for_sound_policy_slice (req : Spec.Request) (entities : Spec.Entities) (slice policies : Spec.Policies) : IsSoundPolicySlice req entities slice policies → Spec.isAuthorized req entities slice = Spec.isAuthorized req entities policies

Policy slicing soundness: isAuthorized produces the same result for a sound slice (subset) of a collection of policies as it does for the original policies.

theorem Cedar.Thm.sound_bound_analysis_produces_sound_slices (ba : Slice.BoundAnalysis) (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : IsSoundBoundAnalysis ba → IsSoundPolicySlice request entities (ba.slice request entities policies) policies

A sound bound analysis produces sound policy slices.

theorem Cedar.Thm.scope_bound_is_sound (policy : Spec.Policy) : IsSoundPolicyBound (Slice.scopeAnalysis policy) policy

Scope-based bounds are sound.

theorem Cedar.Thm.scope_analysis_is_sound : IsSoundBoundAnalysis Slice.scopeAnalysis

Scope-based bound analysis is sound.

theorem Cedar.Thm.isAuthorized_eq_for_scope_based_policy_slice (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : Spec.isAuthorized request entities (Slice.BoundAnalysis.slice Slice.scopeAnalysis request entities policies) = Spec.isAuthorized request entities policies

Scope-based slicing is sound: isAuthorized produces the same result for a scope-based slice of a collection of policies as it does for the original policies.