论文标题
安全协议的合理验证：从设计到可互操作实现（扩展版本）
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
论文作者
论文摘要
我们提供了一个框架，该框架由工具和MetAtheorems组成，用于端到端的安全协议验证，该协议弥合了自动化协议验证和代码级证明之间的差距。我们会自动将tamarin协议模型转换为以分离逻辑表达的一组I/O规格。每个这样的规范都描述了协议角色的预期I/O行为，然后对角色的实现进行了验证。我们的健全性结果确保了经过验证的实现继承了塔玛林模型证明的所有安全性（Trace）属性。因此，我们的框架使我们能够利用塔玛林的大量验证工作来验证新的和现有的实现。使用任何分离逻辑代码验证程序的可能性为目标语言提供了灵活性。为了验证我们的方法并表明它扩展到现实世界方案，我们验证了官方GO实施VireGuard VPN密钥交换协议的很大一部分。
We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against which the role's implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework thus enables us to leverage the substantial body of prior verification work in Tamarin to verify new and existing implementations. The possibility to use any separation logic code verifier provides flexibility regarding the target language. To validate our approach and show that it scales to real-world protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol.
