| 研究課題/領域番号 |
26730067
|
|---|
| 研究機関 | 東京理科大学 |
|---|
研究代表者 |
荒井 研一 東京理科大学, 理工学部, 助教 (60645290)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | 暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / Mizar / CryptoVerif / ProVerif |
|---|
| 研究実績の概要 |
１、暗号プロトコル安全性自動証明ツールCryptoVerifにおける観測等価性を満たすことの証明をMizarプルーフチェッカ上で実現するために、不足しているライブラリの充実化を図った。実数値関数上の差分（forward difference、backward difference、central difference）の形式化記述は既に存在するが、ベクトル値関数上の差分の形式化記述は存在しない。ベクトル値関数上の差分は、観測等価性を満たすことの証明（特に、共通鍵暗号方式の安全性）を実現するために重要であるため、その形式化記述を行った。結果として、不足しているライブラリの充実化を図ることに成功した。
２、計算機を用いたさまざまな暗号プロトコルの安全性検証として、ProVerifを用いた暗号プロトコルの安全性検証を行った。まず、Yehらの提案したBluetoothのセキュアシンプルペアリングの方式に対して、ProVerifによる形式的検証を行った。結果として、なりすましに対する脆弱性を発見することに成功した。さらに、その脆弱性に対する対策法を提案することに成功した。次に、Isawaらの提案したワンタイムパスワード認証方式に対する形式的検証を行った。結果として、サーバに保存されている情報を利用し、なりすましを行う攻撃（Hybrid Theft Attack）及びサーバに保存されている情報を利用し、サーバとユーザ間の認証を不可能にする攻撃（Theft DoS Attack）に対する脆弱性を発見することに成功した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
CryptoVerifにおける観測等価性を満たすことの証明をMizar上で実現するためのライブラリ開発が順調に進んでいる。また、CryptoVerifは「ある暗号プロトコルがある安全性を満たす」ということを自動証明できるが、暗号プロトコルに脆弱性が存在した場合にその脆弱性を発見することはできない。脆弱性を発見可能であるProVerifを用いて暗号プロトコルの安全性検証を行い、いくつかの脆弱性を発見することに成功、すなわち、計算機を用いた暗号プロトコルの安全性証明のさらなる厳密化の可能性を探ることに成功したことからもおおむね順調に進展していると判断される。
|
| 今後の研究の推進方策 |
観測等価性を満たすことの証明をMizar上で実現するために必要なライブラリのさらなる充実化を図る。さらに、CryptoVerifを用いた暗号プロトコルの安全性証明を行い、ProVerifを用いた安全性検証も同時に進める。これらの成果をもとに、CryptoVerifにおける観測等価性を満たすことの証明をMizar上で実現する。なお、CryptoVerifは証明対象となる暗号プロトコルへの攻撃モデル及び安全性の根拠となる暗号プリミティブの安全性を与えると、暗号プロトコルの安全性を自動証明できる。その暗号プリミティブの安全性を記述する際には、観測等価性を満たす２つのプロセスとして記述する必要がある。よって、今後の推進方策としては、まず、それら記述の正しさをMizar上で証明する。さらに、可能であれば上記成果をもとにCryptoVerifにおける観測等価性を満たすことの証明をMizar上で実現する。
|
| 次年度使用額が生じた理由 |
英文校閲代をその他の経費として計上していたが、校閲が不要となったため。
|
| 次年度使用額の使用計画 |
全研究期間を通して旅費の経費が不足しているため、旅費の経費として計上する。
|
