Combining Blockchain and IOT for Decentralized Healthcare Data Management
针对物联网医疗数据云存储的隐私与安全漏洞问题，提出一种专为电子健康设计的区块链协议，采用适合资源受限设备的共识机制与隐私保护访问控制，实现去中心化、安全高效的患者数据管理与防泄露。
2023-03-31 cs.CR
Formal Computational Unlinkability Proofs of RFID Protocols
在计算模型中建立了RFID协议形式化证明的框架。我们依赖于所谓的计算上完全的符号攻击者模型。我们的贡献是：i）设计（并证明合理的）反映散列函数（抗碰撞性，PRF）属性的公理; ii）形式化模型中的计算不可链接性; iii）说明该方法，在计算模型中提供RFID协议不可链接性的第一个形式证明。
2017-05-05 cs.CR
Approaches to Formal Verification of Security Protocols
近年来，已经提出了许多协议来为各种信息和通信系统提供安全性。这些协议在实际使用之前必须测试其功能的正确性。应用形式化方法验证安全协议将提高其可靠性，从而增加使用它们的系统的可用性。因此，安全协议的形式化验证已成为计算机和通信安全领域的一个关键问题。在本文中，我们提出，分析和比较一些流行的方法对安全系统的验证。我们遵循的概念-相同的目标，通过不同的方法-我们正式分析了李约瑟施罗德公钥协议的Lowe的攻击，使用我们提出的每一种方法。
2011-01-10 cs.CR
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol
MimbleWimble是一种面向隐私的加密货币技术，包含安全性和可扩展性，使其与其他同类协议区分开来。在本文中，我们提出并简要讨论了这些属性，并概述了模型驱动的验证方法的基础上，以解决一个特定的协议实现的正确性的认证。
2019-07-03 cs.CR
Privacy-Preserving Mutual Authentication and Key Agreement Scheme for Multi-Server Healthcare System
不同技术和智能设备的使用有助于人们远程获得医疗服务，从而获得多种好处。因此，关键和敏感数据在用户和医生之间交换。当健康数据通过公共信道传输时，保护系统中的各种隐私和安全属性变得至关重要。此外，远程服务的用户数量每天呈指数级增长，因此，由于验证开销、服务器故障和可扩展性问题，使用一个服务器来处理所有用户是不够的。因此，研究者们提出了各种多服务器架构的认证协议，但大多数协议都容易受到不同的安全攻击，并且在实现过程中需要很高的计算资源。为了解决隐私和安全问题，使用较少的计算资源，我们提出了一个隐私保护的相互认证和密钥协商协议的多服务器医疗保健系统。我们讨论了所提出的方案的安全性分析和性能结果，以了解其安全优势和计算资源的要求，分别。此外，我们做的安全性和性能的结果与最近的相关认证协议的比较。
2021-10-13 cs.CR
Formal Support for Standardizing Protocols with State
许多加密协议被设计为仅使用通过开放网络传递的消息来实现其目标。有许多工具都是基于众所周知的基础，用于设计和分析纯粹依赖于消息传递的协议。然而，这些工具遇到的困难时，面对依赖于非本地，可变状态来协调几个本地会话的协议。我们采用这些工具之一，{ \cpsa }，以提供自动化的支持推理状态。我们使用瑞安的信封协议作为一个例子来演示如何消息传递推理可以与状态推理相结合，产生有趣的和强大的结果。关键词：协议分析工具，有状态协议，TPM，PKCS#11。
2015-09-24 cs.CR
A Privacy Preserving Improvement for SRTA in Telecare Systems
射频识别（RFID）是一种通过非物理接触提供身份认证和识别的现代通信技术。最近，这项技术的使用几乎在医疗保健环境中得到了发展。虽然RFID技术可以在系统中准备智能，但隐私和安全问题应该在此之前考虑。最近，在2015年，Li等人提出了SRTA，这是一种基于哈希的RFID认证协议，用于医疗保健的药物验证。在本文中，我们研究了该协议，并表明SRTA协议是脆弱的可追溯性，假冒和Dos攻击。因此，它不提供RFID最终用户的隐私和安全。因此，我们提出了一种改进的安全和高效的RFID认证协议，以提高李等人的方法的性能。分析表明，该协议克服了SRTA协议存在的不足。
2015-10-14 cs.CR
Formal Analysis of Composable DeFi Protocols
去中心化金融（DeFi）已经成为区块链和智能合约最成功的应用之一。DeFi生态系统支持广泛的加密金融活动，而底层的智能合约通常包含漏洞，其中许多漏洞来自于将DeFi协议组合在一起的不可预见的后果。在本文中，我们提出了一个正式的过程代数技术，模型DeFi协议的组合方式，允许有效的属性验证。我们还进行了一个案例研究，以证明所提出的方法在分析两个相互作用的DeFi协议，即曲线和化合物的组成。最后，我们讨论了如何提出的建模和验证方法可以用来分析金融和安全属性的利益。
2021-04-19 cs.CR
SecGoal: A Benchmark for Extracting Formalizable Security Goals from Protocol Documents
Beijing University of Posts and Telecommunications（北京邮电大学）
提出SecGoal基准和AIFG框架，通过微调小型开源LLM实现从协议文档中高精度提取可形式化安全目标，并生成结构化安全属性。
2026-05-28 cs.CR
A formal methodology for integral security design and verification of network protocols
提出了一种在设计级验证网络协议安全性的方法。它可以分为两个主要部分：上下文和需求分析和非正式验证;以及正式表示和过程验证。这是一个迭代的过程，早期的步骤比最后的步骤简单。因此，检测缺陷所需的工作量与相关攻击的复杂性成正比。因此，我们避免了浪费宝贵的资源，用于可以在验证过程的早期检测到的简单缺陷。为了说明我们的方法所提供的优势，我们还分析了三个真正的协议。
2012-09-06 cs.CR
An Algebraic Characterization of Security of Cryptographic Protocols
几个基本的密码构造都有相关的代数结构。Dolev和Yao提出的研究公钥协议（无条件）安全性的形式化模型形成了一个群体。某些类型的协议的安全性可以在这个代数设置中巧妙地公式化。我们研究两方协议的类别。然后，我们考虑扩展的形式代数框架的私钥协议。并讨论了形式化模型的具体实现。在这种情况下，我们提出了一个定义的伪自由群。
2008-02-22 cs.CR
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
MPC-in-the-Head（MitH）是一个通用的框架，它允许从安全多方计算（MPC）协议构造有效的一般NP关系的零知识协议。在本文中，我们给出了这种转换的第一个机器检查的实现。我们从MitH的EasyCrypt形式化开始，它保留了MitH的模块化结构，并且可以用满足标准安全概念的任意MPC协议来实例化，这使我们能够利用现有的基于机器检查的秘密共享的MPC协议开发。在EasyCrypt中证明了ZK协议的安全性和正确性。使用最近开发的代码提取机制EasyCrypt，我们合成了一个正式验证的协议的实现，我们基准测试，以获得与我们的形式化选择和代码提取机制相关的开销的指示。
2021-05-19 cs.CR
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
Canada Protocol: an ethical checklist for the use of Artificial Intelligence in Suicide Prevention and Mental Health
Université du Québec à Montréal（魁北克大学蒙特利尔分校）；Montreal AI Ethics Institute（蒙特利尔人工智能伦理研究所）；Microsoft（微软）
简介：为了改善当前自杀预防和心理健康方面的公共卫生战略，政府、研究人员和私营公司越来越多地使用信息和通信技术，更具体地说，是人工智能和大数据。这些技术很有前途，但提出了目前法律制度很少涵盖的道德挑战。必须更好地识别和预防潜在的道德风险。目的：MHSP是一个工具，用于指导和支持专业人员，用户和研究人员在心理健康和自杀预防中使用AI。方法：根据十份关于人工智能和伦理学的国际报告以及两份关于心理健康和新技术的指南构建了一份清单。确定了329项建议，其中43项被认为适用于精神健康和人工智能。通过两轮德尔菲咨询，对该检查表进行了验证。结果：16名专家参加了第一轮专家咨询，8名专家参加了第二轮专家咨询。在原有的43项中，保留了38项。它们涉及五个类别：“自主智能系统的描述”（n=8），“隐私和透明度”（n=8），“安全性”（n=6），“健康相关风险”（n=8），“偏见”（n=8）。大多数用户认为该清单是相关的，可能需要针对每一类目标用户量身定制版本。
2019-07-17 cs.AI cs.CR cs.CY
Formal Verification of Access Control Model for My Health Record System
我的健康记录系统是澳大利亚政府的数字健康记录系统，保存我的健康记录。我的健康记录是一个安全的在线健康记录，包含消费者的健康信息。该系统旨在为保健专业人员提供关键的健康信息，例如列出药物、过敏和关键诊断;放射学和病理学测试结果。该系统（以前称为个人控制电子健康记录）使消费者能够决定如何与任何注册并连接到该系统的医疗保健提供者共享信息。我的健康记录系统在澳大利亚2012年《我的健康记录法》的立法框架下运作。该法除其他外，建立了一个隐私框架，具体规定哪些实体可以收集、使用和披露系统中的某些信息，以及对不当收集、使用和披露此类信息可施加的处罚。本文介绍了正式规范（从立法）和验证的我的健康记录关于消费者如何可以控制谁访问的信息，以及系统如何坚持这样的访问。我们依赖于正确的建设事件B的方法来证明系统的控制和访问属性。
2020-06-12 cs.CR cs.SE
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
One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)
本文提出可用于Tamarin和ProVerif的通用及BLS聚合签名形式化模型，并通过分析SANA设备证明协议发现其隐含假设缺失会导致攻击。
2025-05-15 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
Enhancing Data Privacy In Wireless Sensor Networks: Investigating Techniques And Protocols To Protect Privacy Of Data Transmitted Over Wireless Sensor Networks In Critical Applications Of Healthcare And National Security
本文研究医疗与国家安全关键应用中WSNs的数据隐私保护，梳理相关技术、挑战与影响因素，引入创新扩散理论分析隐私技术采纳，并结合实证研究验证安全方案有效性。
2024-04-17 cs.CR cs.NI
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
Using Blockchain to Achieve Decentralized Privacy In IoT Healthcare
本文提出一种适用于物联网电子医疗的区块链协议，无需信任第三方，采用适配资源受限设备的共识机制以提供隐私保护访问控制，并提升安全性与效率。
2021-09-30 cs.CR
Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond
本研究提出形式化引导的模糊测试方法，结合形式化验证与模糊测试的优势，分层检测5G协议到软件栈的漏洞，在srsRAN平台发现61个漏洞，将计算成本从指数增长降为线性增长。
2023-07-20 cs.CR
Formal Verification of the Sumcheck Protocol
本文使用 Isabelle/HOL 对 sumcheck 协议进行形式化验证，通过模块化方法建立其可靠性和完备性，并证明公理适用于多元多项式，为基于该协议的密码系统提供安全性保障。
2024-02-08 cs.CR cs.LO
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
A Holistic Approach to Enhanced Security and Privacy in Digital Health Passports
随着世界各国政府决定部署数字健康护照作为遏制新冠肺炎传播的工具，考虑如何通过设计来构建这些护照变得越来越重要。在本文中，我们讨论了构建数字健康护照的常见方法的隐私和安全问题。然后，我们将展示如何以简单有效的方式构建和部署安全和私密的数字健康护照。我们通过使用基于密码的分布式令牌发行协议、秘密共享以及利用现代智能手机的安全硬件来实现这一点。我们的解决方案只需要恒定数量的非对称加密操作和用户与验证用户数字健康护照的一方之间的单轮通信，并且用户与签发数字健康护照的服务器之间只需要两轮通信。
2021-06-09 cs.CR
PACT: Privacy Sensitive Protocols and Mechanisms for Mobile Contact Tracing
通过大规模检测和接触者追踪工作，COVID-19对全球健康的威胁在许多情况下得到了控制。我们创建本文档是为了建议三种功能，说明如何最好地利用计算技术来支持公共卫生组织的目标，即最大限度地减少与COVID-19传播相关的发病率和死亡率，同时保护个人的公民自由。特别是，这项工作倡导第三方免费的方法来辅助移动联系人追踪，因为这种方法减轻了需要可信第三方的安全和隐私风险。我们还明确考虑了任何合同追踪系统中涉及的推理风险，其中对用户的任何警报本身都可能导致去匿名化信息。更广泛地说，我们希望参与将工业界、学术界和民间社会的同事聚集在一起，围绕缓解COVID-19疫情的努力所引发的关键问题进行讨论并达成一致意见。
2020-05-07 cs.CR
A Security Enhanced Authentication Protocol
本文分析两种最新认证协议，指出其易受重放和修改攻击且存在技术正确性问题，并提出保持性能的改进方案。
2023-12-23 cs.CR
DHP Framework: Digital Health Passports Using Blockchain -- Use case on international tourism during the COVID-19 pandemic
为控制COVID-19疫情，多个国家实施延长社交距离措施达数周，实际上暂停了大部分经济活动。为了安全地恢复经济活动，已经成功引入了几种数字接触者追踪应用程序和协议。然而，DCT是一种反应性方法，因为它旨在打破人口中现有的疾病传播链。因此，DCT不适合主动预防疾病的传播;这种方法与某些用例相关，例如国际旅游，其中个人跨境旅行。在这项工作中，我们首先确定的局限性DCT相关的隐私问题，公众不愿意使用DCT移动应用程序，由于隐私问题，不同的DCT应用程序和协议之间缺乏互操作性，并假设有有限的，本地的人口流动性。然后，我们讨论了健康护照的概念，作为一种手段，验证个人是无疾病风险，以及如何可以用来恢复国际旅游业。接下来，我们介绍了DHP框架，该框架使用私有区块链和权威证明来签发数字健康护照。该框架提供了一个分布式基础设施，支持外国卫生系统签发卫生保健计划，并由航空公司和边境管制当局等相关利益攸关方进行核查。我们讨论了系统的可用性和性能，安全性和隐私方面的属性。最后，我们的结论是确定我们的工作，需要严格保证通过适当的安全协议的正式安全和隐私属性的未来扩展。
2020-05-19 cs.CR cs.CY
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
Cryptanalysis on Secure ECC based Mutual Authentication Protocol for Cloud-Assisted TMIS
本文对Kumar等人提出的基于ECC的云辅助TMIS双向认证协议进行密码分析，发现其存在健康报告泄露和机密性缺陷。
2023-06-13 cs.CR cs.IT math.IT
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
Analysis of the DoIP Protocol for Security Vulnerabilities
在ISO 13400中定义的DoIP是用于诊断数据的传输协议栈。诊断数据是车辆的潜在攻击媒介，因此必须保证安全传输以保护敏感数据和车辆。以前的工作分析了DoIP协议的草案版本和早期版本，没有传输层安全性（TLS）。DoIP协议没有正式的分析。这项工作的目标是调查的DoIP协议的设计缺陷，可能会导致安全漏洞和可能的攻击，利用他们。为此，我们演绎分析的DoIP协议的第一步，随后正式确认我们的结论。对于形式分析，我们使用证明器Tamarin。在此基础上，我们提出了提高DoIP安全性的对策，指出DoIP协议不能被认为是安全的，主要是因为DoIP协议中的TLS和客户端认证等安全机制不是强制性的。我们提出了一些措施来缓解我们确认激活TLS后仍然存在的漏洞。这些只需要对协议进行微小的重新设计。
2022-11-22 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
Formalization of Quantum Protocols using Coq
量子信息处理是物理学和计算机科学交叉的一个令人兴奋的研究领域，具有影响信息处理系统未来发展的巨大潜力。实用的、通用的量子计算机的建造可能要到未来几年。然而，量子通信和量子密码学已经发展得很好。商业量子密钥分发系统很容易获得，世界各地已经内置的了几个QKD网络。在这些实现中使用的协议的安全性依赖于信息理论证明，这可能会或可能不会反映实际的系统行为。此外，对实现的测试不能保证没有bug和错误。本文提出了一种新的量子协议建模和验证框架，并使用证明助手Coq实现。我们为量子比特（qubit）、量子门和量子测量提供了一个Coq库。作为验证实际量子通信和安全协议（如量子密钥分发）的一步，我们支持多量子比特，通信和纠缠。我们通过对量子隐形传态协议进行建模来说明这些概念，该协议仅使用经典信道来传达未知量子比特的状态。
2015-11-05 cs.CR cs.LO
