Specifications, Proofs and Animations for Cryptographic Protocols

加密协议的规范、证明和动画

• 批准号: DP0345775
• 负责人: Prof Colin Boyd
• 金额: $ 10.49万
• 依托单位: Queensland University of Technology
• 依托单位国家: 澳大利亚
• 项目类别: Discovery Projects
• 财政年份: 2003
• 资助国家: 澳大利亚
• 起止时间: 2003-03-19 至 2007-06-30
• 项目状态: 已结题
• 来源: https://dataportal.arc.gov.au/RGS/Web/Grants/DP0345775
• 关键词: Specifications; Proofs; Animations; 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.

加密协议是电子通信的基本安全工具。尽管经过多年的深入研究，仍然很难对几乎所有新协议的安全性获得高度信任。 计算机安全社区的研究强调形式规范和基于状态的搜索，而密码学社区则专注于复杂性理论证明。该项目将通过正式指定和动画化密码证明中使用的模型，首次统一这两种方法。结果将是从业者可以独特地获得证明，并且增加对证明的正确性和相关性的信心。