Automated Formal Analysis of Signal's Double Ratchet: Attacks, Fixes and Security Proofs.
本研究对 Signal 协议的核心组件——双棘轮（Double Ratchet）机制进行了自动形式化安全分析。双棘轮负责在消息丢失、重排序或临时密钥泄露等复杂条件下提供前向安全和后向安全。研究者使用 ProVerif 工具（一种自动密码协议
#formal verification
共收录 7 条相关情报。
← 返回所有主题Efficient and Timely Revocation of V2X Credentials.
该论文针对智能交通系统中车辆与基础设施间安全通信的关键需求，聚焦于恶意或异常车辆密码凭证的及时撤销问题。当前标准对撤销处理规定模糊，现有方案在可扩展性和有效性方面存在严重局限。为此，作者提出了一种形式化验证的车辆自撤销机制，该机制利用车辆中
Formal Analysis of Access Control Mechanism of 5G Core Network.
5G核心网作为下一代移动通信网络的核心，其访问控制机制的安全性至关重要。然而，由于5G核心网的复杂性，传统的安全分析手段难以全面覆盖其访问控制策略的潜在缺陷。本文提出5GCVerif，一个基于模型测试的形式化分析框架，专门用于分析5G核心网
Egocentric abstractions for modeling and safety verification of distributed cyber-physical systems.
该论文聚焦于分布式信息物理系统（如物联网、自动驾驶汽车）的安全建模与验证问题。传统建模方法在面对动态成员和复杂交互时变得笨重且不实用，例如多车交互场景中车辆相对位置和车道变化带来的挑战。为此，作者提出了一种以自我为中心的抽象方法，用于简洁地
Formal Verification of Probing Security via Conditional Independence
本文针对密码系统侧信道攻击的掩码防御机制，提出了一种基于概率分离逻辑的形式化验证方法，用于自动验证掩码算法的非干扰性安全属性。作者首先建立了非干扰性与条件独立性之间的数学联系，从而将安全验证问题转化为条件独立性推理问题。随后，利用现有的Li
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
论文提出了一种混合形式化验证方法，结合高层演绎推理和电路级推理，用于高度优化的加密汇编代码。该方法在 EasyCrypt 证明助手中扩展实现，通过使用等价性检查将安全保障传播到同一计算的不同优化或不同架构的实现中，从而降低低级别函数的证明工
Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、M