nickharris808/pqc-formal-corpus

# pqc-formal-corpus [](LICENSE) [](src/pqc_formal_corpus/data/pqc_formal_corpus.jsonl) [](DATASET_CARD.md) [](tests/) [](pyproject.toml) **形式化验证一个后量子握手究竟需要什么？这里是全部 122 个结果，均已命名。** 来自一次持续的多证明器验证工作的定理、引理、不变量和目标 —— Lean, EasyCrypt, Tamarin, TLA+, CryptoVerif, Squirrel —— 汇总在一个可查询的文件中。 **📖 完整文档、教程与概念指南：** ## 为什么会有这个项目 论文只报告了协议*已经*被验证。它们很少公布工作的具体形态： 需要多少个命名结果，哪个证明器承担了哪部分工作，以及其中有多少是对照（controls） 而不是属性。 这种形态很有用。它告诉你验证工作实际上花在了哪里， 它为第三方提供了一个具体的重新推导目标列表， 而且这种东西从代码库中重构起来很繁琐，但发布出来却很简单。 所以：122 行，六种方言（dialect），一个 JSONL。 ## 安装 ``` pip install git+https://github.com/nickharris808/pqc-formal-corpus ``` 尚未发布到 PyPI。该数据集也在 Hugging Face Hub 上，完全不需要 安装 —— 请参阅下面的用法代码片段。 零依赖。 ## 30 秒快速入门 ``` from pqc_formal_corpus import load, by_prover, by_category results = load() len(results) # 122 by_prover(results) # where the effort went ``` ## 实战示例 —— 实际输出 ``` >>> from pqc_formal_corpus import load, by_prover >>> results = load() >>> len(results) 122 >>> by_prover(results) {'cryptoverif': 1, 'easycrypt': 51, 'lean': 20, 'squirrel': 1, 'tamarin': 35, 'tla': 14} >>> [r.name for r in results if r.category == "resource-bound"] ['bounded', 'bounded_at_canonical', 'naive_unbounded', 'separation', 'window_admits_and_bounded', 'window_nonempty'] >>> next(r for r in results if r.name == "bounded") Result(prover='lean', name='bounded', kind='theorem', module='Bound', category='resource-bound', polarity='bound') ``` **EasyCrypt 承担了 122 个中的 51 个** —— 这正是计算归约（computational reductions）所在。Tamarin 处理了 35 个符号结果，Lean 处理了 20 个机器检查的边界（bounds）。这种分布本身*就是* 核心发现。 ## CLI ``` pqc-corpus stats # summary by prover and category pqc-corpus query --prover lean --category resource-bound pqc-corpus export --format csv -o corpus.csv # or jsonl, json, parquet ``` `--json` 是全局的。每个未知的过滤值都会列出有效值，而 不是什么都不返回。 ## Schema `prover` · `name` · `kind` · `module` · `category` · `polarity` 前四个是原样提取的。**`category` 和 `polarity` 是从标识符字符串派生出的启发式结果** —— 适合用于过滤，但不是既定事实。请参阅 [`DATASET_CARD.md`](DATASET_CARD.md) 了解完整的 schema、来源和局限性。 ## 这里没有什么 **没有证明主体，没有 tactic 脚本，没有模型源码。** 一个名称及其来源就是一个 索引；机械化的论证保持闭源， 因为这些证明中有几个直接编码了修复机制。一个测试会在发布的文件中 grep 查找证明语法，如果 出现任何证明语法，测试就会失败。 **ProVerif 贡献了零行。** 它的模型是查询驱动的，其形式不被这个提取器视为命名结果 —— 而且它的内置 `attacker` 谓词一直被提取为唯一的“ProVerif 结果”，直到 denylist 阻止了它。这是一个被如实披露的真实局限，而不是被掩盖过去。 ## 重新生成它 ``` python -m pqc_formal_corpus.build \ src/pqc_formal_corpus/data/pqc_formal_corpus.jsonl ``` 输出是已排序且字节稳定的，因此任何更改都会在重新生成时显示为 干净的 diff。 ## 测试 ``` pip install -e ".[dev]" && pytest # 66 passed ``` 测试涵盖了形态、唯一性、内置 denylist、边界（moat boundary）、已知名称上的启发式 行为，以及数据是打包在 wheel **内部**而不是 在其旁边。 ## 范围 一次工作中命名的结果的索引。**不是证明本身**，不是基准测试，不是完备性声明 —— 一个未被命名的属性仅仅是不存在，而且在这里缺失并不意味着 协议有问题。 ## 相关资源 [`pqc-mfb`](https://github.com/nickharris808/pqc-mfb) (一个可评分的基准测试) · [`pqc-sizes`](https://github.com/nickharris808/pqc-sizes) · [`farkas-check`](https://github.com/nickharris808/farkas-check) (其中一个边界， 可在设备上重新验证) 这个语料库列出了已被证明的内容。证明及其建立的机制是一个 独立的闭源代码库。 相关主题已由提交的临时专利申请涵盖。 如需商业用途，请发起一个 [GitHub Discussion](https://github.com/nickharris808) 或 issue。 ## 诚实的范围 **这证明了什么。** 一次持续的验证工作将这 122 个结果命名， 使用这六种证明器方言，在这些模块中。`prover`, `name`, `kind` 和 `module` 是从提交的证明器源码中原样提取的。 **这没有证明什么。** - **不代表这些结果是正确的。** 这是一个*名称*索引。证明不在这里， 因此此数据集中的任何内容都无法对照证明进行检查。关于一个你 实际可以运行的开发，请参阅 [`pqc-bounds-lean`](https://github.com/nickharris808/pqc-bounds-lean) —— 其中有 20 个名称 在那里，有 0 个 `sorry`。 - **`category` 和 `polarity` 不是既定事实。** 两者都是完全通过子字符串匹配从标识符字符串中派生出来的， 从未来自证明主体。它们的存在是为了让 122 行数据 可浏览，但它们出错的频率足够高，你不应该基于它们得出结论。有 15 行数据落在了 `polarity: other`，因为它们的名称 不包含启发式方法能识别的信号。 - **不完整。** 提取是基于正则表达式的，因此以不寻常 语法形式声明的结果会被遗漏。ProVerif 贡献了 **零** 行正是 因为这个原因 —— 这是一个真实的局限性，已被披露而不是被掩盖。 - **不是基准测试。** 没有任务，没有拆分，没有指标。如需可评分的基准测试，请参阅 [`pqc-mfb`](https://github.com/nickharris808/pqc-mfb)。 - **不能代表整个领域的现状。** 一次努力，一个协议族。EasyCrypt 承担了 122 个结果中的 51 个，这反映了这次工作中的计算证明 所在的位置，而不是说 EasyCrypt 的结果更重要。 ## PQC 迁移工具包 面向将认证密钥交换迁移到后量子（post-quantum）团队的 11 个免费工具。它们负责**查找和测量**；它们不负责修复。 | 工具 | 功能 | 位置 | |---|---|---| | [pqc-sizes](https://github.com/nickharris808/pqc-sizes) | 大小、分片数量以及双侧重组窗口 | PyPI | | [pqc-sizes-js](https://github.com/nickharris808/pqc-sizes-js) | 适用于 Node 和浏览器的相同算法 | npm | | [pqc-guard-action](https://github.com/nickharris808/pqc-guard-action) | 当窗口为空时使构建失败 | GitHub Action | | [pqc-dos-embedded](https://github.com/nickharris808/pqc-dos-embedded) | 169 行 C 代码：真实 64 KB 设备上的失败案例 | 源码 | | [farkas-check](https://github.com/nickharris808/farkas-check) | 在设备上重新验证边界，无需 SMT solver | 源码 | | [pqc-migration-mcp](https://github.com/nickharris808/pqc-migration-mcp) | 面向 AI agent 的六个 MCP 工具 | PyPI | | [pqc-mfb](https://github.com/nickharris808/pqc-mfb) | 322 个案例 · 39 个失败类别 · 评分器 | PyPI | | [pqc-mfb (数据)](https://huggingface.co/datasets/nickh007/pqc-mfb) | 作为数据集的基准测试 | HF | | **pqc-formal-corpus** ← 您在这里 | 122 个命名的形式化结果，6 个证明器 | HF | | [pqc-bounds-lean](https://github.com/nickharris808/pqc-bounds-lean) | Lean 4 中的相同边界 — 0 `sorry`, 0 imports | 源码 | | [pqc-dos-gate-rtl](https://github.com/nickharris808/pqc-dos-gate-rtl) | 可综合 RTL 中的门电路，5 个 Yosys 证明 | 源码 | | [pqc-explorer](https://huggingface.co/spaces/nickh007/pqc-explorer) | 在您的浏览器中尝试，无需安装 | HF Space | **第一次使用？** [端到端教程](https://github.com/nickharris808/pqc-sizes/blob/main/TUTORIAL.md) 会在大约十分钟内，通过一个现实的迁移案例带您了解所有这些工具：大小 -> 窗口 -> CI 门控 -> 基准测试。 **时间紧迫？** [`pqc-sizes`](https://github.com/nickharris808/pqc-sizes) 能在五秒钟内告诉您您的凭据是否会分片，以及是否存在安全上限。 [`pqc-explorer`](https://huggingface.co/spaces/nickh007/pqc-explorer) 可以在浏览器中完成同样的操作，且无需安装。 ### 闭源核心 修复 39 个失败类别 —— 降级绑定、重传安全安装、分片记录、漫游前向保密、多链路密钥隔离、准入控制、组密钥绑定 —— 是一个独立的闭源代码库。相关主题已由提交的临时专利申请涵盖。 这种分离是经过测量的，而非断言的：在复制噪声控制下，32 个修复机制中仅有 **4 个** 是外部可区分的，因此发布这些检测器并不会泄露修复机制本身。 如需商业授权，请对这些仓库中的任何一个发起 [GitHub Discussion](https://github.com/nickharris808/pqc-sizes/discussions) 或 issue。 ## License Apache-2.0。请参阅 [LICENSE](LICENSE)、[CONTRIBUTING.md](CONTRIBUTING.md) 和 [SECURITY.md](SECURITY.md)。

标签：Python, 后量子密码学, 密码学, 形式化验证, 手动系统调用, 无后门, 时序数据库, 逆向工具