Specifications, Proofs and Animations for Cryptographic Protocols

加密协议是电子通信的基本安全工具。尽管经过多年的深入研究，几乎任何新协议的安全性都很难获得高可信度。计算机安全学界的研究侧重于形式规范和基于状态的搜索，而密码学学界则侧重于复杂性理论证明。该项目将首次统一这两种方法，正式指定和动画化加密证明中使用的模型。结果将是对从业者来说是唯一可获得的证明，同时增加了对证明既正确又相关的信心。

Cryptographic protocols are fundamental security tools for electronic communications. Despite years of intensive research it remains difficult to obtain high confidence in the security of almost any new protocol. Research in the computer security community has emphasised formal specifications and state based searching, while the cryptographic community has concentrated instead on complexity theoretic proofs. This project will unify these two approaches for the first time by formally specifying and animating the very models used in cryptographic proofs. The result will be proofs that are uniquely accessible to practioners combined with increased confidence that the proofs are both correct and relevant.