Computational Logical Verification Method for Cryptographic Protocols

密码协议的计算逻辑验证方法

• 批准号: 21700023
• 负责人: HASEBE Koji
• 金额: $ 2.83万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21700023/
• 关键词: 仕様記述; 仕様検証; 形式手法; 暗号プロトコル; 安全性検証; 論理推論; 計算論的安全性; 数理的技法; 計算論的安全性証明

We developed an extended inference system based on Based Protocol Logic (BPL), a variant of first order logic for proving correctness of cryptographic protocols. This extended system was obtained from BPL by adding some computational aspects of cryptography and sound with respect to a computational semantics. We also demonstrated the usefulness of this system by proving secrecy property of some protocols, such as Needham-Schroeder protocol.

我们开发了一个基于基于协议逻辑（BPL）的扩展推理系统，这是用于证明加密协议正确性的一阶逻辑的变体。这个扩展系统是通过在计算语义方面添加密码学和声音的一些计算方面从 BPL 获得的。我们还通过证明一些协议（例如Needham-Schroeder协议）的保密性来证明该系统的实用性。

项目成果

Recent approaches to computational semantics for first-order logical analysis of cryptographic protocols

用于密码协议一阶逻辑分析的计算语义的最新方法

• 发表时间: 2009
• 作者: Gergely Bana;Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada

Secrecy-Oriented, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols

面向保密、计算合理的加密协议一阶逻辑分析

• 发表时间: 2010
• 作者: Gergely Bana;Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada

数理的技法による情報セキュリティ

使用数学技术的信息安全

• 发表时间: 2010
• 作者: 長谷部浩二;岡田光弘;バナ・ゲルゲイ
• 通讯作者: バナ・ゲルゲイ

計算論的に健全な一階述語論理による暗号プロトコルの分析

使用计算合理的一阶谓词逻辑分析密码协议

• 发表时间: 2012
• 作者: Gergely Bana;長谷部浩二;岡田光弘
• 通讯作者: 岡田光弘

Secrecy-Oriented Computationally Sound First-Order Logical Aanlysis of Cryptographic Protocols

面向保密的加密协议计算合理的一阶逻辑分析

• 发表时间: 2010
• 作者: Gergely Bana;Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada