# PQC-MAVP

**Repository Path**: Forever7368/PQC-MAVP

## Basic Information

- **Project Name**: PQC-MAVP
- **Description**: 面向后量子密码的协议多智能体验证平台
- **Primary Language**: Python
- **License**: GPL-2.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 46
- **Forks**: 34
- **Created**: 2025-10-28
- **Last Updated**: 2026-02-14

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# ProtocolMind - 面向后量子密码的多智能体协议形式化验证平台

## 项目概述

ProtocolMind是一个基于LangChain和LangGraph的多智能体系统，专门用于网络协议的形式化分析和验证，特别针对后量子密码学环境进行了优化。系统通过四个专门的智能体协作，将自然语言协议描述转换为Tamarin Prover形式化模型，并自动执行安全验证。

## 核心特性

- 🤖 **多智能体架构**: 四个专门化的智能体协作完成协议分析
- 🔍 **智能协议分析**: 从自然语言描述中提取结构化信息，支持链式思维推理
- 📝 **自动建模**: 生成符合Tamarin规范的形式化模型，支持后量子密码原语
- ✅ **自动验证**: 集成Tamarin Prover执行安全验证，支持详细攻击路径分析
- 🔧 **智能修复**: 提供验证失败时的修复建议，攻击路径转自然语言建议准确率≥85%
- 🌐 **REST API**: 完整的HTTP API接口，支持异步任务管理
- 📊 **工作流编排**: 基于LangGraph的状态管理
- 🚀 **性能优化**: 建模时间缩短≥80%，语法通过率≥98%
- 🔐 **后量子支持**: 支持Kyber、Dilithium、Falcon、SPHINCS+等后量子密码原语
- 🎯 **场景适配**: 支持IoT、6G通信、边缘计算等多种场景的协议变体

## 智能体架构

### 1. AnalysisAgent (分析智能体)
- **功能**: 从自然语言协议描述中提取结构化信息
- **输入**: 协议描述文本
- **输出**: JSON格式的协议分析结果
- **提取内容**: 参与方角色、消息流、密码原语、安全目标

### 2. ModelingAgent (建模智能体)
- **功能**: 基于协议分析生成Tamarin形式化模型
- **输入**: 协议分析结果
- **输出**: .spthy格式的形式化模型
- **生成内容**: 角色定义、规则、密码函数、安全目标lemma

### 3. VerificationAgent (验证智能体)
- **功能**: 执行Tamarin Prover验证
- **输入**: 形式化模型
- **输出**: 验证结果和攻击路径
- **验证内容**: 安全目标、攻击路径分析、验证时间统计

### 4. RepairAgent (修复智能体)
- **功能**: 分析验证失败原因并提供修复建议
- **输入**: 验证结果和原始模型
- **输出**: 修复建议和代码示例
- **提供内容**: 根本原因分析、具体修复建议、代码修改示例

## 技术栈

- **框架**: LangChain + LangGraph
- **LLM**: GPT-4/GPT-3.5
- **验证工具**: Tamarin Prover
- **API框架**: FastAPI
- **语言**: Python 3.9+
- **状态管理**: LangGraph StateGraph

## 安装和配置

### 1. 环境要求
```bash
Python 3.9+
pip
Tamarin Prover (可选，用于本地验证)
```

### 2. 安装依赖
```bash
cd protocolmind_backend
pip install -r requirements.txt
```

### 3. 环境配置
```bash
# 复制环境配置文件
cp .env.example .env

# 编辑.env文件，设置以下变量：
OPENAI_API_KEY=your_openai_api_key_here
OPENAI_MODEL=gpt-4
OPENAI_TEMPERATURE=0.1
TAMARIN_PROVER_PATH=/path/to/tamarin-prover
MAX_RETRIES=2
TIMEOUT_SECONDS=1800
LOG_LEVEL=INFO
```

### 4. 启动服务
```bash
python run.py
```

服务将在 `http://localhost:8000` 启动

## API接口

### 基础接口

- `GET /` - 根路径，返回服务信息
- `GET /health` - 健康检查
- `GET /docs` - API文档 (Swagger UI)

## 新增API接口

