暗号ソフトウェアの実装に対するセキュリティ検証

1.game-basedな安全性証明手法の拡張:代表者であるNowakは中国科学院のYu Zhang氏と共同で、引き続き任意の一様なデータを標本抽出するという処理をランダムビットとして実装する問題について研究を続けた。彼の以前開発した確率的多項式時間プログラムに対する識別不能性の解析証明システムCSLRにさらに拡張を加え、これを用いた暗号プリミティブの安全性証明を行うことができた。本成果はThe Fourth International Conference on Provable Security (ProvSec 2010)で発表された。検証ツールの実装を作っている。2.暗号スキーム実装の安全性証明:ケーススタディとして、Blum,Blum and Shubによって提案された疑似乱数生成器を用いた場合のElGamal暗号スキームの安全性について検討をした。3."Toolbox"の拡張:無限の時間があれば解読可能な暗号プリミティブが現実的な攻撃者に対して頑強であることを示すためには攻撃の実行時間を鍵長などの多項式時間によって制限する形で定式化を行うが、チューリングマシンなどの実装の詳細なモデルを対象に実行手順数をカウントすると極めて煩雑になる。我々はプログラミング言語による記述を複雑度と結びつける間接的な手法を用い、実行モデルに依存しない結果を得る。代表者であるNowakはフランスのINRIAのSylvain Heraud氏と共同で、"Toolbox"の拡張を作った。多項式時間関数の計算量の構文的処理による分類の手法について研究を行った。本成果はThe second International Conference on Interactive Theorem Proving (ITP 2011)で発表される。

1.game-basedな安全性証明手法の拡張:代表者であるNowakは中国科学院のYu Zhang氏と共同で、引き続き任意の一様なデータを標本抽出するという処理をランダムビットとして実装する問題について研究を続けた。彼の以前開発した確率的多項式時間プログラムに対する識別不能性の解析証明システムCSLRにさらに拡張を加え、これを用いた暗号プリミティブの安全性証明を行うことができた。本成果はThe Fourth International Conference on Provable Security (ProvSec 2010)で発表された。検証ツールの実装を作っている。2.暗号スキーム実装の安全性証明:ケーススタディとして、Blum,Blum and Shubによって提案された疑似乱数生成器を用いた場合のElGamal暗号スキームの安全性について検討をした。3."Toolbox"の拡張:無限の時間があれば解読可能な暗号プリミティブが現実的な攻撃者に対して頑強であることを示すためには攻撃の実行時間を鍵長などの多項式時間によって制限する形で定式化を行うが、チューリングマシンなどの実装の詳細なモデルを対象に実行手順数をカウントすると極めて煩雑になる。我々はプログラミング言語による記述を複雑度と結びつける間接的な手法を用い、実行モデルに依存しない結果を得る。代表者であるNowakはフランスのINRIAのSylvain Heraud氏と共同で、"Toolbox"の拡張を作った。多項式時間関数の計算量の構文的処理による分類の手法について研究を行った。本成果はThe second International Conference on Interactive Theorem Proving (ITP 2011)で発表される。