# verifpal

**Repository Path**: sakana_ctf/verifpal

## Basic Information

- **Project Name**: verifpal
- **Description**: No description available
- **Primary Language**: Go
- **License**: GPL-3.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-10-21
- **Last Updated**: 2025-10-21

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

<!---
# SPDX-FileCopyrightText: © 2019-2022 Nadim Kobeissi <nadim@symbolic.software>
# SPDX-License-Identifier: CC-BY-SA-4.0
-->

# [Verifpal](https://verifpal.com)

## 什么是 Verifpal？

<img src="https://verifpal.com/res/img/png/pose1.png" alt="" align="left" height="300" style="margin:10px" />

Verifpal 是一款用于验证密码协议安全性的新软件。它基于符号化形式验证领域的最新研究，主要目标是在不牺牲全面形式验证功能的前提下，更好地吸引现实世界的从业者、学生和工程师。

为此，Verifpal 引入了一种新颖直观的协议建模语言，比现有工具使用的语言更易于编写和理解。同时，Verifpal 能够在具有无限会话和新鲜值的主动攻击者模型下分析协议，并支持高级安全属性的查询，如前向安全性或密钥泄露冒充。

Verifpal 已被用于验证 Signal、Scuttlebutt、TLS 1.3、Telegram 等协议的安全属性。这是一个以社区为中心的项目，采用 GPLv3 许可证发布。

#### 直观的协议建模语言

Verifpal 语言旨在使协议的描述方式接近非正式对话中的描述，同时仍保持精确性和足够的表达能力以进行形式化建模。Verifpal 通过显式主体进行协议模型推理：Alice 和 Bob 存在并拥有独立状态。

#### 避免用户错误的建模

Verifpal 不允许用户自定义密码学原语。相反，它内置了密码学函数——这旨在消除用户错误定义基本密码操作的可能性。

#### 易于理解的分析输出

当发现查询存在矛盾时，结果会以可读格式呈现，将攻击与现实场景关联起来。通过使用特定术语（如通过临时密钥的中间人攻击）来说明攻击如何实现。

#### 友好且集成化的软件

Verifpal 提供 Visual Studio Code 扩展，支持语法高亮、自动格式化、实时分析、图表可视化等功能，让开发者在编写模型时就能获得深入洞察。

## Verifpal 是测试版软件

Verifpal 的语法、语义和分析方法已通过手工和 Coq 定理证明器进行形式化，从而获得了更高级别的保证。但由于其发展时间相对较短（尤其是与已开发二十多年的 [ProVerif](https://proverif.inria.fr) 等工具相比），仍被归类为测试版软件。

## 入门指南

### Verifpal 用户手册

[Verifpal 用户手册](https://verifpal.com/res/pdf/manual.pdf) 是使用 Verifpal 进行密码协议分析的重要入门指南。强烈建议在使用 Verifpal 前阅读该手册。

### 获取 Verifpal

在 Windows 上，推荐通过 [Scoop](https://scoop.sh) 包管理器安装，可自动更新：

```
scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git
scoop install verifpal
```

在 Linux 和 macOS 上，推荐通过 [Homebrew](https://brew.sh) 包管理器安装，可自动更新：

```
brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal
```

其他方式：

- *手动下载安装发布版*：适用于 Windows、Linux、macOS 和 FreeBSD 的发布版可在此处获取。
- *从源码编译*：请继续阅读！

### 从源码构建 Verifpal

构建 Verifpal 需先安装 [Go](https://golang.org)。请查阅 [Go 入门指南](https://golang.org/doc/install) 了解如何为您的系统安装 Go。

#### 安装依赖

Verifpal 依赖 [Aurora](https://github.com/logrusorgru/aurora) ANSI 彩色打印机、[Cobra](https://github.com/spf13/cobra) CLI 应用库和 [Pigeon](https://github.com/mna/pigeon) PEG 解析器生成器。执行 `make dep` 即可安装。

#### 编译 Verifpal

- *Windows*：执行 `Build` 可构建适用于 Windows、Linux、macOS 和 FreeBSD 的版本（会自动安装依赖）。
- *Linux/macOS/FreeBSD*：执行 `make all` 可构建多平台版本。

构建产物位于 `build/` 目录。

### Visual Studio Code 扩展

Verifpal 提供 Visual Studio Code 扩展，支持语法高亮、自动格式化、实时分析、图表可视化等功能。在 VS Code 中搜索 "Verifpal" 即可安装，详情参见[此链接](https://github.com/symbolicsoft/verifpal-vscode)。

## 讨论

注册 [Verifpal 邮件列表](https://lists.symbolic.software/mailman/listinfo/verifpal) 可获取最新动态并参与讨论。

## 许可证

Verifpal 及其 VS Code 扩展由 Symbolic Software 发布，是基于 [GNU 通用公共许可证 v3](https://www.gnu.org/licenses/gpl-3.0.en.html) 的自由开源软件。用户手册采用 [知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议](https://creativecommons.org/licenses/by-nc-nd/4.0/)。

© 版权所有 2019-2022 Nadim Kobeissi。保留所有权利。"Verifpal" 名称及标识均为 Nadim Kobeissi 注册商标。