置信度引导的协议 IR 审查 UI

本仓库包含一个用于 LLM 辅助安全协议建模的本地人在回路 UI。它支持我们工作中描述的工作流：

用于 LLM 辅助安全协议建模的置信度引导协议 IR

该系统引入协议中间表示（IR）作为自然语言协议描述与 Sapic+/Tamarin 生成之间的语义检查点，使审查者能够在形式化验证之前审计 LLM 生成的协议模型的语义准确性。

UI 预览

以下截图展示了在审查 UI 中加载的 Sigfox 准备就绪工作流。

工作流导入

字段审查

Tamarin 结果

仓库布局

• run_contract_review_ui.py：本地 HTTP 服务器和工作流 API。
• contract_review_ui/：浏览器 UI。
• protocol_ir_pipeline/：IR 处理、建模契约生成、Sapic+ 生成、修复、证明 lint 和 Tamarin 辅助工具。
• protocol_ir_pipeline/c_to_ir.py：分阶段的 C/C++ 源码到 ProtocolIR 提取，带有内嵌提示词。
• scripts/c_to_protocol_ir.py：C/C++ 提取流程的命令行入口点。
• config/：默认本地 lint/检索配置。
• examples/ui_input_cases.json：用于实验的 UI 就绪基准输入。
• examples/ui_inputs.md：便于复制、用于手动填写 UI 的基准输入，按难度分组。
• examples/protocol-abstraction-cases.json：捆绑的抽象提示库，仅在 UI 中启用时使用。
• examples/prepared_workflows/gpt55/：基准用例的原始 IR 和人工审查后的 IR 快照。
• examples/user_tested_workflows/deepseek_ui_20260615/：作者通过 UI 手动测试的 Toy 和 Sigfox 工作流。
• NOTICE.md：归属和工件范围说明。
• LICENSE：GPLv3 许可证文本。

要求

• Python 3.10+
• 用于 DeepSeek、OpenAI、Anthropic 或 OpenAI 兼容 Llama 端点的 LLM API 密钥
• tamarin-prover 位于你的 PATH 中，用于编译/证明验证。请按照适用于你平台的官方说明安装 Tamarin Prover：https://tamarin-prover.com/manual/master/book/002_installation.html。

安装 Python 依赖：

pip install -r requirements.txt

配置凭据：

cp .env.example .env
# edit .env and set the provider API key

运行 UI

从空的工作流目录开始：

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

打开：

http://127.0.0.1:8765/

典型工作流：

1. 粘贴自然语言协议描述并生成原始 IR/建模契约。
2. 审查并编辑 Messages、Checks、Events、Proof Targets 和 Attack Surface 中的语义字段。
3. 点击 Save Reviewed 以写入 modeling_contract.reviewed.json。
4. 点击 Generate Sapic+。
5. 如果安装了 tamarin-prover，则使用 Tamarin 进行编译和证明。

Save Reviewed 不要求确认每个审查徽章。确认字段有助于审查进度跟踪和证明关键生成提示，但保存的编辑仍会被生成过程使用。

C/C++ 源码提取

提取阶段、JSON 输出契约和提示词位于 protocol_ir_pipeline/c_to_ir.py。

使用 LLM 运行分阶段提取：

python3 scripts/c_to_protocol_ir.py \
  --source path/to/protocol.c \
  --output-dir runs/c_to_ir_demo \
  --name MyProtocol \
  --provider deepseek

本仓库包含 tpm2-sessions.c 的经过清理的 C-to-IR 演示工件。以下命令启动 UI 并打开演示：

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

http://127.0.0.1:8765/c-code-demo

协议 IR 审查

协议 IR 记录了最终形式化模型要有意义就必须正确的语义决策，包括：

• 协议角色和长期设置值；
• 消息构造、解析、加密、签名和验证；
• 值来源，包括新生成值、接收值、派生值和公开值；
• 证明目标所使用的事件；
• 保密性、认证、可执行性和预期反例目标；
• 攻击面假设。

抽象提示

UI 可以在启动后定位捆绑的抽象提示库，但除非用户在生成 Sapic+ 之前勾选 Use abstraction hints，否则不会使用它。启用该复选框后，后端会从以下位置检索证明工程提示：

examples/protocol-abstraction-cases.json

你可以替换此库或使用另一个库：

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --abstraction-hints-path /path/to/protocol-abstraction-cases.json

准备好的 IR 快照

examples/prepared_workflows/gpt55/ 包含基准用例的原始 IR 和人工审查后的 IR 快照。每个用例仅包含：

ir/protocol_ir.json
ir/protocol_ir.reviewed.json

这些文件是人工审查前后 IR 的紧凑示例。

用户测试过的 UI 工作流

examples/user_tested_workflows/deepseek_ui_20260615/ 包含两个在手动测试期间实际通过 UI 运行的工作流：

Toy
Sigfox

它们包含这些 UI 运行中的轻量级工件：输入/审查工件、提示词、LLM 调用元数据、生成的 Tamarin 模型、编译/修复输出和证明日志。不包含 API 凭据。

要在 UI 中检查它们，请使用此工作流库启动服务器：

python3 run_contract_review_ui.py \
  --run-dir runs/tmp_user_tested_review \
  --workflow-library-dir examples/user_tested_workflows/deepseek_ui_20260615 \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

然后打开 UI，使用 Select prepared workflow...，并选择 easy / Toy 或 easy / Sigfox。

现有工作流库

你可以选择性地公开一个准备好的工作流目录，以便从 UI 导入：

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --workflow-library-dir /path/to/prepared/workflows \
  --provider deepseek

基准输入

examples/ui_input_cases.json 包含为此审查 UI 准备的 18 个协议输入。它们以自然语言描述、假设、目标和预期结果的形式表示，可以复制到 UI 中。

对于手动测试，examples/ui_inputs.md 将相同用例包含在一个便于复制的 Markdown 文件中，分为 Easy、Medium 和 Hard 部分。

包含的用例：

Example, NSPK, Naxos, Toy, Woo_Lam, sigfox, EDHOC, KEMTLS, LAK06, SPLICE,
SSH, CCITT_X509, Denning_Sacco, Kao_Chow, NSSK, Neuman_Stubblebine,
Otway_Rees, Yahalom

归属

examples/ui_input_cases.json 中的基准输入整理自 AutoSM 18 用例基准输入。完整的 AutoSM 基准参考 Sapic+/Tamarin 文件未包含在此包中。

Ziyu Mao, Jingyi Wang, Jun Sun, Shengchao Qin, and Jiawen Xiong. "LLM-Aided Automatic Modeling for Security Protocol Verification." ICSE 2025. DOI: 10.1109/ICSE55347.2025.00197.

AutoSM 工件仓库：https://github.com/zerrymore/AutoSM

此包随附 LICENSE 中的 GPLv3 许可证文本。有关工件范围归属说明，请参见 NOTICE.md。