PAuth checks tool names, arguments, and cross-service data dependencies against a user-authenticated task using symbolic slices and signed provenance.
An agent may hold permission to invoke a service while still making a call that violates the user's particular request. The recipient, amount, or prerequisite for an operation can depend on earlier service responses, so checking the tool name alone does not establish that the complete operation follows the task.
The paper asks how servers can verify these dependencies while treating the agent as untrusted. Its setting assumes an authenticated, sufficiently specified task and a trusted server-side translation model. Existing application controls and the correctness of authoritative service data remain separate assumptions.
A task-scoped authorization model in which each server derives a symbolic specification of the operations relevant to its part of the task.
Signed envelopes that connect concrete return values to their computational provenance across services.
An MCP proxy and server middleware implementation, accompanied by AuthBench cases for legitimate operations and deliberately altered calls.
The user authenticates the task text. A proxy distributes it and the available tool schemas to participating servers. Each server's language model translates the request into a restricted imperative program; deterministic processing derives a slice for each relevant call, including argument expressions and branch conditions.
Upstream services return signed envelopes containing both a concrete value and its symbolic origin. When a later call arrives, the receiving server verifies the signatures, reconstructs the relevant value environment, checks the slice's conditions, and computes the expected arguments. Execution proceeds when the actual call matches an authorized rule.
Calls outside the derived rules trigger explicit authorization. Arguments that require unresolved external interpretation are represented as nondeterministic values, which cannot automatically satisfy a concrete match. Alternatively, the user can confirm a refined task that resolves those values before registration. Successful calls produce further envelopes for downstream verification.

AuthBench adapts AgentDojo's banking, messaging, travel, and workspace tasks and adds shopping workflows with cross-service dependencies. It distinguishes original underspecified instructions from refined instructions, then replays legitimate traces and tests operand changes, unrelated tools, and bypassed guards.
The protocol runs in both an in-process AgentDojo setting and independent MCP servers connected through OpenClaw. Evaluation examines authorization without intervention, escalation of off-task calls, generated-slice correctness, task complexity, and registration versus runtime overhead. Additional translation models and manual slice inspection probe dependence on the language-model stage.
Open this note in the interactive notebook (comments, hooks) → · All notes