把智能体授权写成可验证关系：Groth16 原型在 531 约束电路上完成主体与计划绑定，但执行绑定仍空缺

论文把智能体授权刻画为一个请求绑定的可加密验证关系 RCVA，其合取形式为 BindPrincipal ∧ BindRequest ∧ BindContext ∧ SatisfyPolicy，公开陈述 x 包含主体标识、请求承诺、上下文承诺、策略标识与新鲜性参数，私有见证 w 包含智能体秘密、私有授权属性及承诺原像。 作者强调其贡献不是把零知识证明用于智能体系统，而是把授权本身从身份认证、能力委托与事后审计中分离出来，作为独立的安全关系来形式化。 属于假设与理论型论文，给出形式化定义与方程，但作者明确说明完整的安全归约（含显式提取器与模拟器论证）留待未来工作。

论文定义了一组候选安全属性：授权可靠性、主体绑定、授权请求绑定、策略绑定、上下文绑定与重放抵抗，并给出非形式化归约草图，把攻击者优势界定为 Groth16 可靠性优势与哈希碰撞或承诺绑定性优势之和。 这些属性被明确标注为候选定义，其作为已确立安全保证的地位取决于尚未完成的归约论证，作者在文中反复声明这一点。 归约草图基于 Groth16 的知识可靠性以及 Pedersen 式承诺的绑定性，但作者说明草图不含显式提取器或模拟器构造。

论文给出一个可执行的零知识概念验证：在 bn128 曲线上用 Circom 2.x 与 snarkjs 实现 Groth16 电路，公开陈述为 xPoC = (idi, hplan, n, t)，私有见证为 wPoC = (ski, ρi, attrsi, plan)，主体绑定用双输入 Poseidon(ski, ρi)，计划绑定用 SHA256(plan)，策略满足性以电路内算术约束表示，重放保护由网关的非一次性状态在电路外执行。 该原型是作者此前在 RootedCON Madrid 公开演示的实验前身，本文把它映射到 CVA 抽象，作为主体绑定与计划级请求绑定可行性的构造性证据。 单一电路配置：531 个约束、537 条线、九个私有输入、五个输出；n = 20 次运行下见证生成 61.9 ± 1.1 ms、证明生成 351.9 ± 26.6 ms、验证 309.4 ± 22.6 ms、证明大小 805 字节，计时经命令行调用因而包含 Node.js 进程启动开销。

论文把身份绑定、授权请求绑定与运行时执行绑定三者的结构性分离作为核心开放问题：验证通过的证明只说明被承诺的请求满足授权关系，并不说明运行时执行了同一请求，弥合该缺口需要远程证明、可信执行环境或可验证执行回执等执行期信任锚。 作者称据其所知，现有智能体安全框架尚未在可加密验证的授权关系内形式化这一区分，并据此提出可证伪的研究议程，包括必要绑定、可表示策略与运行可行性三个研究问题。 该分离以方程形式给出并作为结构性观察而非博弈式属性；作者同时指出多跳委托链需要额外的 BindDelegationScope 与递归证明组合，且该条件在本文中刻意未形式化。

该工作面向研究智能体授权机制的研究者与设计者，适用于单一智能体与网关之间的授权交互场景，其原型针对 Groth16 与 bn128 曲线上的单电路配置，并假设网关部分可信、底层密码原语不可攻破。它为进一步形式化候选属性、实现上下文承诺、比较不同证明系统以及引入执行期信任锚提供了起点。

读者仍需关注候选安全属性何时能获得完整归约、上下文承诺 hc 的具体构造（定长填充或 Poseidon 海绵）如何选择、以及运行时执行绑定将采用何种执行期证据机制。作者列出的限制还包括策略语言限于静态算术电路、Groth16 需要可信设置且非后量子安全、网关部分可信、未做多智能体委托链评估，以及原型仅用单一计划级承诺而非模型中的资源与动作分解。这些是范围与开放问题，而非对工作的否定。