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