@@ -37,7 +37,7 @@ sets), delegation/attenuation semantics, revocation checks, and CEP verification
3737behavior. Transport/envelope bindings and sigchain framing are defined in PSP-3;
3838receipt formats and proof traces are defined in PSP-2; enforcement
3939placement/modes are defined in the CEP/BA specification; acceptance and
40- governance live in TAP/RAM and related profiles .
40+ governance live in TAP/RAM.
4141
4242## 2. Terminology and Requirements Language
4343
@@ -160,8 +160,7 @@ convention. Scheme names (e.g., `vault:`, `k8s:`) and content identifiers (e.g.,
160160
161161These canonical names appear in the textual specification and in the
162162non-normative JSON projections. PSP-3 defines the on-wire field names and
163- encodings; profiles MAY map the canonical names to alternative encodings but
164- MUST provide a bijection between the PSP-1 names and the on-wire representation.
163+ encodings.
165164
166165## 3. Overview and Goals
167166
@@ -206,8 +205,8 @@ What PSP-1 defines:
206205- Receipt schemas: All receipt formats (PoAR/VOR/View) are specified in PSP-2.
207206- Transport/envelope and sigchain framing (JOSE/COSE/DSSE, canonical bytes):
208207 specified in PSP-3.
209- - Channel-binding mechanisms : Concrete binding profiles (e.g., TLS exporter,
210- DPoP) are profiled elsewhere; PSP-1 only requires a verified binding.
208+ - Channel-binding profiles : Concrete channel- binding mechanisms (e.g., TLS
209+ exporter, DPoP) are defined elsewhere; PSP-1 only requires a verified binding.
211210- Global time/ordering: PSP-1 does not require a global clock or total order.
212211 Acceptance (TAP) specifies clock sources and tolerances.
213212- Secret issuance/derivation/aggregation crypto and interactive evaluation
@@ -307,14 +306,14 @@ Deterministic Evaluation and PSP-4).
307306 signature, and tightening rule are defined in the Builtins registry (PSP-4).
308307 The exact set in use is pinned by ` builtinsId ` in the Grant.
309308- Channel comparisons (e.g., ` channelGeq ` ) consult the pinned
310- ` channelLatticeId ` , which defines the set of recognized channel profile
311- identifiers and their partial order. Unknown profiles or an unknown lattice
312- MUST cause deny.
309+ ` channelLatticeId ` , which defines the set of recognized channel-binding
310+ profile identifiers and their partial order. Unknown identifiers or an unknown
311+ lattice MUST cause deny.
313312- Resource subset checks in declaration-aware builtins (e.g., inPairSet) consult
314313 the scheme comparator selected by the resource's scheme name.
315314- If a builtin, lattice, or comparator required by the Program is unknown or
316315 unavailable, evaluation MUST fail closed.
317- - Programs may constrain the live session's profile using
316+ - Programs may constrain the live session's channel-binding profile using
318317 ` channelGeq(channel, "...") ` as defined by the pinned channel lattice.
319318 Programs may also assert runtime or provenance context via equality over
320319 environment facts (e.g., ` ctxEq("k","v") ` ). How those environment facts are
@@ -371,7 +370,7 @@ evaluate Programs deterministically and emit minimal proof traces (which check,
371370which query, which literals). This keeps receipts auditable without a general
372371Datalog engine. If richer inference is required in a domain, issuers or
373372attestors SHOULD precompute finite sets (content-addressed) and reference them
374- from the Program; alternative profiles that carry ruleful logic MUST remain
373+ from the Program; alternative extensions that carry ruleful logic MUST remain
375374TAP-gated and provide either a compiled CPL/0 guard or an approved CEP runtime.
376375
377376### 4.5 Evaluation Environment
@@ -386,7 +385,7 @@ reference these facts by name.
386385 - iat: Int - NumericDate (Unix seconds) carried by the Presentation.
387386 - presenter: Str - DID of the presenting Subject.
388387 - enforcer: Str - DID/identifier of the enforcing CEP (audience).
389- - channel: Str - profile representing the live session's binding.
388+ - channel: Str - the live session's channel- binding profile identifier .
390389 - ctx: ` Map<Str, Term> ` - runtime context (e.g.,
391390 ` {"ns":"prod","pod":"runner-42"} ` ).
392391- Optional environment facts (TAP-gated)
@@ -433,9 +432,9 @@ PairSet/ActionSet.
433432- data:export
434433- model:infer
435434
436- Actions are plain strings compared for equality. Any domain governance over
437- action names (allowlists, required constraints) is outside PSP-1 and MAY be
438- enforced by TAP or profiles by requiring corresponding Program literals .
435+ Actions are plain strings compared for equality. Governance over action names
436+ (e.g., allow-lists, required prefixes/ constraints) is out of scope for PSP-1 and
437+ is defined by TAP policy .
439438
440439### 5.2 Resources
441440
@@ -589,8 +588,8 @@ identifier references an immutable snapshot in a registry (see PSP-4):
589588 one scheme is referenced.
590589- ** ` channelLatticeId ` ** - ** REQUIRED only if** the Program uses the
591590 ` channelGeq ` builtin. It is a content-addressed snapshot of the channel
592- lattice used to interpret ` >= ` between channel profile labels . It MUST be
593- omitted if the Program does not call ` channelGeq ` .
591+ lattice used to interpret ` >= ` between channel-binding profile identifiers . It
592+ MUST be omitted if the Program does not call ` channelGeq ` .
594593
595594A Grant does ** not** pin any action registry; actions are plain strings compared
596595for equality. Governance over action names lives in TAP and MAY be enforced by
@@ -606,11 +605,11 @@ rulebooks when evaluating Programs.
606605 builtin operators. Each operator entry defines the operator's identifier,
607606 argument types, semantics, tightening rules for attenuation, and resource
608607 bounds (time/memory). Unknown operators MUST cause denial at verification.
609- - ** Channel lattice snapshot** - Contains a unique ID, a set of channel profile
610- labels , and a partial order over those labels . The partial order defines the
611- result of ` channelGeq(channel, floor) ` . The precise meaning of each label
612- (e.g., ` mtls:v1 ` , ` tlsExporter :v1` , ` dpop:v1 ` , ` bearer:v1 ` ) is defined outside
613- this spec in the registry; only the ordering matters here.
608+ - ** Channel lattice snapshot** - Contains a unique ID, a set of channel-binding
609+ profile identifiers , and a partial order over those identifiers . The partial
610+ order defines the result of ` channelGeq(channel, floor) ` . The precise meaning
611+ of each label (e.g., ` mtls:v1 ` , ` tls-exporter :v1` , ` dpop:v1 ` , ` bearer:v1 ` ) is
612+ defined outside this spec in the registry; only the ordering matters here.
614613- ** Schemes manifest (` schemesSnapshotId ` )** - Contains a unique ID and a map
615614 from scheme names to comparator snapshot IDs. Each comparator snapshot defines
616615 normalization and subset decision rules for one scheme (e.g., vault, k8s,
@@ -650,17 +649,17 @@ A CEP MUST deny if any of the following holds:
650649
651650### 6.6 Interpreting ` channelGeq `
652651
653- The literal ` channelGeq(channel, floor) ` compares the verified channel profile
654- (from the Presentation's channel binding) against the floor value under the
655- pinned channel lattice. Common channel binding profiles include:
652+ The literal ` channelGeq(channel, floor) ` compares the verified channel-binding
653+ profile identifier (from the Presentation's channel binding) against the floor
654+ value under the pinned channel lattice. Common channel- binding profiles include:
656655
657656- ** ` mtls:v1 ` ** - Mutually authenticated TLS 1.3 (see RFC 8446).
658- - ** ` tlsExporter :v1` ** - TLS exporter-based channel binding (see RFC 9266).
657+ - ** ` tls-exporter :v1` ** - TLS exporter-based channel binding (see RFC 9266).
659658- ** ` dpop:v1 ` ** - Demonstrating Proof-of-Possession (DPoP) (see RFC 9449).
660659- ** ` bearer:v1 ` ** - No sender-constraining (Bearer tokens).
661660
662661The pinned lattice defines the partial order between these labels (for example:
663- ` mtls:v1 >= tlsExporter :v1 >= dpop:v1 >= bearer:v1 ` ). This subsection is
662+ ` mtls:v1 >= tls-exporter :v1 >= dpop:v1 >= bearer:v1 ` ). This subsection is
664663informative; the authoritative ordering and the set of recognized profiles are
665664defined by the snapshot referenced by ` channelLatticeId ` .
666665
@@ -999,9 +998,9 @@ Grants and transient proof-of-use.
999998 - syntactic attenuation (checks/literals tightening and declarations
1000999 subset).
10011000 - How parent Grants are made available is TAP-governed (e.g., local cache,
1002- pre-enforcement resolver, or a profile-defined stapled chain receipt / zk
1003- chain proof). At enforcement, if required parent Grants are not locally
1004- available, the CEP MUST deny.
1001+ pre-enforcement resolver, or a TAP required stapled chain proof / zk chain
1002+ proof). At enforcement, if required parent Grants are not locally available,
1003+ the CEP MUST deny.
10051004 - Any failure in the above MUST cause deny.
10061005- Storage
10071006 - Presentations MUST NOT be recorded on sigchains.
@@ -1050,9 +1049,9 @@ alternative encodings but MUST preserve the semantics.
10501049 step outside CPL/0 evaluation. At enforcement, if required parent Grants are
10511050 not locally available, the CEP MUST deny.
10521051 - A TAP policy (with PSP-3 bindings) MAY define alternate, bounded chain
1053- attestation artifacts (e.g., a stapled chain receipt or a zero-knowledge
1054- chain proof). PSP-1 core does not define or require such artifacts and
1055- forbids embedding raw Grant bodies in Presentations.
1052+ attestation artifacts (e.g., a stapled chain proof or a zero-knowledge chain
1053+ proof). PSP-1 core does not define or require such artifacts and forbids
1054+ embedding raw Grant bodies in Presentations.
10561055
10571056** Example:** The following JSON projection illustrates one possible mapping of
10581057the conceptual fields. Names and encodings are illustrative only; the normative
@@ -1081,9 +1080,9 @@ specification of on-wire fields is defined in PSP-3.
10811080 channel binding verification, custody/attenuation verification, and Program
10821081 evaluation under the pinned semantics and bundled declarations.
10831082- Per-use narrowing is achieved by the Program's literals (e.g., ctxEq, ttlOk)
1084- evaluated against Presentation-supplied ctx and iat/exp. A future TAP-gated
1085- profile MAY introduce presentation overlays with strict attenuation and
1086- receipt requirements.
1083+ evaluated against Presentation-supplied ctx and iat/exp. TAP policy MAY
1084+ introduce presentation overlays with strict attenuation and receipt
1085+ requirements.
10871086
10881087## 11. Delegation and Attenuation
10891088
@@ -1215,8 +1214,8 @@ hop-by-hop. Children MAY only narrow or preserve authority.
12151214- No network I/O in evaluation:
12161215 - Program evaluation and attenuation checks MUST NOT perform network I/O.
12171216 Required parent Grants MUST be locally available at enforcement (e.g., via
1218- cache, pre-enforcement resolver permitted by TAP, or a profile -defined
1219- stapled artifact). If not locally available, the CEP MUST deny.
1217+ cache, pre-enforcement resolver permitted by TAP, or a TAP -defined stapled
1218+ artifact). If not locally available, the CEP MUST deny.
12201219
12211220### 11.7 Fail-Closed Conditions
12221221
@@ -1858,7 +1857,7 @@ CEP evaluation outline
18581857 Principal-side (as shown).
18591858- Presentations remain small; do not embed Grant bodies in PSP-1 core. If
18601859 parents aren't local at enforcement, deny (TAP defines pre-enforcement
1861- hydration or profile-level stapling).
1860+ hydration or stapling chain proof ).
18621861- Receipts: PoAR should capture enough to audit the decision (` programId ` ,
18631862 declaration CIDs, pins, minimal trace), plus derivation metadata (tokenRef),
18641863 but never the token itself.
@@ -2065,7 +2064,7 @@ invocations.
20652064| --------------- | ------------------------------------------ | ------- | ----------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------- | ----------------------------------------------------------- |
20662065| ` withinTime ` | ` (now:Int, nbf:Int, exp:Int) ` | Bool | ` nbf <= now < exp ` | ` [nbf_child >= nbf_parent $\land$ exp_child <= exp_parent] ` | ill-typed => deny; else boolean result |
20672066| ` ttlOk ` | ` (iat:Int, now:Int, ttlMax:Int) ` | Bool | ` now < iat + ttlMax ` | ` ttlMax_child <= ttlMax_parent ` | ill-typed => deny; else boolean result |
2068- | ` channelGeq ` | ` (channel:Str, floor:Str) ` | Bool | channel >= floor in the pinned lattice | floor_child >= floor_parent | unknown lattice or profile => deny |
2067+ | ` channelGeq ` | ` (channel:Str, floor:Str) ` | Bool | channel >= floor in the pinned lattice | floor_child >= floor_parent | unknown lattice or channel-binding profile => deny |
20692068| ` inPairSet ` | ` (action:Str, resource:Str, pairsCid:Str) ` | Bool | ` (action, resource) $\in$ PairSet(pairsCid) ` (resource normalized via comparator) | PairSet_child $\subseteq$ PairSet_parent | missing/malformed declaration or comparator failure => deny |
20702069| ` inActionSet ` | ` (action:Str, actionsCid:Str) ` | Bool | ` action $\in$ ActionSet(actionsCid) ` | ActionSet_child $\subseteq$ ActionSet_parent | missing/malformed declaration => deny |
20712070| ` inResourceSet ` | ` (resource:Str, resourcesCid:Str) ` | Bool | $\exists$ selector $\in$ ResourceSet(resourcesCid) such that resource $\subseteq$ selector under comparator | ResourceSet_child $\subseteq$ ResourceSet_parent | comparator or normalization failure => deny |
0 commit comments