### 协议模板接口
- `GET /templates` - 获取所有可用的协议模板
- `GET /templates/{template_id}` - 获取特定协议模板详情

### 场景适配接口
- `GET /scenarios` - 获取所有可用的场景配置
- `POST /adapt/{template_id}/{scenario_id}` - 将协议模板适配到特定场景

### 质量监控接口
- `GET /quality/dashboard` - 获取质量指标仪表板
- `GET /quality/metrics/{metric_type}` - 获取特定指标的历史数据

### 任务管理接口
- `GET /tasks` - 列出所有任务
- `GET /tasks/statistics` - 获取任务统计信息
- `DELETE /tasks/{task_id}` - 取消运行中的任务

### 使用示例

#### 1. 协议分析
```bash
curl -X POST "http://localhost:8000/analyze" \
  -H "Content-Type: application/json" \
  -d '{
    "protocol_description": "简单的认证协议：1. 客户端发送用户名密码 2. 服务器验证 3. 返回令牌"
  }'
```

#### 2. 完整工作流
```bash
curl -X POST "http://localhost:8000/workflow" \
  -H "Content-Type: application/json" \
  -d '{
    "protocol_description": "Diffie-Hellman密钥交换协议：1. Alice和Bob协商参数 2. 交换公钥 3. 计算共享密钥"
  }'
```

## 数据格式

### 协议分析结果 (protocol_analysis.json)
```json
{
  "roles": ["Client", "Server"],
  "message_flow": [
    {"from": "Client", "to": "Server", "content": "username, password", "step": 1}
  ],
  "primitives": ["Hash", "Symmetric_Encryption"],
  "security_goals": ["authentication", "confidentiality"]
}
```

### 验证结果 (verification_result.json)
```json
{
  "status": "verified|falsified|timeout|error",
  "verified_lemmas": ["authentication", "confidentiality"],
  "failed_lemmas": [],
  "attack_traces": [],
  "verification_time": 15.5,
  "error_message": null
}
```

## 测试和示例

### 运行测试
```bash
# 测试分析智能体
python examples.py analysis

# 测试建模智能体
python examples.py modeling

# 测试完整工作流
python examples.py workflow

# 测试API接口
python examples.py api
```

### 示例协议
系统内置了多个示例协议用于测试：
- 简单认证协议
- Diffie-Hellman密钥交换
- Otway-Rees协议
- Needham-Schroeder协议

## 工作流说明

1. **Analysis**: 分析协议描述，提取结构化信息
2. **Modeling**: 基于分析结果生成Tamarin模型
3. **Verification**: 执行Tamarin Prover验证
4. **Repair**: 仅在验证失败时触发，提供修复建议

### 质量指标
- 生成模型语法正确率: ≥98%
- 安全目标覆盖率: ≥90%
- 验证结果准确率: 100%
- 端到端执行时间: <10分钟
- 建模效率提升: ≥80%
- 攻击路径分析准确率: ≥85%
- 后量子密码兼容性: ≥80%

## 错误处理

- **重试机制**: 建模和验证阶段最多重试2次
- **超时处理**: 单个步骤超时30分钟自动终止
- **错误恢复**: 详细的错误信息和恢复建议
- **日志记录**: 完整的执行日志和调试信息

## 扩展和定制

### 添加新的智能体
1. 继承 `BaseAgent` 类
2. 实现核心方法
3. 在 `workflow.py` 中集成到工作流

### 自定义提示词
修改各智能体的 `system_prompt` 来优化性能

### 集成其他验证工具
在 `VerificationAgent` 中添加对其他形式化验证工具的支持

## 贡献指南

1. Fork 项目
2. 创建功能分支
3. 提交更改
4. 创建 Pull Request

## 许可证

MIT License

## 联系方式

如有问题或建议，请通过以下方式联系：
- 项目Issues
- 邮箱: [your-email@example.com]

## 引用的仓库

- **ElasticShield**
  - 仓库地址: [https://gitee.com/linjhs/elastic-shield](https://gitee.com/linjhs/elastic-shield)
  
---

**注意**: 使用前请确保已正确配置OpenAI API密钥和Tamarin Prover路径。