Analyzing Multi-Factor Authentication Through Cryptographic Security Properties
该论文聚焦于现代身份认证体系中的多因素认证（MFA）平台，试图用密码学安全属性的形式化视角来审视其安全性，而不是依赖经验性的渗透测试或厂商自述。研究背景是：认证系统从早期的单一机制（用户名/口令、物理令牌、生物特征）逐步演变为把多种机制组合
#cryptographic-protocols
共收录 10 条相关情报。
← 返回所有主题Modular Design of Secure Group Messaging Protocols and the Security of MLS.
本文正式研究了安全群组消息（SGM）协议的安全性定义与模块化构造，并以 IETF 正在标准化的 Messaging Layer Security（MLS）协议为具体对象，填补了此前缺乏对完整 MLS 协议进行安全证明的空白。此前对 MLS
Certified in Theory, Broken in Practice: Assumption Gaps in Cryptographic Model Certification
本文研究了密码学模型认证（CMC）协议中的安全假设与实际部署之间的差距。隐私保护的机器学习审计协议允许审计员评估模型的准确性或公平性，而无需暴露模型内部或训练数据，因此特别适用于医疗、金融等敏感领域。然而，现有安全定义通常仅保证模型在固定审
CryptoBap: A Binary Analysis Platform for Cryptographic Protocols.
该论文提出 CryptoBap，一个用于验证加密协议二进制代码安全属性的平台。研究背景是：现实中的加密协议实现可能因编译器优化、平台差异或编程错误而引入安全漏洞，而传统的形式化验证方法通常针对高级语言或协议规范，难以直接分析编译后的机器码。
Algorithmically Presented Numbers and Canonical Representations in Cryptographic Protocols
本文从表示论的角度研究密码协议中的数字表示问题。传统观点认为，只要协议中的数值是计算上可访问的即可，但本文指出，在实际协议操作中，数值的固定表示形式同样关键。论文区分了三种表示论概念：算法可逼近数（A_app，即可计算实数）、系统中有限准确
LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
该论文提出了一种名为 LeanDY 的形式化验证框架，面向密码协议的安全性分析。现有工具要么全自动但表达能力有限，要么交互式证明灵活但自动化不足。LeanDY 通过结合基于类型推理（type-based reasoning）与基于轨迹推理（
Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin
该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性
FLUTE: Fast and Secure Lookup Table Evaluations.
本文提出FLUTE协议，用于安全多方计算（MPC）中快速且安全的查找表（LUT）评估。传统的布尔电路在安全计算中存在较大的在线阶段开销，而查找表可以替代传统门电路（如AND、XOR），生成更紧凑的电路，并显著提升在线性能。已有工作利用LUT
Deanonymizable Scoped Linkable Ring Signatures
该论文提出了一种新型环签名方案——Deanonymizable Scoped Linkable Ring Signatures (DSLRS)，旨在同时实现作用域可链接性与去中心化问责。传统的环签名虽能提供匿名性和签名者自主组成的灵活性，但
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
本文对IETF QUIC协议记录层的安全性进行了系统研究。QUIC是传输层协议，其记录层负责数据包加密和头部保护，IETF标准第30版相比Google原始协议和早期草案有重大变化。作者首先提出了一种新的安全定义——带半隐式nonce的认证加