# 密码安全论证包：威胁模型、协议与证明/攻击对照 工作单元：W-M11；版本：2026-10-21.workunits.2；复核：2026-10-20 对一个锁定密码构造/协议交付明确安全游戏或符号模型、可检查论证或攻击及精确适用范围。 ## 当前用法 安全目标/模型可锁定时，可整包委派形式论证候选；模型生成、完整证明和实现安全分别接收。 依据：CrypFormBench专门评估密码模型解释、生成、补全、转换和修正，语法可执行与安全语义需分开看。；ShannonProver v1在专家给定安全模型及引理级分解后自动构建EasyCrypt证明，含部署协议相关个案。 来源状态：active 本站记录：本站本任务AI运行数、成功率、实际成本及人工介入量均为null；代表例为交付设计，未执行。 条件： - 威胁模型与安全定义可核 - 工具和假设固定 - 有已知攻击/不安全变体控制 ## 请求与范围 研究/工程团队需评估构造、协议变体或现有论证，避免自然语言安全主张无模型。 安全定义、攻击者、假设、协议模型、证明/反例为一包；代码执行和物理泄漏另按W-M12验收；非授权实际攻击不纳入。 ## 输入 - 方案与安全目标：构造/协议版本、角色/消息、密钥/nonce生成和复用条件、参数；安全游戏/攻击者能力/信道与腐化模型。 - 形式环境与先验：符号或计算模型、允许假设/理想化、目标EasyCrypt/Tamarin/CryptoVerif等版本、已知攻击/论文及允许改动区。 - 研究边界：目标证明/攻击、可用计算/搜索预算；完整安全模型由可信输入提供或分阶段核对，不从可编译反推。 ## 交付物 - 原方案—安全定义/模型—形式声明对应和假设清单 - 可重建完整形式开发/证明、攻击trace或条件性未解义务 - 安全游戏/辅助引理的依赖及差异，非平凡性/可达性检查 - 适用参数/攻击复杂性/理想化和代码落地缺口；来源及后续修订 ## 验收 1. 安全模型忠实 方法：独立核对角色、密钥、nonce、消息绑定和攻击者查询/腐化能力；用已知不安全变体作为负控制，验证模型能暴露攻击。 拒收：删去重放/腐化能力使协议“安全”；加理想信道而原实现没有。 2. 完整形式结果不藏未证部分 方法：固定环境重放全部目标，核对admit/axiom/假设/solver与证明依赖；游戏跃迁和引理连接到最终目标，局部通过单列。 拒收：多个引理通过但最终安全界未证；把构造安全假设直接当最终定理。 3. 攻击/反例在原模型内 方法：重放trace/代码，检查前提、复杂性、概率、参数和预算；区分符号攻击与可实现计算攻击。 拒收：攻击需要超出允许查询或不现实时间，却写破坏目标安全级别。 4. 保证与部署不混淆 方法：核对报告只声称已证模型/参数；理论保证到代码/随机源/侧信道/密钥管理缺口必须可见。 拒收：IND-CPA证明被说成认证加密/抗侧信道；nonce重复时仍套原安全界。 ## 具体例子 输入：设计例：锁定使用唯一nonce的AEAD保密/完整性游戏，再对nonce可能复用的协议变体分析；消息格式、查询与腐化条件明定。 预期产物：安全模型/目标、完整证明或有效攻击trace、参数界和部署限制；没有本例运行。 失败：证明只覆盖唯一nonce却声明支持重复nonce；完成辅助引理却省略最终游戏跃迁。 ## 工作重组 以前：密码专家写安全模型/游戏，证明工程师手工分解和填tactic，改模型后再交接。 现在：代理可搜索中间游戏、引理和证明并响应checker；来源/安全定义与最终游戏连接独立核对，不固定所有密码任务用同一工具。 保留： - 安全目标及攻击者能力确认 - 安全假设和最终部署采纳 新增： - 游戏/引理与最终目标版本同源 - 符号/计算/实现保证分开 - 已知攻击负控制 ## 人的责任与失败接管 密码研究接收者确认模型、假设与可用范围；代理可探索模型候选、证明与反例，形式工具核查适用目标，发布者承担安全主张的范围责任。 不能证明时列最小未解引理和已证范围；发现攻击保留可重放输入/trace；模型歧义先给相异解释及影响，不偷偷削弱攻击者。 ## 尚待补足 - 10月代码的项目级搜索超出v1已验证范围 - 无本例可调用工具的稳定性数据 ## 职业与团队下一步 密码研究、形式密码分析 安全模型、完整目标/证明或有效攻击与参数/假设说明 补密码安全定义、工具语言和已知攻击背景。 /explore?purpose=career&domain=math 模型、游戏分解还是tactic成本限制研究？ 代理承担证明工程/候选攻击，接收者核对安全模型、完整覆盖和部署适用。 用一个公开案例完整重放，再选未泄漏引理/协议变体测迁移。 /explore?purpose=team&domain=math ## 证据与关系 - CrypFormBench v1：密码形式模型能力：https://arxiv.org/html/2606.25561v1 定位：§3五类任务；§5设置/结果；§6错误与语义；代码b5540654533dbb7a491ece75e50c8da67defc604；公开 2026-06-24；核查 2026-10-20；复查 2026-11-20 支持：密码形式分析专属的能力/失败证据。；模型语义失配决定验收边界。 未覆盖：不是生产代码、硬件泄漏或任意新密码安全性；历史模型/题集限定。；本AEAD变体为设计例，未执行。 - ShannonProver v1：密码引理级形式证明：https://arxiv.org/html/2607.02847v1 定位：Abstract；§V evaluation/case studies；AppendixC；公开 2026-07-03；核查 2026-10-20；复查 2026-11-20 支持：明确的密码证明工程成果与输入边界。 未覆盖：不是独立设计完整安全模型，也不是代码/物理安全证明；部分污染控制材料不公开。 - Shannon Prover固定源码与项目级入口：https://github.com/SkyShannonProver/shannon-prover/blob/60701dbe37ee72075e60e655a076e282efe7485e/README.md 定位：What does Shannon automate / Install / Project-level proving / Benchmark guide；公开 2026-10-01（固定提交）；核查 2026-10-20；复查 2026-11-20 支持：当前实现可检查及运行入口。 未覆盖：源码方法声明不是该宽范围已测成功率。 ## 任务级判断与证据 采用方式：分阶段接收 从证据到建议：密码专属评估和Shannon个案支持自动证明工程；它们都不能替代模型选择与部署条件。因此给代理完整论证目标，按语义/最终证明和有效攻击接收，保留未解出口。 当前可用性：mixed；公开资料和工具入口已核对；论文配置、当前实现声明及本任务成绩分别记录，未运行本任务。 - Shannon Prover：https://github.com/SkyShannonProver/shannon-prover/tree/60701dbe37ee72075e60e655a076e282efe7485e 60701dbe…；vendored EasyCrypt及locked Python；macOS/Linux、opam/Python≥3.12/uv及模型key；严格live eval需Linux+bubblewrap，未运行。 - CrypFormBench：https://github.com/Secbrain/CrypFormBench/tree/b5540654533dbb7a491ece75e50c8da67defc604 b5540654…；论文v1；公开数据/实验及多语言工具，非统一即用协议安全产品。 ### CrypFormBench专门评估密码模型解释、生成、补全、转换和修正，语法可执行与安全语义需分开看。 依据身份：外部报告结果；状态：active - CrypFormBench v1：密码形式模型能力：https://arxiv.org/html/2606.25561v1 定位：§3任务；§5评估；§6语义错误；关系：direct 支持：密码形式分析专属的能力/失败证据。 限制：不是生产代码、硬件泄漏或任意新密码安全性；历史模型/题集限定。 核查：2026-10-20；来源状态：active 配置：v1；9模型、7工具语言，符号与计算模型；任务类型及分母依论文分开，本文不把总体分当任务完成概率。 适用限制：不是生产代码、硬件泄漏或任意新密码安全性；历史模型/题集限定。 相关进展（本条判断）： - 密码模型的生成/转换开始独立于通用编码测量：/explore?purpose=understand&domain=math&window=all#P-M-CRYPFORM 首次公开 2026-06-24 ### ShannonProver v1在专家给定安全模型及引理级分解后自动构建EasyCrypt证明，含部署协议相关个案。 依据身份：外部报告结果；状态：active - ShannonProver v1：密码引理级形式证明：https://arxiv.org/html/2607.02847v1 定位：Abstract；evaluation/case studies；AppendixC；关系：direct 支持：明确的密码证明工程成果与输入边界。 限制：不是独立设计完整安全模型，也不是代码/物理安全证明；部分污染控制材料不公开。 核查：2026-10-20；来源状态：active 配置：arXiv2607.02847v1；专家供模型/分解；EasyCrypt checker与多分支调度；不同任务预算/可获得材料按原文，不推本例成本。 适用限制：不是独立设计完整安全模型，也不是代码/物理安全证明；部分污染控制材料不公开。 相关进展（本条判断）： - 密码引理证明工程已有EasyCrypt代理案例：/explore?purpose=understand&domain=math&window=all#P-M-SHANNON 首次公开 2026-07-03；判断变化 2026-07-03 ### 10月固定源码提供游戏/辅助引理分解搜索与完整文件检查入口，比v1论文输入范围更宽的声明需另验证。 依据身份：工具与方法依据；状态：active - Shannon Prover固定源码与项目级入口：https://github.com/SkyShannonProver/shannon-prover/blob/60701dbe37ee72075e60e655a076e282efe7485e/README.md 定位：What does Shannon automate / project-level guide；关系：direct 支持：当前实现可检查及运行入口。 限制：源码方法声明不是该宽范围已测成功率。 核查：2026-10-20；来源状态：active 适用限制：源码方法声明不是该宽范围已测成功率。 ### 给出可核对安全目标后，委派完整论证候选并以模型、最终目标和攻击控制接收；代码部署另验。 依据身份：有条件的编辑推断；状态：active - CrypFormBench v1：密码形式模型能力：https://arxiv.org/html/2606.25561v1 定位：semantic alignment/error analysis；关系：adjacent 支持：模型语义失配决定验收边界。 限制：本AEAD变体为设计例，未执行。 核查：2026-10-20；来源状态：active 适用限制：本AEAD变体为设计例，未执行。 ## 情境变化 ### 符号协议模型 输入变化：秘密/认证目标与Dolev-Yao式理想化。 判断变化：可交模型/trace候选，不套计算安全证明。 验收变化：角色/消息绑定、可达性和攻击者能力，有限搜索界与无界保证分开。 ### 固定计算安全引理 输入变化：安全游戏/假设已可信且只缺proof。 判断变化：可整包委派固定引理，与M10程序或M01数学义务不同上下文。 验收变化：EasyCrypt完整检查、允许假设和最终目标覆盖；不以子引理通过当完整协议。 ### 新构造/密码分析 输入变化：模型和构造都可变，可能研究新攻击。 判断变化：探索候选与反例；需要独立文献/复杂性及原模型核对。 验收变化：假设/参数/复杂性/攻击成功定义，未解不等于安全。 ### 既有构造的计算安全模型 输入变化：对已有原语/协议定义或核对计算安全游戏、查询/腐化能力与安全界，不要求先提出新构造或仅补局部引理。 判断变化：可委派模型/游戏及论证候选，语义先核再查最终安全目标。 验收变化：假设/参数/攻击者查询、nonce/随机性和游戏跃迁逐项对应原方案；局部证明和完整安全界分开。 研究前沿：论文v1在专家给模型与引理分解下完成证明工程；10月固定源码进一步声明项目级分解搜索，属于可检实现入口，需另试验，不能冒称论文已验证更宽能力。 下一项验证：固定一个公开协议或AEAD安全游戏，隐藏参考证明，对照已知nonce复用不安全变体；独立重建全部目标及模型对应，保存未解引理和总预算。 未来改判信号： - 扩大：未见协议/游戏分解下，完整安全目标在固定攻击者模型中通过，独立密码分析一致。 - 收缩：只会补语法，漏nonce/腐化假设、改变目标或跳过最终目标；缩到固定引理补全。 ## 与本单元直接关联的进展 ### 密码引理证明工程已有EasyCrypt代理案例 公开 2026-07-03；判断变化 2026-07-03 给定模型和引理分解后可以委派证明脚本搜索。 支持范围：10月源码更宽分解能力不继承v1已测范围。 来源状态：active /explore?purpose=understand&domain=math&window=all&kind=all#P-M-SHANNON ### 密码模型的生成/转换开始独立于通用编码测量 公开 2026-06-24 符号与计算安全模型有专属形式分析评价。 支持范围：不覆盖生产代码/硬件泄漏或现实部署可靠性。 来源状态：active /explore?purpose=understand&domain=math&window=all&kind=all#P-M-CRYPFORM 领域背景与未来情景：/explore?purpose=understand&domain=math ## 工具与采用佐证