Consent as an Operational Semantics

Abstract. Consent in software is almost always a policy: a document, a checkbox, a promise about future behavior. Policies do not survive scale, acquisition, or incentive change. We give consent an operational semantics instead — a small-step transition system over grants, requests, and receipts, in which the properties usually asserted in prose become statements that either hold of the system or do not. We define the syntax, give the transition rules, state five properties the model is designed to satisfy, and sketch their arguments. We then spend the longest section of the paper on what the formalism provably does not give you, because a consent model that produces false confidence is worse than no model at all.

1. Why consent needs a semantics

The dominant industrial notion of consent is a speech act performed once: a person agrees to a document, and thereafter the system does what the document allows. This has three failure modes so familiar they are hardly noticed.

It is unbounded in scope — the document describes categories, not accesses. It is unbounded in time — agreement persists until affirmatively withdrawn, and withdrawal is typically not wired to anything. And it is unobservable— the person cannot see what was actually done under the agreement, so the agreement's scope is unfalsifiable in practice.

The industry response has been better documents. We think the error is more basic: consent is being modeled as a static predicate when it is really a dynamic capability. A person does not agree to a category of use; they authorize a specific principal to perform a specific operation on specific data for a specific purpose until a specific time, and they retain the ability to withdraw that authorization and to inspect what happened under it.

That is not a legal object. It is a systems object, and systems objects can have semantics. The contribution of this paper is to write those semantics down small enough to reason about.

2. Design commitments

Three commitments shape the model and should be stated before the notation, since they are assumptions rather than results.

Consent is a capability, not a permission bit. Holding a grant is what authorizes an access. There is no ambient authority — no configuration in which a principal may act because of who it is rather than what it holds.

Every access is observable to the subject.Receipts are not an audit feature for the operator; they are the mechanism by which the subject can check the system's claims. A model that permits unobserved access has no enforcement, only etiquette.

Revocation is total over the future and powerless over the past. We insist on both halves. Systems that promise revocation quietly imply retroactive effect, which is not achievable; being explicit that revocation cannot un-know is a correctness requirement, not a disclaimer.

3. Syntax

The objects are deliberately few. P ranges over principals (the subject who owns data, and requesters who may act). D ranges over data items. S ranges over scopes — a scope denotes a set of data items, and we require scopes to be closed under a decidable membership test. U ranges over purposes, drawn from a fixed published vocabulary. t ranges over time.

  grant   g  ::=  ⟨ id, subject P, holder P', scope S, purpose U,
                     expiry t, revoked? b ⟩

  request r  ::=  ⟨ holder P', item D, purpose U, at t ⟩

  receipt k  ::=  ⟨ grant id, holder P', item D, purpose U,
                    at t, returned δ ⟩

  state   Σ  ::=  ⟨ G, K ⟩          G = set of grants
                                     K = append-only receipt log

A purpose vocabulary that is fixed and published matters more than it appears. If requesters may invent purposes, purpose-binding degrades to free text and the property in §6 becomes unenforceable. This is a real constraint on the design and it costs expressiveness.

4. Operational semantics

Three rules generate all behavior. We write Σ → Σ′ for a transition.

  [ISSUE]
     P authorizes g   with subject(g) = P
     ─────────────────────────────────────────
       ⟨ G, K ⟩  →  ⟨ G ∪ {g}, K ⟩


  [ACCESS]
     g ∈ G     holder(g) = P'     D ∈ scope(g)
     purpose(g) = U    t < expiry(g)    ¬revoked(g)
     ─────────────────────────────────────────────────
       ⟨ G, K ⟩  →  ⟨ G, K · ⟨g.id, P', D, U, t, δ⟩ ⟩

           where δ is the data released


  [REVOKE]
     g ∈ G      subject(g) = P      P revokes g
     ────────────────────────────────────────────
       ⟨ G, K ⟩  →  ⟨ G[g.revoked := true], K ⟩

The essential structural feature is that [ACCESS] is the only rule that releases data, and it emits a receipt in the same step. Access and receipt are not two operations that the implementation is trusted to perform together; they are one transition. An implementation that can release without logging is not an implementation of this semantics — which is exactly the kind of statement a prose policy cannot make.

Note also what is absent. There is no rule that grants authority to a principal by identity, no rule by which a holder extends its own grant, and no rule that removes entries from K. Absence of rules is how a small-step semantics expresses a prohibition.

5. Properties

Each property below follows by induction over transition sequences; we sketch rather than develop the arguments, since they are routine once the rules are fixed.

P1 (No access without a live grant). If a data item is released in a transition, there exists a grant in the state whose holder is the requester, whose scope contains the item, whose purpose matches, which is unexpired and unrevoked. Immediate: [ACCESS] is the only releasing rule and its premises are exactly these.

P2 (Receipt completeness). The receipt log contains exactly one entry per release, and no entry without a release. Follows from [ACCESS] emitting precisely one receipt, no other rule touching K, and K being append-only.

P3 (Revocation totality over the future). After a revoking transition, no subsequent transition releases data under that grant. The revoked flag falsifies an [ACCESS] premise, and no rule clears it.

