polysec-auth

PolySec auth — UC-3, the authentication & privilege state machine

The second anchor scenario (docs/polysec-spec.md §2 UC-3): the TLS-lineage classic, generalized — no privileged action before the authenticating transition, plus an ordering invariant (the handshake must complete before application data is accepted). It's where PolySec catches the SKIP-TLS shape — state-machine confusion — at design time.

npm run polysec:auth     # fully-mediated verdict → out/security-report.{json,md}
npm test                 # the assertions behind this scenario

$0 API, deterministic, exhaustive over the finite declared domains.

What's new versus the sandbox (UC-1)

	sandbox (UC-1, lethal trifecta)	auth (UC-3)
invariant class	confidentiality / coexistence	reachability + ordering
forbidden regions	one	two (privilege + ordering)
havoc hero variable	egress	privileged
the famous bug it catches	prompt-injection exfiltration	SKIP-TLS state confusion
recovery	containment (flag persists)	restoration (reversible)

The machine

next.cjs is a SAM v2 strict-profile machine. State (all booleans): handshake, authenticated, appData, privileged, peerClosed.

• Ordering — AUTHENTICATE and ACCEPT_APP_DATA are default-denied until handshake completes (handshake ≺ auth, handshake ≺ appData).
• Privilege gate — DO_PRIVILEGED is default-denied in every state where authenticated is false. This is the gate.
• Restoration — TEARDOWN returns the session to the pristine unauthenticated start. Unlike the trifecta's compromise flag, UC-3 recovery is genuinely reversible (no external damage, §2 UC-3), so the desired state is pristine, not merely contained.

Forbidden regions (security.json):

1. no-privileged-pre-auth — predicate: "privileged && !authenticated"
2. handshake-precedes-appdata — predicate: "appData && !handshake"

The harden progression

1. Clean from-init. Over all reachable states of the mediated machine, neither region is entered — the gates enforce both the privilege rule and the ordering.
2. Havoc counterexample when privilege is left adversarial. With security.privileged-adversarial.json, the designer treats privileged as something an unmodeled channel could trigger (adversarial). Havoc drills privileged := true from an unauthenticated state → privileged ∧ ¬authenticated. The counterexample names privileged. The repair (security.json) makes privileged protected — settable only via the auth-gated DO_PRIVILEGED.
3. SKIP-TLS negative control. next.skip-auth.cjs changes one line — DO_PRIVILEGED guards on handshake instead of authenticated. The from-init check reaches the forbidden region via COMPLETE_HANDSHAKE → DO_PRIVILEGED (no AUTHENTICATE in between) — a privileged effect after the handshake but before authentication. That reachable-bad-state is the SKIP-TLS vulnerability, emitted with the shortest witness.
4. Fully-mediated verdict. The mediated machine passes all three gates → FULLY MEDIATED, written to out/security-report.{json,md}.

Controls. POSITIVE: next.cjs passes. NEGATIVE: next.skip-auth.cjs fails from-init with the SKIP-TLS path. The verdict flips exactly on the conjunction.

Honest note (same as the sandbox)

This is exhaustive over the finite declared domains and the observable projection only (§0). Havoc over-approximates (safe direction); gate-deletion reachability is monotone, so a bypass it reports is also a from-init violation — its distinct value is the witness. Havoc is the check that reaches beyond the modeled machine — the SKIP-TLS demo shows it naming a privilege escalation an unmodeled channel could cause.

Files

file	role
next.cjs	mediated auth machine (positive control)
next.skip-auth.cjs	SKIP-TLS negative control (mis-guarded DO_PRIVILEGED)
contract.json	observable scope / action alphabet
invariants.mjs	privilege + ordering invariants (check.mjs entry point)
security.json	mediated manifest (two forbidden regions)
security.privileged-adversarial.json	pre-repair manifest (privilege adversarial)
out/security-report.{json,md}	the fully-mediated verdict (generated)

Try it with the Polygraph plugin

With the Polygraph plugin installed, drive this machine in natural language ($0 API):

• Render the machine + invariants: Using polyviz, render the state machine and invariants for examples/polysec-auth (next.cjs, invariants.mjs).
• Elicit / grade invariants: Elicit invariants for examples/polysec-auth/next.cjs using its contract.json.

This scenario ships no trace corpus, so /verify (which needs one) does not apply here — use the sandbox for a full verify run.