2016 Fiscal Year Annual Research Report
Computer-based Evaluation of Cryptographic Protocol Security
| Project/Area Number |
26730067
|
|---|
| Research Institution | Nagasaki University |
|---|
Principal Investigator |
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / ProVerif / CryptoVerif / Mizar |
|---|
| Outline of Annual Research Achievements |
計算機を用いた暗号プロトコルの安全性検証（評価）として、暗号プロトコルの安全性自動検証ツールProVerifを用いた暗号プロトコルの安全性検証を行った。
１．現在標準化の議論が進められているTLS 1.3（Transport Layer Security TLS Protocol Version 1.3）のハンドシェイクプロトコルに対してProVerifを用いて形式的に記述し、その安全性検証を行った。具体的には、TLS 1.3のドラフト仕様を継続的に形式化し、その安全性検証を行った。結果として、TLS 1.3ハンドシェイクプロトコルに対する安全性（Secrecy、Authentication、さらにはForward Secrecy）を示すことに成功した。また、本成果は国際的な協力体制で暗号プロトコルの安全性評価に取り組んでいる暗号プロトコル評価技術コンソーシアム（CELLOS）の活動にも貢献した。
２．ProVerif をはじめとする暗号プロトコルの安全性自動検証ツールは、暗号プリミティブの形式化が正しく行われているかどうかの評価は人手で行う必要がある。すなわち、暗号プリミティブの形式化の正当性を検証する手段が用意されていない。よって、ProVerifにおける暗号プリミティブの形式化に関する研究を行った。具体的には、昨年度提案した方法である、ProVerif で形式化した暗号プリミティブをProVerif 自身の検証器を用いて形式化の正当性を検証する方法を拡張した。結果として、公開鍵暗号方式に求められる安全性の概念であるCCA（CCA1、CCA2）安全性の形式化及び検証に成功した。これにより、ProVerifにおける暗号プリミティブの記述能力の向上、さらには安全性検証の信頼性を高めることに成功した。
|
