From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
该论文聚焦于一个长期存在的安全工程问题：即时通信协议的「形式化规范保证」与「实际运行实现行为」之间存在落差。Signal 协议为数以十亿计的用户提供加密通信，是 WhatsApp（全球用户量最大的消息应用）与 Signal 官方客户端的底层
#protocol-verification
共收录 5 条相关情报。
← 返回所有主题Accountability in Certificate Transparency and Variants
该论文针对证书透明化（Certificate Transparency, CT）这一已被所有主流浏览器支持的 TLS 证书生态机制，重新梳理其安全目标并给出严格的形式化分析。CT 的设计初衷是降低对证书颁发机构（CA）的信任依赖：所有 CA
Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅
An Interactive Prover for Protocol Verification in the Computational Model.
这篇 arXiv 论文提出了一套用于在计算模型下对安全协议进行机械化验证的框架和交互式证明器。研究背景是：安全协议设计的正确性至关重要，需要坚实的数学基础和计算机辅助方法。此前 Bana 和 Comon 提出的形式化方法只能分析固定会话数目
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和