暗号アルゴリズムの安全性検証技術の基礎研究で、世界に先駆けて「データの状態を保持したままの繰返し処理を形式化する技術の構築」 を実現

エプソンアヴァシス株式会社(本社：長野県上田市、代表取締役：武井 喬)の三重野 武彦 (主筆)、および信州大学 大学院総合理工学研究科 工学専攻 岡﨑 裕之准教授、長崎大学 情報データ科学部/大学院工学研究科 荒井 研一准教授、東京工科大学 コンピュータサイエンス学部 コンピュータサイエンス学科 布田 裕一教授からなる研究グループは、IEEE Access Open Access Journalの最新号に、暗号アルゴリズムの安全性検証技術に関する研究成果を発表しました。
著者らは、プライベートチャネルを用いたプロセス間の通信で、ProVerifを利用して、データの状態を保持したまま、繰返し処理を形式化する方法を提案しました。これは、多くの暗号プロトコルの形式化とその安全性の形式的検証の効率化に大きく貢献できる成果となります。

■研究の概要と背景
本研究では、暗号プロトコルの安全性評価の有効性に着目し、IoTデバイスやPC等の計算機能を用いた、暗号プロトコルの安全性評価を厳密かつ容易に行うことができる手法の実現に向け検討を行っています。

本研究でのフォーマルメソッド(形式手法)を用いた安全性評価は、暗号の安全性検証に形式的定理証明やモデル検査等の形式手法を用いる試みとして、近年注目を集めていますが、最も成功している暗号安全性検証用モデル検査器の１つにProVerif (※1) があります。ProVerifは、暗号に対する攻撃を網羅探索し、その攻撃手順を導出することで、暗号の安全性を検証するメジャーなツールの一つであり、本研究ではこのProVerifを利用しています。

(※1) モデル検査器ProVerif :フランス国立情報学自動制御研究所で最初に提唱・開発された、Cryptographic protocol verifier in the formal model

参考URL：https://www.inria.fr/fr
　　　　　https://bblanche.gitlabpages.inria.fr/proverif/

■成果と今後
繰返し処理をどう形式化するかは、形式検証の研究者にとって、大変にポピュラーなテーマです。暗号プロトコルは、多数の繰返し処理構造を持つアルゴリズムを持つことが多いため、本研究では、その特徴に着目し「データの状態を保持したままの繰返し処理を形式化する」革新的な方法を提案しました。

具体的には、ハッシュ関数のMD構造 (図1) やブロック暗号のCBCモード (図2) 等の事例を、関数呼び出しの形式モデル (図3) として記述し、その形式化の正しさを確認しました。また、その妥当性を実証するために、一方向圧縮関数とその出力によって変更される内部変数を含めることにより、データの状態を保持し、繰返し実行のように動作するMD構築手法の安全性を、衝突困難性を含め厳密に形式検証しました。更に、共通のブロック暗号動作モード、つまり、反復実行を処理するために提案した方法で使用される、CBC モードを形式化する方法も提示しました。

現在この手法を使いこなすには、モデル検査と暗号理論の専門知識を必要としますが、ProVerifをはじめとするモデル検査器と本手法による形式化手法を活用することにより、産業界はじめ実社会で広く利用されている、さまざまな暗号アルゴリズムの安全性検証を厳密かつ容易に出来るようにすることを目標としています。

図1

図2

図3

なお、本成果は、電気・電子工学分野における世界最大の学術・技術研究機関である米国電気電子学会(IEEE)が発刊する国際ジャーナル「IEEE Access」に受理、3月4日に掲載されました。

●論文タイトル : How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif
●著者 : Takehiko Mieno（三重野 武彦）, Hiroyuki Okazaki（岡崎 裕之）, Kenichi Arai (荒井 研一), Yuichi Futa (布田 裕一)
●ジャーナル名 : IEEE Access
●論文 URL : https://ieeexplore.ieee.org/document/10443411

【お問い合わせ先】
問い合わせフォームよりお願いいたします。