土法炼钢兴趣小组的算法知识备份

【密码学百科】协议安全性分析：形式化验证与符号模型

2026-04-12 | cryptography | #protocol-analysis #Dolev-Yao #BAN-logic #ProVerif #Tamarin #Spin #symbolic-model #TLS-verification #Signal-verification

聚焦密码协议的形式化分析方法——从 Dolev-Yao 符号模型到 ProVerif/Tamarin/Spin 三大工具的深度对比，以 TLS 1.2 三重握手漏洞为完整案例，展示形式化工具如何发现真实协议中的致命设计缺陷