P4 (Non-escalation). No transition sequence beginning from a state yields a release outside the union of scopes of grants issued by the subject. There is no rule producing a grant except [ISSUE], whose premise requires the subject's authorization.

P5 (Purpose binding). A release recorded under purpose U occurred under a grant whose purpose is U. Direct from the premise. We flag immediately that this is a syntacticguarantee — the model cannot determine whether the requester's real intent matched the declared purpose. See §7.

6. Expiry, and why time is the hard parameter

Expiry is the one premise requiring a clock, which makes it the weakest part of the system in practice. A holder whose clock is behind may believe a grant live after expiry; a distributed implementation must decide whose clock is authoritative.

We take the position that the data holder's clock must not be the authority, since it belongs to the party with an incentive to see grants as live. Evaluation should occur at the point of release under a clock the subject's side controls or can verify. This is a real distributed-systems constraint that a purely syntactic reading of the rules hides, and we think it is where careless implementations of this model will actually fail.

7. What this model does not give you

This is the most important section, and it is longer than the results on purpose. A formalism confers authority, and a consent formalism that is quoted without its limits will be used to claim protections it does not provide.

It does not prevent inference. P1 constrains what is released, not what can be concluded. A requester granted coarse location for a legitimate purpose may infer a home address across permitted accesses. Nothing in the semantics bounds the inferential closure of released data, and we know of no tractable way to make it do so. This is, in our judgment, the single largest gap between what consent models promise and what they deliver.

It does not survive the boundary without a chain. The model governs one system. A holder that lawfully receives data and then re-shares it is outside the transition system entirely. Sticky-policy and information-flow approaches address this and are, in general, defeatable by a determined recipient. Our model does not solve it; it makes the boundary visible by ensuring the last in-system release is receipted.

Purpose binding is syntactic, not semantic.P5 guarantees the declared purpose matches the grant. It cannot guarantee the requester's actual use. Purpose limitation is ultimately enforced by consequence, not by construction, and a model that appears to enforce it may cause exactly the misplaced trust we are trying to eliminate.

Revocation cannot un-know.P3 is a statement about future transitions. Data released before revocation is released. We state this loudly because the everyday meaning of “revoke” suggests retrieval, and any interface implying otherwise is lying to the person using it.

Aggregation leaks across grants. Each of several narrow grants may be individually unobjectionable while their union is highly identifying. The model has no notion of cumulative disclosure, and a subject reasoning grant-by-grant will systematically underestimate what they have disclosed in total. Extending the semantics with a budget is a natural direction and connects directly to the composition problem in our work on measurement under consent.

Consent quality is out of scope. The semantics assumes the [ISSUE] premise — that the subject authorized the grant. Whether the authorization was informed, uncoerced, or comprehensible is a human-factors and legal question the formalism is silent on. A dark-pattern interface produces perfectly well-typed grants.

8. Related work

Policy languages such as XACML and ODRL express rich rules over access and usage, and are considerably more expressive than what we describe; our aim is different — a semantics small enough to prove things about and to implement identically twice. The Platform for Privacy Preferences (P3P) is instructive as a failure: it standardized machine-readable policy without a mechanism binding the policy to actual behavior, which is precisely the binding [ACCESS] provides. Sticky policies and usage control attack the cross-boundary problem we explicitly do not solve. Information-flow control gives far stronger non-interference guarantees at a cost in annotation burden that has kept it out of most production systems. Capability-based security is the closest ancestor: our grants are capabilities with an expiry, a declared purpose, and a mandatory audit obligation on exercise. In law, the GDPR notions of lawful basis, purpose limitation, and erasure are the regulatory analogues, and the gap between erasure-as-law and revocation-as-mechanism is one this paper tries to make precise rather than paper over.

9. Open problems

A disclosure budget. Extend the state with an accounting of cumulative disclosure per requester and refuse [ACCESS] when a bound is exceeded. The difficulty is choosing a metric that is meaningful across heterogeneous data types.

Delegation with attenuation.Real workflows require a holder to pass narrowed authority to a subcontractor. Adding a delegation rule that provably cannot widen scope, keeps the subject's revocation effective transitively, and preserves receipt completeness through the chain, is the most-requested and least-safe extension.

Verifiable receipts. Our receipts are trustworthy insofar as the log is. Making them independently verifiable — so a subject can detect a suppressed receipt without trusting the operator — is what would move P2 from a design property to a checkable one, and it is where we would most like to be proven able.

Usability of the grant model.Nothing here helps a person reason about hundreds of live grants. The formalism's guarantees are worthless if the interface presenting them is incomprehensible, and we consider this at least as hard as the technical extensions.

10. Conclusion

The claim is modest by design: consent expressed as a transition system makes a small number of properties checkable, and makes the boundaries of those properties explicit. That is less than the industry usually promises and, we would argue, considerably more than it usually delivers.

The section we most want read is §7. A person is better served by a narrow guarantee stated honestly than by a broad assurance that dissolves on contact with inference, aggregation, or a boundary crossing. If this paper is cited, we would rather it be cited for its limits.