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

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

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

密码协议的安全性分析需要超越直觉——本文讲解 Dolev-Yao 符号模型、BAN 逻辑、ProVerif/Tamarin 等自动化验证工具，以及 TLS 1.3、Signal 等真实协议的形式化验证实践