| 研究課題/領域番号 |
26730067
|
|---|
| 研究機関 | 長崎大学 |
|---|
研究代表者 |
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | 暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / ProVerif / Mizar / CryptoVerif |
|---|
| 研究実績の概要 |
計算機を用いた暗号プロトコルの安全性検証（評価）として、暗号プロトコルの安全性自動検証ツールProVerifを用いた暗号プロトコルの安全性検証を行った。
１．インターネット技術の標準化推進団体IETFにおいて標準化の議論が進められているTLS 1.3（Transport Layer Security TLS Protocol Version 1.3）のハンドシェイクプロトコルに対してProVerifを用いて形式的に記述し、その安全性検証を行った。具体的には、TLS 1.3のドラフト06以降の仕様を継続的に形式化し、その検証を行った。結果として、TLS 1.3ハンドシェイクプロトコルに対する安全性（秘匿及び認証）を示すことに成功し、その結果をTLS 1.3の標準化に反映させることに成功した。また、本成果は国際的な協力体制で暗号プロトコルの安全性評価に取り組んでいる暗号プロトコル評価技術コンソーシアム（CELLOS）の活動にも貢献した。
２．ProVerifは（暗号プロトコルの構成部品である）暗号プリミティブの形式化の正しさを検証する仕組みがないため、その検証は困難である。よって、ProVerifにおける暗号プリミティブの形式化に関する研究を行った。結果として、暗号プリミティブを暗号プロトコルの一種として形式化することで、形式化の正当性を検証する手法を提案することに成功した。これにより、ProVerifにおける暗号プリミティブの形式化表現能力を向上させることに成功した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
CryptoVerifにおける観測等価性を満たすことの証明をMizar上で実現するためのライブラリ開発を現在進めているが、やや遅れている。一方で、ProVerifを用いた暗号プロトコルの安全性検証（評価）を行い、世界的な注目を集めている暗号プロトコル（TLS1.3）に対して安全性を検証することに成功し、さらにProVerifにおける暗号プリミティブの形式化表現能力を向上させることにも成功したため、計算機を用いた暗号プロトコルの安全性証明のさらなる厳密化の可能性を探ることには成功した。以上より、おおむね順調に進展している部分とそうでない部分があるため、全体としてはやや遅れていると判断される。
|
| 今後の研究の推進方策 |
観測等価性を満たすことの証明をMizar上で実現するために必要なライブラリの充実化を図る。上記成果をもとに、CryptoVerifにおける観測等価性を満たすことの証明をMizar上で実現し、計算機を用いた暗号プロトコルの安全性証明を厳密にできる手法を提案する。また、本研究が計画通りに進まない場合の対応策として、ProVerifを用いた暗号プリミティブの形式化のアイディアを応用し、観測等価性を満たすことの評価をProVerif上で実現する。これにより、計算機を用いた暗号プロトコルの安全性証明を厳密にできる手法を提案する。
|
| 次年度使用額が生じた理由 |
研究代表者の所属変更に伴い、いくつかの出張が行えなかったため。さらに、英文校閲代をその他の経費として計上していたが、校閲が不要となったため。
|
| 次年度使用額の使用計画 |
次年度は旅費の経費が不足すると考えられるため、旅費の経費として計上する。
|
