Formally prove additional Cedar authorization properties

[mwhicks1]

Category

Lean formalization

Describe the feature you'd like to request

The following properties should be true in Cedar, and are useful for justifying optimizations. Might be nice to prove them in Lean.

For all policy stores S, requests R, and entities ET,

1. isAuthz(S,R,ET) = (X,D,E) implies that D is disjoint from E (where D are the determining policies and E are the erroring ones)
2. isAuthz(S,R,ET) = (Allow,D,E) implies that for all permit policies P, isAuthz(S+{P},R,ET) = (Allow,D’,E’) where D’ >= D and E’ >= E. I.e., adding a permit policy won’t change an Allow decision
3. isAuthz(S,R,ET) = (Deny,D,E) implies that for all forbid policies P, isAuthz(S+{P},R,ET) = (Deny,D’,E’) where D’ >= D and E’ >= E. I.e., adding a forbid policy won’t change a Deny decision
4. For all policies P, isAuthz(S,R,ET) = (X,D,E) implies that if P in D, then for all policies P0, isAuthz(S+{P0},R,ET) = (X,D1,E1) implies P in D1. In other words, if P is a determining policy, then adding another policy won’t change that if the decision X is unchanged.
5. For all policies P, isAuthz(S,R,ET) = (X,D,E) implies that if P in E, then for all policies P0, isAuthz(S+{P0},R,ET) = (X1,D1,E1) implies P in E1. In other words, if P is an erroring policy, then adding another policy won’t change that (even if the decision changes).

Describe alternatives you've considered

N/A.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change