Computer-based Evaluation of Cryptographic Protocol Security

基于计算机的密码协议安全性评估

• 批准号: 26730067
• 负责人: ARAI Kenichi
• 金额: $ 1.25万
• 依托单位: Nagasaki University (2015-2016)Tokyo University of Science (2014)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2014
• 资助国家: 日本
• 起止时间: 2014-04-01 至 2017-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-26730067/
• 关键词: 暗号プロトコル; 安全性; フォーマルメソッド; 自動検証; 自動証明; ProVerif; Mizar; CryptoVerif

项目成果

Formal Verification of Improved Numeric Comparison Protocol for Secure Simple Paring in Bluetooth Using ProVerif

使用 ProVerif 对蓝牙中安全简单配对的改进数字比较协议进行形式验证

• 发表时间: 2014
• 作者: Kenichi Arai;Toshinobu Kaneko
• 通讯作者: Toshinobu Kaneko

Difference of Function on Vector Space over F

F 上向量空间函数的差分

• DOI: 10.2478/forma-2014-0027
• 发表时间: 2014
• 期刊: Formalized Mathematics
• 影响因子: 0.3
• 作者: Kenichi Arai;Ken Wakabayashi;Hiroyuki Okazaki
• 通讯作者: Hiroyuki Okazaki

ProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証（その2）

使用 ProVerif 对 TLS1.3 握手协议进行形式化验证（第 2 部分）

• 发表时间: 2016
• 作者: 荒井 研一;徳重 佑樹;櫻田 英樹
• 通讯作者: 櫻田 英樹

ProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証

使用 ProVerif 对 TLS1.3 握手协议进行形式化验证

• 发表时间: 2016
• 作者: 三改木 裕矢;高橋 翔;小川 貴弘;長谷山 美紀;荒井 研一
• 通讯作者: 荒井 研一

暗号プロトコル評価ツールProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証

使用密码协议评估工具ProVerif对TLS1.3握手协议进行形式化验证

• 发表时间: 2015
• 作者: 三改木 裕矢;高橋 翔;小川 貴弘;長谷山 美紀;荒井 研一;Hsiang-Yun Wu;松原靖子;高橋翔，長谷山美紀;Hsiang-Yun Wu;荒井 研一
• 通讯作者: 荒井 研一