spore-protocols

Security Protocols Open Repository (SPORE)数据集是一个包含安全协议规范的全面集合，这些协议已经过形式化分析。每个协议规范包括主体声明（协议参与者）、加密原语（密钥、随机数、时间戳等）、带有加密操作的消息交换序列以及对加密、签名等安全操作的清晰表示。数据集包含两种格式：指令型和对话型。

原始信息汇总

Security Protocols Open Repository (SPORE) Dataset 概述

数据集基本信息

• 许可证: MIT
• 任务类别: 文本生成、问答、文本分类
• 语言: 英语
• 标签: 密码学、安全、网络安全、安全协议、协议验证、形式化方法、SPORE、Clark-Jacob库、AVISPA库、AVANTSSAR库
• 数据集名称: Security Protocols Open Repository (SPORE)
• 规模类别: n<1K

数据集配置

• instruction配置: 数据文件路径为"instruction.jsonl"
• conversation配置: 数据文件路径为"conversation.jsonl"

数据集描述

安全协议开放存储库是经过正式分析的安全协议综合集合。每个协议规范包含：

• 主体声明（协议参与者）
• 密码原语（密钥、随机数、时间戳等）
• 带有密码操作的消息交换序列
• 加密、签名和其他安全操作的清晰表示法

数据集结构

数据集提供两种格式：instruction和conversation

instruction格式

json {"text": "<Protocol Name>

<Protocol Specifications>"}

conversation格式

json { "messages": [ {"role": "system", "content": "You are an expert in formal verification of security protocols."}, {"role": "user", "content": "Analyze the following protocol:

<Protocol Name>

<Protocol Specifications>"}, {"role": "assistant", "content": ""} ] }

协议规范表示法

• A, B, S: 主体（参与者）
• Na, Nb: 随机数（随机值）
• Ka, Kb: 密码密钥
• {M}K: 使用密钥K加密的消息M
• A -> B: 从A到B的消息流

使用场景

1. 协议理解: 训练LLM解析和理解安全协议规范
2. 协议分析: 学习识别参与者、消息流和密码操作
3. 安全研究: 理解历史协议及其漏洞
4. 形式化方法: 学习安全协议的形式化表示法

数据来源

• Security Protocols Open REpository (SPORE): http://www.lsv.ens-cachan.fr/spore
• Clark-Jacob Library: https://www.cs.cmu.edu/~iliano/projects/MSR/cjl/index.shtml
• AVISPA Library: https://web.archive.org/web/20160606114053fw_/http://www.avispa-project.org/library/avispa-library.html#IETF
• AVANTSSAR Library: https://web.archive.org/web/20170603130116/http://www.avantssar.eu/

数据处理

原始协议规范经过以下处理：

• 清理格式伪影
• 去除注释和元数据
• 标准化为一致的文本格式
• 按协议名称字母顺序排序
• 转换为JSONL格式便于加载

数据集统计

• 协议总数: 49个来自SPORE + 18个来自Clark-Jacob库 + 16个来自AVISPA库 + 6个来自AVANTSSAR库
• 协议家族: 包含经典协议的变体、修复和修改版本
• 平均长度: 从简单的3消息协议到复杂的多方协议不等
• 语言: 形式化协议规范语言

局限性

• 数据集相对较小（89个协议）
• 协议以特定的形式化表示法表示
• 不包含自然语言描述或安全证明

更新记录

• 2025年10月23日: 数据集现在包含来自Clark-Jacob库、AVISPA库和AVANTSSAR库的额外协议

搜集汇总

数据集介绍

构建方式

在网络安全协议研究领域，该数据集通过整合多个权威来源构建而成，汇集了来自SPORE开放知识库、克拉克-雅各布协议库以及欧盟FP7框架支持的AVISPA与AVANTSSAR验证平台的规范化协议。原始数据经过系统化清洗，剔除格式冗余与注释信息，采用统一文本结构进行标准化处理，并按照协议名称字母顺序重新编排，最终转化为便于机器学习加载的JSONL格式。

特点

该数据集囊括了89个经过形式化验证的安全协议，涵盖从基础三方消息交互到复杂多方协商的协议架构。每个协议采用标准符号系统清晰标注参与主体、密码学原语及消息流序列，例如通过{A->B:{M}K}表示加密消息传输。其独特价值在于完整保留了协议的形式化描述语言，为理解认证机制与密钥交换逻辑提供了结构化模板。

使用方法

研究者可通过HuggingFace数据集库直接加载instruction或conversation两种配置，前者以纯文本格式呈现协议规范，后者采用对话式结构适配指令微调场景。在模型训练环节，开发者可借助SFTTrainer将协议文本映射至模型输入，有效培养语言模型对安全协议形式化语言的解析能力，进而支撑协议漏洞分析、自动化验证等前沿研究。

背景与挑战

背景概述

安全协议开放存储库（SPORE）由法国巴黎-萨克雷高等师范学校的规范与验证实验室（LSV）主导创建，整合了克拉克-雅各布协议库、AVISPA与AVANTSSAR协议库等权威资源。该数据集聚焦于密码学协议的形式化验证领域，旨在通过结构化描述协议参与主体、密码原语及消息交换序列，构建机器可解析的安全协议规范集合。其核心研究问题在于解决传统安全协议分析依赖人工推理的局限性，通过标准化表示方法为自动化验证工具与人工智能模型提供训练基础，对网络安全领域的协议脆弱性检测与形式化方法发展具有重要推动作用。

当前挑战

在密码协议分析领域，该数据集需应对协议语义理解的复杂性挑战，包括加密操作嵌套逻辑的解析、多方会话中时序依赖的建模，以及攻击者模型下安全属性的形式化定义。数据构建过程中，面临多源异构协议库的整合难题，需克服AVISPA等历史库的文档结构差异，统一不同规范中的符号系统与语法约定。此外，小规模数据量与协议形式化表示的专有性，限制了机器学习模型对协议动态行为与未知威胁模式的泛化能力。

常用场景

经典使用场景

在网络安全研究领域，SPORE-Protocols数据集为大型语言模型理解密码协议提供了结构化训练素材。其经典应用体现在模型通过学习标准化的协议规范，掌握参与者声明、密码原语定义及消息交换序列的解析能力。这种训练使模型能够准确识别加密、签名等安全操作，为自动化协议分析奠定基础。

实际应用

实际部署中，该数据集支撑着智能安全审计系统的开发。基于训练的语言模型可辅助工程师快速解析新协议设计，检测潜在的逻辑漏洞。在网络安全教育领域，这些规范化的协议案例成为理解认证机制、密钥交换原理的优质教学资源，显著提升协议分析的效率与准确性。

衍生相关工作

该数据集催生了多项创新研究，如基于神经符号推理的协议验证框架。研究者通过结合传统形式化工具与语言模型的语义理解能力，开发出混合验证系统。这些工作扩展了自动化安全分析的技术边界，为构建下一代智能协议验证平台提供了理论支撑与实践范例。