Formal security analysis of registration protocols for interactive systems: a methodology and a case of study
在这项工作中，我们提出并正式分析CHAT-SRP（基于混沌的票证安全注册协议），一个协议，以提供一个强大的密码解决方案，经典的安全问题的交互和协作平台。也就是说，我们专注于保密性和真实性，同时保持高可用性。从这个意义上说，用户被迫盲目信任系统管理员和开发人员。此外，据我们所知，使用形式化方法来验证通信协议的安全属性还不是一个普遍的做法。我们在这里提出了一种方法来填补这一空白，即，分析拟议议定书的安全性和基本前提的相关性。在这个问题上，我们提出了一个协议的定义和正式评估的数字身份的分布。一旦分发，这些身份可用于验证信息的完整性和来源。我们的安全分析基于科学界广泛接受的安全协议的自动验证工具，以及它们所基于的原则。此外，它是假设完美的密码原语，以便集中在协议消息的交换分析。我们的协议的主要属性是合并票，使用基于随机数（仅使用一次的数字）和用户的个人数据的混沌的计数器创建。结合多通道认证方案与一些以前的知识，这些票提供安全性在整个协议中，通过明确地链接每个注册用户与一个单一的请求。[..]
2012-09-06 cs.CR
SLIP-SEC: Formalizing Secure Protocols for Model IP Protection
本文提出SLIP混合推理协议的形式化框架与安全基础，通过权重矩阵加法分解、掩码及概率验证技术构建安全推理协议，证明其对诚实但好奇敌手的信息论安全与对恶意敌手的低误差鲁棒性，为大语言模型知识产权保护提供理论支撑。
2025-10-28 cs.CR
Formal Security Analysis of Agent Protocol Composition
Dartmouth College（达特茅斯学院）；Palo Alto Networks（帕洛阿尔托网络）；Meta；UC Riverside（加州大学河滨分校）
提出AgentThread框架，通过分层安全范围、TLA+形式化检查和两阶段验证器，对智能体协议进行安全分析，发现35个规范级问题及30个组合缺陷，揭示协议间责任缺失。
2026-06-27 cs.CR
Protocol Dialects as Formal Patterns: A Composable Theory of Lingos -- Technical report
本文提出协议方言作为轻量级安全方法，通过Lingo组件使攻击者无法“说”该语言并成为移动目标，并给出多种Lingo转换与组合方法以生成更强Lingo，从而提升协议方言安全性。
2025-04-30 cs.CR
Formal Analysis of an E-Health Protocol
鉴于健康数据的敏感性，电子保健系统的安全和隐私至关重要。至关重要的是，电子保健系统必须确保用户保持隐私-即使他们被贿赂或强迫透露自己或他人的信息：例如，制药公司可能贿赂药剂师透露侵犯医生隐私的信息。在本文中，我们首先确定和正式几个新的，但重要的隐私属性对执行医生的隐私。然后分析了一个复杂而实用的电子健康协议DLV 08的安全性和隐私性。我们的分析揭示了协议中的歧义，并显示在何种程度上这些新的隐私属性以及其他安全属性（如保密性和认证）和隐私属性（如匿名性和不可追溯性）的协议得到满足。最后，我们解决了发现的模糊性，导致安全和隐私缺陷，并提出了修复它们的建议。
2018-08-25 cs.CR
On the security of the Blockchain Bix Protocol and Certificates
BIX协议是一种基于区块链的协议，允许分发将主体与其公钥链接的证书，因此提供类似于PKI的服务，但不需要CA。在本文中，我们分析了BIX协议的安全性在一个正式的方式，在四个步骤。首先，我们确定正式的安全性假设是非常适合这个协议。其次，我们提出了一些针对BIX协议的攻击场景。第三，我们提供了一个正式的安全证明，其中一些攻击是不可行的，根据我们以前建立的假设。最后，我们将展示如何进行另一次攻击。
2016-07-28 cs.CR
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
National University of Singapore（新加坡国立大学）；Beijing Normal-Hong Kong Baptist University（北京师范大学-香港浸会大学联合国际学院）；Griffith University（格里菲斯大学）
本文提出一种人在回路的框架，利用大语言模型生成可审计的协议中间表示，并通过置信度引导的交互界面辅助用户检查关键语义，最终生成Tamarin可验证的安全协议形式化模型。
2026-09-30 cs.CR
Model-Driven Engineering for Formal Verification and Security Testing of Authentication Protocols
即使可以通过形式分析的手段来实现对认证协议的核查，但由于缺乏自动化和一体化的流程，对这种活动进行建模也是一项容易出错的任务。本文提出了一种全面的方法，基于统一建模语言（UML）的分析技术和模型转换，使自动分析的认证协议从高层次的模型。特别地，基于UML的方法能够生成通信协议的带注释的模型，从该通信协议的带注释的模型中，AnBx，Tamarin）。这种模型在较低级别的语言可以分析与现有的求解器和/或与传统的测试技术，通过测试用例生成方法。由于安全需求的不断增长以及将工业流程和设备连接到虚拟化计算基础设施的必要性，该研究的工业影响很大。该研究是在两个案例研究中进行的：铁路信号系统和基于区块链的应用。
2022-10-06 cs.CR
Formal Analysis of V2X Revocation Protocols
对车辆网络（V2X）安全性的研究已经产生了一系列针对该领域的安全机制和协议，解决了安全性和隐私性。通常，对这些建议的安全分析基本上是非正式的。然而，形式化分析可以用来暴露缺陷，并最终在协议中提供更高级别的保证。本文着重于对许多提案中发现的V2X安全机制的特定元素进行形式化分析：通过使其凭据无效来从V2X系统中撤销恶意或行为不端的车辆。即使在车辆定期更改其名称的情况下，也需要以不受干扰的方式执行该撤销，以保护车辆隐私。Forster等人的REWIRE方案及其子方案BASIC和RTOKEN旨在通过密码解决方案和可信硬件来解决这一挑战。使用TAMARIN证明器的形式化分析确定了这些方案中的一些功能正确性和认证属性的两个缺陷。然后，我们提出了模糊令牌（OTOKEN），REWIRE的扩展，使隐私保护的方式撤销。我们的方法通过引入额外的密钥对来解决功能和认证属性，该密钥对提供了更强的和可验证的成功撤销车辆的保证，而无需解决长期身份。OTOKEN是第一个与正式模型共同设计的V2X撤销协议。
2017-08-06 cs.CR
A Theory of Composable Lingos for Protocol Dialects
Universitat Politècnica de València（瓦伦西亚理工大学）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出用形式模式增强协议方言的安全性，通过组合语言提升其防御能力，提供形式化方法保障协议安全。
2026-07-10 cs.CR
Formal Analysis of an Authentication Protocol Against External Cloud-Based Denial-of-Service (DoS) Attack
拒绝服务（DoS）攻击被认为是云计算服务可用性的最大威胁之一。由于云计算系统独特的架构，其检测和防范拒绝服务攻击的方法与传统网络系统有很大的不同。DoS攻击者的主要目标是身份验证协议，因为它被认为是访问云资源的网关。在这项工作中，我们提出了一个基于云的身份验证协议-一个安全地验证云用户，并有效地防止拒绝服务攻击的云计算系统-通过涉及用户在一个高的计算过程。然后，我们分析了协议通过Syverson和Van Oorschot（SVO）逻辑验证协议的认证过程中的云计算系统。
2017-11-22 cs.CR
Formal Security Analysis on dBFT Protocol of NEO
NEO是全球顶级公共链之一。我们专注于其骨干共识协议，称为委托拜占庭容错（dBFT）。dBFT协议已被各种区块链系统（如ONT）采用。dBFT声称当不超过$f = \lfloor \frac{n}{3} \rfloor$节点是拜占庭时保证安全性，其中$n$是共识参与者的总数。然而，我们识别攻击来打破声称的安全性。在本文中，我们展示了我们的结果，提供了一个安全性分析其dBFT协议。首先，我们评估了NEO的源代码，并通过状态机复制（SMR）模型正式提出了dBFT的过程。接下来，我们提供了两个示例攻击的理论分析。这些攻击破坏了不超过$f$节点的dBFT的安全性。然后，我们就如何针对已识别的攻击修复系统提供建议。建议的修复已被近地天体官方团队接受。最后，我们进一步讨论了导致这些问题的原因，与当前许可的区块链系统的关系以及潜在影响的范围。
2022-06-19 cs.CR
ModelForge: Using GenAI to Improve the Development of Security Protocols
本文提出 ModelForge，利用 NLP 与 GenAI 并微调 LLM，将自然语言安全协议规范自动转换为 CPSA 形式化定义，实验表明其输出质量稳定且语法准确性突出。
2025-06-08 cs.CR
Anumati: Proof of Adherence as a Formal Consent Model for Autonomous Agent Protocols
Independent Researcher（独立研究者）
本文提出一种形式化同意模型，用于自主代理协议中的合规性证明，通过三个原始构件实现版本化、只追加的同意模型，并将其扩展到两种常用代理协议中。
2026-04-16 cs.CR
Formal Methods Analysis of the Secure Remote Password Protocol
我们分析了安全远程密码（SRP）协议的结构弱点，使用密码协议分析器（CPSA）在SRP的第一次正式分析（特别是，版本3）。SRP是一种广泛部署的密码验证密钥交换（PAKE）协议，用于1Password，iCloud钥匙串和其他产品。与许多PAKE协议一样，两个参与者使用预先共享的密码来相互验证并建立会话密钥。SRP旨在抵抗字典式攻击，不在服务器上存储明文等效密码，避免专利侵权，并通过不使用加密来避免出口控制。SRP的形式化分析是具有挑战性的，部分原因是现有的工具没有提供简单的方法来推理其使用的数学表达式$v + g^b \mod q$。建模$v + g^b$加密，我们完成了详尽的研究所有可能的执行序列的SRP。忽略可能的代数攻击，这种分析没有发现重大的结构性弱点，特别是没有泄漏任何秘密。我们发现一个显着的弱点，SRP，这是从它的设计约束。恶意服务器可以在没有客户端参与的情况下伪造与客户端的身份验证会话。如果客户端的权限高于服务器，则此操作可能会导致权限攻击升级。我们在使用CPSA之前就设想了这种攻击，并通过使用CPSA生成相应的执行形状来确认它。
2020-03-16 cs.CR
A Formal Security Analysis of the pEp Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email
为了发送加密的电子邮件，用户通常需要创建和交换密钥，这些密钥随后应该通过手动验证，例如，通过比较长字符串。这些任务对于普通用户来说是繁琐的。为了更方便地使用加密电子邮件，一个名为pEp的安全电子邮件应用程序自动化了密钥管理操作; pEp仍然需要用户进行验证，但是，认证过程很简单：用户必须比较熟悉的单词而不是随机字符串，然后应用程序通过彩色视觉指示器向用户显示他们已经达到的信任级别。然而，用户可能不会按照预期执行认证仪式，pEp的信任评级可能被错误地分配，或者两者兼而有之。要了解是否pEp的信任评级（和相应的视觉指标）的分配一致，我们提出了一个正式的安全分析pEp的认证仪式。从C语言的软件实现，我们得出的规范的一个抽象的协议，公钥分布，加密和信任的建立，然后，我们模型的协议中的一个变种的应用π演算，后来正式验证和验证特定的隐私和认证属性。我们还讨论了其他研究方向，可以丰富分析。
2020-08-29 cs.CR
Formal Verification of the Sumcheck Protocol
本文使用 Isabelle/HOL 对 sumcheck 协议进行形式化验证，通过模块化方法建立其可靠性和完备性，并证明公理适用于多元多项式，为基于该协议的密码系统提供安全性保障。
2024-02-08 cs.CR cs.LO
Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond
本研究提出形式化引导的模糊测试方法，结合形式化验证与模糊测试的优势，分层检测5G协议到软件栈的漏洞，在srsRAN平台发现61个漏洞，将计算成本从指数增长降为线性增长。
2023-07-20 cs.CR
Formal Modelling and Security Analysis of Bitcoin's Payment Protocol
针对比特币支付协议标准BIP70因缺乏退款地址认证易受退款攻击的问题，首次构建其形式化模型并定义退款地址安全目标，分析验证原协议漏洞后提出带公开可验证证据的修订方案，证明修订后协议满足安全目标。
2021-03-15 cs.CR cs.FL
Formal and Fuzzing Amplification: Targeting Vulnerability Detection in 5G and Beyond
本文提出融合形式化验证与模糊测试的分层框架，通过双向反馈在5G NSA的RRC流程中建立1个攻击模型并发现53个漏洞，提升大规模网络漏洞检测的可扩展性。
2023-07-11 cs.CR
AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation
Sectra Communications（赛特拉通信）；Linköping University（林雪平大学）
提出一种语言优先方法，通过领域特定语言实现协议并自动生成 Tamarin 模型，验证迹属性并保证其传递到实现，同时集成符号执行分析内存安全，在签名 Diffie-Hellman 和 WireGuard 协议上验证了安全性和互操作性。
2026-06-19 cs.CR
Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard -- the POST/Artifact use case
University of Zagreb（萨格勒布大学）
本文通过Tamarin证明器对SAML V2.0 SP发起的SSO与POST/Artifact绑定用例进行了全面的形式安全分析，验证了多个关键安全属性并识别了潜在漏洞。
2026-01-20 cs.CR
Segment-Based Formal Verification of WiFi Fragmentation and Power Save Mode
针对WiFi功能层面缺乏形式化验证方法且存在严重漏洞，本文提出基于分段的形式化验证流程，结合Tamarin中的MAC欺骗威胁模型，分析WiFi分片与省电模式，发现多个漏洞并验证应对措施的有效性。
2023-12-16 cs.CR
STRIATUM-CTF: A Protocol-Driven Agentic Framework for Autonomous CTF Solving
Department of Computer Science, Florida State University, Tallahassee, USA（计算机科学系，佛罗里达州立大学，塔拉萨斯，美国）
本文提出STRIATUM-CTF框架，通过Model Context Protocol标准化工具接口，提升CTF求解的自主性和适应性，在真实竞赛中取得第一名。
2026-11-02 cs.AI cs.CR cs.MA
An Analysis of the CAVES Attestation Protocol using CPSA
本文介绍了CAVES认证协议，并提出了一个工具支持的分析表明，该协议的运行达到了既定的目标。通过使用可靠保证方法用逻辑公式注释协议，形式化地陈述了目标。使用的协议分析工具是加密协议形状分析器。
2012-07-02 cs.CR
A Trace Logic for Local Security Properties
我们提出了一个新的简单的\emph{trace}逻辑，可用于指定\emph{local security properties}，即安全属性，指的是一个单一的参与者的协议规范。我们的技术允许协议设计者提供所需的安全属性的正式规范，并将其自然地集成到密码协议的设计过程中。此外，该逻辑还可用于形式化验证。我们说明了我们的技术的效用，通过暴露新的攻击研究协议TMN。
2004-11-30 cs.CR
Security Analysis of the Open Banking Account and Transaction API Protocol
本文利用AnBx形式化建模及OFMC和Proverif工具，结合NatWest沙箱实际测试，对英国开放银行账户与交易API协议进行了无限会话的安全性分析与验证。
2025-05-03 cs.CR
Formal Verification of Permission Voucher
本文使用 Tamarin Prover 对分布式环境下的 Permission Voucher Protocol 进行形式化验证，确认其在认证、机密性等方面的鲁棒性，并提出应对内部威胁及系统扩展性的改进策略。
2024-12-18 cs.CR
Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Channel Binding
本文通过形式化方法分析 FIDO UAF 信道绑定，发现其无法阻止攻击者转移认证挑战并实施中间人攻击，进而提出并验证改进方案，强调密码学绑定上下文的必要性。
2025-11-08 cs.CR
A Formal Analysis of 5G Authentication
移动通信网络连接着世界上大部分人口。用户通话、SMS和移动数据的安全性取决于所使用的认证密钥交换协议提供的保证。对于下一代网络（5G），3GPP组已经为此目的标准化了5G AKA协议。我们提供了AKA系列协议的第一个全面的正式模型：5G AKA。我们还从定义5G的3GPP标准中提取了精确的要求，并确定了缺失的安全目标。使用安全协议验证工具Tamarin，我们针对5G安全目标对模型进行了全面、系统的安全评估。我们的自动分析确定了每个安全目标所需的最低安全假设，我们发现，除了标准中缺少的其他假设之外，一些关键的安全目标没有得到满足。最后，我们针对我们发现的攻击和弱点提出了明确的建议，并提供了可证明安全的修复方案。
2020-01-10 cs.CR
Automated Cryptographic Analysis of the Pedersen Commitment Scheme
为了更好地保证密码系统的安全性，密码结构的形式化验证受到了越来越多的关注。对流行的Pedersen承诺协议进行了一种机械化的形式化验证，证明了其正确性、完全隐藏和计算绑定等安全性质.为了正式验证协议，我们扩展了EasyCrypt理论，EasyCrypt是一个允许在计算模型中进行推理的框架，它支持离散对数和承诺协议的抽象。承诺是许多加密构造的构建块，例如，可验证的秘密共享、零知识证明和电子投票。我们的工作为验证这些更复杂的结构铺平了道路。
2017-05-16 cs.CR
A Formal Analysis of the MimbleWimble Cryptocurrency Protocol
MimbleWimble（MW）是一种面向隐私的加密货币技术，它提供了与其他同类协议不同的安全性和可扩展性。我们提出并讨论了这些属性，并概述了模型驱动的验证方法，以解决协议实现的正确性认证的基础。特别是，我们提出了一个理想化的模型，这是在所描述的验证过程中的关键，并确定和精确状态的充分条件，我们的模型，以确保验证相关的安全属性的MW。由于MW是建立在共识协议之上的，我们开发了一个这样的协议的Z规范，并从Z规范生成的$\{log\}$原型的摘录。该$\{log\}$原型可用作可运行模拟的可执行模型。这使我们能够分析协议的行为，而不必在低级程序设计语言中实现它。最后，我们分析了MW的Grin和Beam实现的当前发展状况。
2021-04-02 cs.CR cs.SE
Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation
Indian Institute of Technology Jodhpur（印度技术学院焦特普尔分校）；Ohio State University（俄亥俄州立大学）
本文形式化研究无线通信中基于配对的隐私攻击的根本原因，通过对Wi-Fi P2P和蓝牙低功耗的建模提出解决方案，获相关组织认可，为隐私保护无线协议发展铺路。
2026-08-13 cs.CR cs.NI
CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection
University of Udine（乌迪内大学）；University of Trieste（的里雅斯特大学）；AAU Klagenfurt（克拉根福应用技术大学）；Apart Research（阿帕特研究院）
本文提出CryptoFormalEval基准，通过让大语言模型与定理证明器Tamarin交互，自动发现新密码协议漏洞，并验证了前沿模型在网络安全应用中的潜力。
2024-11-20 cs.AI cs.CR cs.SC
Data Minimisation in Communication Protocols: A Formal Analysis Framework and Application to Identity Management
随着互联网上交换的个人信息越来越多，隐私越来越成为用户关注的问题。保护隐私的关键原则之一是数据最小化。这一原则要求只收集和处理实现某个目标所需的最小量的信息。已经提出了“隐私增强”通信协议，以保证在广泛的应用中的数据最小化。然而，目前还没有令人满意的方法来评估和比较它们提供的隐私，以一种精确的方式：现有的分析要么太不正式和高层次，或特定于一个特定的系统。在这项工作中，我们提出了一个一般的正式框架来分析和比较通信协议的隐私数据最小化。隐私要求是正式独立于一个特定的协议在知识（联盟）的演员在一个三层模型的个人信息。然后，通过从它们的通信描述计算该知识，针对特定协议自动验证这些要求。我们验证我们的框架中的身份管理（IdM）的案例研究。随着IdM系统被越来越多地用于满足对可靠的在线身份识别和认证的日益增长的需求，隐私正成为一个越来越关键的问题。我们使用我们的框架来分析和比较四个身份管理系统。最后，我们讨论的完整性和（可再）可用性的建议框架。
2014-01-13 cs.CR cs.NI
A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols
Teesside University（蒂斯赛德大学）
针对从业者难以常规使用形式化方法的问题，提出核心包含AnB符号系统等组件的Eclipse IDE，经评估可辅助用户掌握网络安全概念，是项目完成的重要组件且获用户复用认可。
2024-11-26 cs.CR cs.SE
A Symbolic Logic with Concrete Bounds for Cryptographic Protocols
本文提出了一种形式逻辑，用于网络协议安全性的定量推理。该系统允许我们导出具体的安全界限，可用于选择密钥长度和其他安全参数。我们提供公理推理数字签名和随机数，安全性的基础上的具体安全的签名方案和伪随机数发生器（PRG）。形式逻辑支持一阶推理和协议不变量推理，并考虑了具体的安全边界。在我们的逻辑中构造的证明也提供了传统的渐近安全保证，因为具体的界限在证明中积累的方式。作为一个说明性的例子，我们使用形式逻辑证明了一个基于签名的挑战-响应协议的认证性质与具体的界限。
2015-11-24 cs.CR cs.LO
Secure Neighbor Discovery in Wireless Networks: Formal Investigation of Possibility
无线通信使从商品到战术系统的广泛应用成为可能。邻居发现（ND），即确定哪些设备处于直接无线电通信内，是网络协议和应用的构建块，并且其脆弱性可能严重损害它们的功能。已经公布了一些确保ND安全的建议，但没有一个正式分析过这个问题。在本文中，我们贡献这样一个分析：我们建立了一个正式的模型捕捉无线系统的显着特点，最显着的障碍和干扰，我们提供了一个规范的ND问题的基本变体。然后，我们推导出一个不可能的结果，一般类的协议，我们称之为“基于时间的协议”，其中许多计划在文献中属于。我们还确定了不可能结果被解除的条件。此外，我们探讨了第二类协议，我们称之为“基于时间和位置的协议”，并证明他们可以安全ND。
2008-08-19 cs.CR cs.NI
Formal Model Guided Conformance Testing for Blockchains
针对多客户端区块链协议实现语义不匹配易引发分裂与攻击、现有临时测试一致性保障不足的问题，提出结合协议形式化模型与确定性模拟器中实现的双互补工作流一致性测试框架，可检测所有违规类型，已在工业级共识协议上验证实用性。
2025-01-18 cs.CR cs.LO cs.SE
Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)
本文针对结合物理层安全技术的Needham-Schroeder协议，提出基于Isabelle的通用可配置形式化验证框架，通过全面分析保密性与真实性，并设计安全的PLS-Diffie-Hellman协议，克服了ProVerif方法的局限。
2025-08-28 cs.CR cs.FL cs.LO
A Formal Analysis of Agent Payment Protocols
Southern University of Science and Technology（南方科技大学）；Indian Institute of Technology（印度理工学院）；City University of Hong Kong（香港城市大学）
该研究在Tamarin中对x402等四种智能体支付协议进行形式化分析，复现46个验证案例并发现40个新一致性问题，提出18项安全原则，验证了委托授权需与经济服务效果一致的结论。
2026-09-02 cs.AI cs.CR
Formal Black-Box Analysis of Routing Protocol Implementations
Internet基础设施完全依赖于其路由协议的开放标准。然而，互联网上的大多数路由器都是闭源的。因此，没有直接的方法来分析它们。具体来说，人们不能轻易地识别路由器的路由功能与路由协议标准的偏差。这种偏差（无论是故意的还是无意的）的识别是特别重要的，因为它们可能会降低网络的安全性或弹性。基于模型的测试过程是一种允许基于待测试系统的模型系统地生成测试的技术;从而发现系统中与模型相比的偏差。然而，将这种方法应用于复杂的多方路由协议需要大量的测试来覆盖所需的功能。我们提出了有效的和实用的优化基于模型的测试过程中，量身定制的路由协议的分析。这些优化允许设计一个正式的黑盒方法来挖掘闭源路由协议实现中的偏差。该方法仅依赖于测试目标协议实现并观察其输出的能力。偏差的识别是全自动的。我们评估我们的方法对一个复杂的和广泛使用的路由协议在互联网上-OSPF。我们寻找思科OSPF实施中的偏差。我们的评估发现了许多可能被滥用以损害网络安全的重大偏差。思科确认了这些偏差。我们进一步采用我们的方法来分析Quagga路由套件的OSPF实现。分析发现了一个重大偏差。在披露偏差后，IBM、联想和华为也在自己的产品中发现了其中一些偏差。
2017-09-23 cs.CR cs.NI
How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET
移动自组织网络的安全路由协议是近年来发展起来的，然而，由于缺乏对这些协议的形式化分析，它们所具有的特性还不清楚。在本文中，我们关注这个问题，如何指定和如何证明一个安全的路由协议的正确性。我们提供了一个定义，什么是一个协议预计将实现独立的功能，以及通信和对手的模型。通过这种方式，我们可以对安全路由协议的正确性进行形式化推理。我们证明了这一点，从文献中分析两个协议。
2009-12-30 cs.CR cs.NI
Protocols to Code: Formal Verification of a Next-Generation Internet Router
本文针对 SCION 互联网路由器，结合 Isabelle/HOL 协议精化验证与 Go 代码自动化验证，首次实现从安全协议模型到生产实现的端到端形式化保证。
2024-05-09 cs.CR cs.NI cs.PL
Automated Attacker Synthesis for Distributed Protocols
分布式协议应该对良性故障（例如数据包丢失或延迟）和来自内部或外部对手的攻击（例如消息重放）都具有鲁棒性。在本文中，我们采取了一种形式化的方法来自动合成攻击者，即可能导致协议故障的对抗过程。具体来说，给定一个正式的威胁模型捕获分布式协议模型和网络拓扑结构，以及潜在攻击者的位置，目标和接口（输入和输出），我们自动合成攻击者。我们正式四个攻击者的合成问题-攻击者总是成功与那些有时失败，攻击者永远攻击与那些不-我们提出了算法解决方案，其中两个。我们报告的原型实现称为KORG和它的应用程序TCP作为一个案例研究。我们的实验表明，KORG可以在几秒钟或几分钟内自动生成已知的TCP攻击。
2022-04-12 cs.CR cs.FL
A Security Verification Framework of Cryptographic Protocols Using Machine Learning
NTT Computer & Data Science Laboratories（NTT计算机与数据科学实验室）；NTT Social Informatics Laboratories（NTT社会信息学实验室）
针对密码协议形式化验证耗时长、无判定性保证的问题，提出基于机器学习的安全验证框架，通过自动生成带标签数据集和适配协议结构的神经网络，实现线性时间复杂度的验证。
2023-04-26 cs.CR cs.LG
Safe Low Bandwidth SPV: A Formal Treatment of Simplified Payment Verification Protocols and Security Bounds
University of Exeter Business School（埃克塞特大学商学院）
本文从第一性原理形式化重建比特币SPV协议，证明其在有界对抗假设下安全且最优，并引入低带宽优化，为安全实现提供蓝图并反驳对非验证客户端的误解。
2025-07-01 cs.CL cs.CR cs.DC
Symbolic Abstractions for Quantum Protocol Verification
量子协议，如BB84量子密钥分配协议，交换量子比特以实现信息理论安全保证。提出了许多不同的方案，其中一些已经得到实施。该领域现有的安全性证明大多是繁琐的，容易出错的纸笔证明的核心协议，很少考虑其他关键组件，如身份验证。这就需要正式的自动化验证技术，彻底探索所有可能的入侵者行为，并具有很好的可扩展性。符号方法提供了严格的数学框架和自动化工具来分析安全协议。基于精心设计的抽象，它允许对TLS 1.3和移动电话协议等现实协议进行大规模的形式化分析。因此，一个自然的问题是：我们能否利用这一成功的工作来分析量子协议？本文提出了第一个肯定的答案，并激励进一步研究这一未探索的道路。
2019-04-10 cs.CR quant-ph
Verification and Attack Synthesis for Network Protocols
本论文表明形式化方法能切实刻画网络协议在正常条件及遭受攻击时的功能与性能，解决协议因缺陷、故障或攻击无法满足要求的问题。
2025-11-03 cs.CR cs.FL
From Automata Learning to Model Checking: Formal Security Verification of Black-Box Protocols
Mälardalen University（马尔默达尔大学）；AVL List GmbH（AVL李斯特有限公司）；AIT Austrian Institute of Technology GmbH（奥地利技术研究所有限公司）；KTH Royal Institute of Technology（皇家理工学院）
本文提出结合自动机学习与模型检查的方法，用于系统验证通信协议的安全属性，通过自动化流程减少建模工作量并提高安全性验证的自动化水平。
2026-09-14 cs.CR cs.FL
A Secure Consensus Protocol for Sidechains
侧链技术被认为是一种有前途的解决方案，可以在可扩展性和互操作性方面加速当今的公共区块链。通过依靠主链的安全性，不同的侧链可以制定自己的规则来达成共识。虽然文献已经考虑了在侧链中使用共识协议的可能性，但到目前为止，还没有尝试为侧链定制具有高性能和形式安全性证明的共识协议。为了填补这一空白，我们介绍了Cumulus，一个低开销，高效，安全可证明的侧链协议。Cumulus利用智能合约来确保每轮只有一个在侧链中提出的区块会在主链上执行，从而以有效的方式达成共识。给出了Cumulus的形式化规范，保证了Cumulus的安全性和活跃性，而无需客户端的任何在线要求。在安全性分析方面，给出了通用可组合安全模型下的形式化安全定义和证明。作为概念证明，我们实现了Cumulus并在以太坊测试网中对其进行了评估。
2019-11-16 cs.CR cs.DC
Formal Barriers to Longest-Chain Proof-of-Stake Protocols
大多数现有加密货币的安全性是基于一个名为工作量证明的概念，在这个概念中，用户必须解决一个计算困难的加密难题来授权交易（“一个计算单位，一票”）。这导致在硬件和电力上的巨大支出，以便收集与交易授权相关的奖励。权益证明是一种替代概念，它选择用户授权与其财富成比例的交易（“一枚硬币，一票”）。这两种范式的某些方面是相同的。例如，在权益证明中获得投票权就像在工作量证明中一样有货币成本：一个硬币不能像一个计算单位那样容易被复制。然而，有些方面是根本不同的。特别是，正是因为权益证明是无浪费的，偏离不存在固有的资源成本（通常称为“无利害关系”问题）。与之前的工作相比，我们专注于激励驱动的偏离（如果这样做可以产生更高的收入，任何参与者都会偏离），而不是对抗性腐败（对手可能会接管网络的很大一部分，但其余的参与者会遵守协议）。本文的主要结果是设计激励兼容的权益证明加密货币（不适用于工作量证明）的几个正式障碍。
2018-09-18 cs.CR cs.GT
Building Secure and Anonymous Communication Channel: Formal Model and its Prototype Implementation
需要结合各种技术来实现匿名认证通信。加密工具支持匿名用户身份验证，而匿名通信协议则对服务提供商隐藏用户的IP地址。实现匿名认证通信的一种简单方法是它们的简单组合，但这引起了另一个问题;如何建立安全信道。由于用户的公钥标识了用户，因此无法使用当前的公钥基础设施。为了解决这个问题，我们提出了一个协议，使用基于身份的加密数据包加密，而不牺牲匿名性，和匿名用户认证的群签名。协议中的通信通过代理实体进行，代理实体对服务提供商隐藏用户的IP地址。底层的群签名是定制的，以满足我们的目标，并提高其效率。我们还介绍了一个概念验证的实现，以证明该协议的可行性。通过与SSL通信的性能比较，证明了该协议的实用性，并得出结论：该协议实现了用户与服务提供者之间的安全、匿名、认证的通信，具有实用性。
2014-05-08 cs.CR cs.NI
RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers
过去在协议实现的消息解析器中发现了各种漏洞。甚至像TLS库这样高度敏感的软件组件也会定期受到影响。由此产生的问题包括从拒绝服务攻击到提取敏感信息。协议的复杂性和自然语言中不精确的规范是实现中出现细微bug的核心原因，这些bug很难被发现。缺乏精确的规格妨碍了形式化验证。在本文中，我们提出了一个模型和相应的特定领域的语言来正式指定现有的现实世界中的二进制协议的消息格式。该模型的一个独特功能是定义不变量的能力，这些不变量指定消息字段之间的关系和依赖关系。此外，该模型允许定义不同协议层之间的消息关系，从而确保有效载荷数据的正确解释。我们提出了一种技术，以获得可验证的分析器的模型的基础上，生成有效的代码，其实现，并自动证明不存在运行时错误。以太网和TLS的解析器规范的例子证明了我们的方法的适用性。
2019-10-02 cs.CR cs.NI cs.PL
