Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
该论文研究如何让大语言模型（LLM）可靠地参与安全协议的形式化建模。背景是：安全协议（如认证与密钥交换协议）的安全性通常需要借助 Tamarin 这类形式化验证工具来证明，而把自然语言写的协议描述（RFC、规范文档）翻译成可验证的形式化模型
#Tamarin
共收录 7 条相关情报。
← 返回所有主题Understanding the Usability of Cryptographic Verification Tools
该论文针对密码学协议形式化验证工具的实际使用体验开展了一项以人为中心的探索性研究。作者指出，Tamarin、ProVerif 等协议验证工具已被广泛用于分析复杂协议的安全性，但用户如何与这些工具交互、在哪里受阻，长期以来缺乏系统性研究。为此
From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
该论文聚焦于一个长期存在的安全工程问题：即时通信协议的「形式化规范保证」与「实际运行实现行为」之间存在落差。Signal 协议为数以十亿计的用户提供加密通信，是 WhatsApp（全球用户量最大的消息应用）与 Signal 官方客户端的底层
Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution
量子密钥分发（QKD）协议通过量子力学原理提供信息论安全性，但实际部署中QKD本质上是混合协议：其安全结论高度依赖量子阶段与经典后处理阶段的正确集成。虽然ETSI和ITU-T等标准组织已定义了QKD的架构与接口，但现有规范通常在隔离条件下评
A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
这篇论文针对两个主流的协议形式化验证工具 Tamarin 和 ProVerif 提出了首个从 Tamarin 到 ProVerif 的忠实的（sound）翻译方法，以支持系统性的对比分析。Tamarin 基于多集重写规则，验证是可靠且完备的
Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin
该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和