ProofFrog/ProofFrog
GitHub: ProofFrog/ProofFrog
一个用于验证密码学游戏跳跃证明中转换有效性的工具，通过领域特定语言 FrogLang 定义原语、方案和安全游戏，帮助初学者理解和构建可证明安全性论证。
Stars: 15 | Forks: 3
# ProofFrog
**一个用于检查密码学游戏跳跃证明中转换的工具。**
ProofFrog 检查游戏跳跃证明中转换的有效性——这是可证明安全性中用于证明密码学方案满足安全属性的标准技术。证明是用 FrogLang 编写的，这是一种用于定义原语、方案、安全游戏和证明的领域特定语言。ProofFrog 旨在处理入门级的证明，以牺牲表达能力和功能性来换取易用性。该引擎通过在 Z3 和 SymPy 等其他工具的帮助下将抽象语法树处理为规范形式，来检查每一个跳跃。ProofFrog 的引擎没有任何形式化的保证：其转换的可靠性尚未经过验证。
ProofFrog 可以通过 **命令行界面**、**基于浏览器的编辑器** 或用于与 AI 编程助手集成的 **MCP server** 使用。更多信息请访问 [prooffrog.github.io](https://prooffrog.github.io/)。
## 安装
需要 **Python 3.11+**。
### 从 PyPI 安装
```
python3 -m venv .venv
source .venv/bin/activate
pip install proof_frog
```
通过 pip 安装 ProofFrog 后，您可能需要下载示例仓库：
```
git clone https://github.com/ProofFrog/examples
```
### 从源码安装
```
git clone https://github.com/ProofFrog/ProofFrog
cd ProofFrog
git submodule update --init
python3 -m venv .venv
source .venv/bin/activate
pip install -e .
pip install -r requirements-dev.txt
```
## 网页界面
```
proof_frog web [directory]
```
启动一个本地 Web 服务器（默认端口 5173）并在浏览器中打开编辑器。`[directory]` 参数指定证明文件的工作目录；默认为当前目录。
网页界面允许您编辑 ProofFrog 文件（带有语法高亮），从网页编辑器验证证明，并探索每一步跳跃时的游戏状态。
## 命令行界面
| 命令 | 描述 |
|---------|-------------|
| `proof_frog parse
` | 解析文件并打印其 AST 表示 |
| `proof_frog check ` | 对文件进行类型检查以确保其格式正确 |
| `proof_frog prove ` | 验证游戏跳跃证明（`-v` 用于详细输出） |
| `proof_frog web [dir]` | 启动基于浏览器的编辑器 |
从源码安装时，请使用 `python3 -m proof_frog` 代替 `proof_frog`。
## 在 ProofFrog 中编写证明
请查看在 ProofFrog 中编写证明的[指南](https://github.com/ProofFrog/ProofFrog/blob/main/docs/guide.md)。
ProofFrog 使用四种文件类型来表达密码学证明的组成部分。
### 原语 (`.primitive`)
**原语** 定义了密码学操作的接口——其参数、类型和方法签名。以下是伪随机生成器接口的示例：
```
Primitive PRG(Int lambda, Int stretch) {
Int lambda = lambda;
Int stretch = stretch;
BitString evaluate(BitString x);
}
```
### 方案 (`.scheme`)
**方案** 实现了一个原语。方案可以由其他原语通用构建。以下是一次性填充对称加密方案的示例：
```
Scheme OTP(Int lambda) extends SymEnc {
Set Key = BitString;
Set Message = BitString;
Set Ciphertext = BitString;
Key KeyGen() {
Key k <- Key;
return k;
}
Ciphertext Enc(Key k, Message m) {
return k + m;
}
Message Dec(Key k, Ciphertext c) {
return k + c;
}
}
```
### 游戏 (`.game`)
**安全属性** 定义为一对游戏（左/右）。攻击者无法区分这两个游戏即构成了安全性。以下是 PRG 安全游戏的示例：
```
Game Real(PRG G) {
BitString Query() {
BitString s <- BitString;
return G.evaluate(s);
}
}
Game Random(PRG G) {
BitString Query() {
BitString r <- BitString;
return r;
}
}
export as Security;
```
### 证明 (`.proof`)
**证明脚本** 声明假设，陈述定理，并列出一系列游戏。每一对相邻的游戏必须被证明为代码等价（自动验证）或归约到某个假设的安全属性。以下片段展示了证明的基本部分：
```
proof:
let:
SymEnc proofE = SymEnc(ProofMessageSpace, ProofCiphertextSpace, ProofKeySpace);
assume:
OneTimeUniformCiphertexts(proofE);
theorem:
OneTimeSecrecy(proofE);
games:
OneTimeSecrecy(proofE).Left against OneTimeSecrecy(proofE).Adversary;
OneTimeUniformCiphertexts(proofE).Real compose R1(proofE) against OneTimeSecrecy(proofE).Adversary;
OneTimeUniformCiphertexts(proofE).Random compose R1(proofE) against OneTimeSecrecy(proofE).Adversary;
OneTimeUniformCiphertexts(proofE).Random compose R2(proofE) against OneTimeSecrecy(proofE).Adversary;
OneTimeUniformCiphertexts(proofE).Real compose R2(proofE) against OneTimeSecrecy(proofE).Adversary;
OneTimeSecrecy(proofE).Right against OneTimeSecrecy(proofE).Adversary;
```
## Vibe-Coding 一个证明
ProofFrog 还提供了一个 MCP server，用于与 Claude Code 等 AI 编程助手集成。请参阅 ProofFrog 网站了解如何[使用 Claude Code 进行 ProofFrog 证明的 vibe-coding 示例](https://prooffrog.github.io/hacs-2026/vibe/)。
## 示例
[`examples/`](https://github.com/ProofFrog/examples) 仓库包含主要改编自 Mike Rosulek 的 [*The Joy of Cryptography*](https://joyofcryptography.com/) 的原语、方案、游戏和证明。另请参阅 [ProofFrog 网站上的示例和教程](https://prooffrog.github.io/)。
## 许可证
ProofFrog 根据 [MIT 许可证](https://github.com/ProofFrog/ProofFrog/blob/main/LICENSE) 发布。
## 致谢
ProofFrog 由 Ross Evans 和 Douglas Stebila 创建，建立在由 Douglas Stebila 和 Matthew McKague 创建的 pygamehop 工具之上。有关 ProofFrog 设计的更多信息，请参阅 [Ross Evans 的硕士论文](https://uwspace.uwaterloo.ca/bitstream/handle/10012/20441/Evans_Ross.pdf)和 [eprint 2025/418](https://eprint.iacr.org/2025/418)。
我们感谢加拿大自然科学与工程研究委员会 (NSERC) 的支持。
包含来自 [vscode-codicons](https://github.com/microsoft/vscode-codicons) 项目的图标。标签：Android, DSL, Game-Hopping, MCP Server, odt, Python, SymPy, Web编辑器, Z3, 二进制发布, 可证明安全, 安全协议分析, 安全证明, 定理证明器, 密码学, 开源工具, 形式化验证, 手动系统调用, 抽象语法树, 教学工具, 文档结构分析, 无后门, 符号执行, 计算机辅助证明, 领域特定语言