Policy automata for stateful authorization

Modern policy languages decide whether an action is allowed by evaluating logical conditions over the request and the surrounding context, and by attaching a result (e.g. permit or forbid) to each matching rule. Yet most of these languages are stateless: each request is evaluated in isolation, which makes history-dependent (usage) policies awkward to express. In this paper we first introduce a minimal language of policies with effects, where a policy is a guarded effect: a guard is a logical formula on the current state and the effect is a generic state transformer fired when the guard holds. We then define policy automata, a deterministic, stateful variant of usage automata in which the policy state is explicit and transitions update it through effects. Each transition also emits an access-control decision, so a policy automaton reads as a Mealy machine whose output is the verdict. Determinism removes the need to instantiate the automaton over all resource assignments and makes run-time monitoring conceptually simple. We show the model is analysable over a decidable guard logic (well-formedness, reachability of a denial, and policy subsumption and equivalence are decidable) and that it is compositional: compliant languages are closed under conjunction and disjunction, with a “deny-overriding” rule-set union recovering the conjunction. The explicit state also pays off in expressiveness: policy automata are strictly more expressive than the stateless core of Cedar and Rego, with a memory cost that grows with the usage bound.