• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2016 年度 実績報告書

計算機を用いた暗号プロトコルの安全性に関する研究

研究課題

研究課題/領域番号 26730067
研究機関長崎大学

研究代表者

荒井 研一  長崎大学, 工学研究科, 助教 (60645290)

研究期間 (年度) 2014-04-01 – 2017-03-31
キーワード暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / ProVerif / CryptoVerif / Mizar
研究実績の概要

計算機を用いた暗号プロトコルの安全性検証(評価)として、暗号プロトコルの安全性自動検証ツールProVerifを用いた暗号プロトコルの安全性検証を行った。

1.現在標準化の議論が進められているTLS 1.3(Transport Layer Security TLS Protocol Version 1.3)のハンドシェイクプロトコルに対してProVerifを用いて形式的に記述し、その安全性検証を行った。具体的には、TLS 1.3のドラフト仕様を継続的に形式化し、その安全性検証を行った。結果として、TLS 1.3ハンドシェイクプロトコルに対する安全性(Secrecy、Authentication、さらにはForward Secrecy)を示すことに成功した。また、本成果は国際的な協力体制で暗号プロトコルの安全性評価に取り組んでいる暗号プロトコル評価技術コンソーシアム(CELLOS)の活動にも貢献した。

2.ProVerif をはじめとする暗号プロトコルの安全性自動検証ツールは、暗号プリミティブの形式化が正しく行われているかどうかの評価は人手で行う必要がある。すなわち、暗号プリミティブの形式化の正当性を検証する手段が用意されていない。よって、ProVerifにおける暗号プリミティブの形式化に関する研究を行った。具体的には、昨年度提案した方法である、ProVerif で形式化した暗号プリミティブをProVerif 自身の検証器を用いて形式化の正当性を検証する方法を拡張した。結果として、公開鍵暗号方式に求められる安全性の概念であるCCA(CCA1、CCA2)安全性の形式化及び検証に成功した。これにより、ProVerifにおける暗号プリミティブの記述能力の向上、さらには安全性検証の信頼性を高めることに成功した。

  • 研究成果

    (2件)

すべて 2017 2016

すべて 学会発表 (2件)

  • [学会発表] ProVerifにおけるphaseについて2017

    • 著者名/発表者名
      荒井研一、岡崎裕之、布田裕一
    • 学会等名
      2017年 暗号と情報セキュリティシンポジウム(SCIS2017)
    • 発表場所
      ロワジールホテル那覇(沖縄県那覇市)
    • 年月日
      2017-01-25
  • [学会発表] ProVerif での形式化における技術的な注意点について2016

    • 著者名/発表者名
      荒井研一、岡崎裕之
    • 学会等名
      日本応用数理学会 2016年度 年会
    • 発表場所
      北九州国際会議場(福岡県北九州市小倉)
    • 年月日
      2016-09-12

URL: 

公開日: 2018-01-16  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi