Computer-based Evaluation of Cryptographic Protocol Security

• Project/Area Number: 26730067
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Information security
• Research Institution: Nagasaki University (2015-2016); Tokyo University of Science (2014)
• Principal Investigator: ARAI Kenichi 長崎大学, 工学研究科, 助教 (60645290)
• Project Period (FY): 2014-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000); Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2015: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2014: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
• Keywords: 暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / ProVerif / Mizar / CryptoVerif

Outline of Final Research Achievements

The complexity of cryptographic protocols has increased in recent years in response to various requirements. This increase in complexity makes the evaluation of cryptographic protocol security difficult and increases the likelihood of human error. For this reason, the problem has arisen that many studies contain evaluation errors. This study focuses on the effectiveness of computer-based evaluation of cryptographic protocol security and aims to realize a method for rigorously conducting such evaluations. The results of this research will provide an effective solution for the serious problem of the increase in evaluation errors due to the growing complexity of cryptographic protocols.

Research Products

• [Journal Article] Difference of Function on Vector Space over F (2014)
  • Author(s): Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki
  • Journal Title: Formalized Mathematics Volume: 22(3) Issue: 3 Pages: 269-275
  • DOI: 10.2478/forma-2014-0027
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] ProVerifにおけるphaseについて (2017)
  • Author(s): 荒井研一、岡崎裕之、布田裕一
  • Organizer: 2017年 暗号と情報セキュリティシンポジウム（SCIS2017）
  • Place of Presentation: ロワジールホテル那覇（沖縄県那覇市）
  • Year and Date: 2017-01-25
• [Presentation] ProVerif での形式化における技術的な注意点について (2016)
  • Author(s): 荒井研一、岡崎裕之
  • Organizer: 日本応用数理学会 2016年度 年会
  • Place of Presentation: 北九州国際会議場（福岡県北九州市小倉）
  • Year and Date: 2016-09-12
• [Presentation] Proverifを用いた暗号プリミティブの形式化 (2016)
  • Author(s): 岡崎 裕之、荒井 研一
  • Organizer: 2016年 暗号と情報セキュリティシンポジウム（SCIS2016）
  • Place of Presentation: ANAクラウンプラザホテル熊本ニュースカイ（熊本県熊本市）
  • Year and Date: 2016-01-19
• [Presentation] ProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証（その2） (2016)
  • Author(s): 荒井 研一、徳重 佑樹、櫻田 英樹
  • Organizer: 2016年 暗号と情報セキュリティシンポジウム（SCIS2016）
  • Place of Presentation: ANAクラウンプラザホテル熊本ニュースカイ（熊本県熊本市）
  • Year and Date: 2016-01-19
• [Presentation] ProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証 (2016)
  • Author(s): 荒井 研一
  • Organizer: SCAIS (Small-workshop on Communications between Academia and Industry for Security) 2016
  • Place of Presentation: 熊本市国際交流会館（熊本県熊本市）
  • Year and Date: 2016-01-18
• [Presentation] 暗号プロトコル評価ツールProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証 (2015)
  • Author(s): 荒井 研一
  • Organizer: 暗号プロトコル技術評価コンソーシアム（CELLOS）シンポジウム2015
  • Place of Presentation: 株式会社インターネットイニシアティブ（東京都千代田区）
  • Year and Date: 2015-12-17
• [Presentation] ProVerif によるTLS1.3ハンドシェイクプロトコルの形式検証 (2015)
  • Author(s): 荒井 研一、渡辺 大、櫻田 英樹
  • Organizer: コンピュータセキュリティシンポジウム2015（CSS2015）
  • Place of Presentation: 長崎ブリックホール（長崎県長崎市）
  • Year and Date: 2015-10-21
• [Presentation] ProVerifによるTheft DoS Attackに耐性のあるワンタイムパスワード認証方式の形式的検証 (2015)
  • Author(s): 岩本 智裕, 荒井 研一, 金子 敏信
  • Organizer: The 32nd Symposium on Cryptography and Information Security (SCIS2015)
  • Place of Presentation: リーガロイヤルホテル小倉（北九州市）
  • Year and Date: 2015-01-20 – 2015-01-23
• [Presentation] Formal Verification of Improved Numeric Comparison Protocol for Secure Simple Paring in Bluetooth Using ProVerif (2014)
  • Author(s): Kenichi Arai, Toshinobu Kaneko
  • Organizer: The 2014 International Conference on Security and Management (SAM'14)
  • Place of Presentation: Monte Carlo Resort (Las Vegas, Nevada, USA)
  • Year and Date: 2014-07-21 – 2014-07-24