SCIS 2024 長崎で行われた暗号と情報セキュリティシンポジウムで研究成果を発表してきました

データ&リサーチGrp の三重野 武彦です。
信州大学とセキュリティの共同研究を実施しています。

2024 Symposium on Cryptography and Information Securityが、2024年1月23日～26日、長崎の「出島メッセ長崎」で開催されました。 こちらの学会には、国内外から約1,000人の参加者、83の主要なセッションが含まれ、345の技術・研究・パネルセッション、および基調講演とナイトセッションが行われました。
1984年から毎年1回ずつ日本国内で開催されているシンポジウムで、暗号と情報セキュリティ技術に関する最新の研究成果を発表し、情報交換の場を提供しているものです。
私は1日目の1月23日と、3日目の1月25日の夜に発表をしてきました。

[SCIS2024] (https://www.iwsec.org/scis/2024/program.html)

[研究内容]

[ProVerifとTamarin proverを開発支援プロセスへ導入するための考察]
近年、セキュリティプロトコルの解析や検証する手法として、形式手法が有効である研究報告が増加しています。その中でも、暗号プロトコルの安全性自動検証ツールであるProVerifやTamarin proverは、形式検証の分野で幅広く利用されています。
ProVerifは、モデルによって"cannot be proved"、すなわち、ProVerifでは検証結果が判断できないので、検証者に攻撃導出手順の判断を委ねることがあります。この場合に、Tamarin proverを用いて検証することで、厳密にモデルのセキュリティ特性や弱点を判断することができる可能性があります。
そのため、両ツールを用いて、ProVerifが観測等価性の同値性が成立しない場合:"Observational equivalence cannot be proved."を出力するモデルの検証を行いました。
この仮説を基に、セキュア・プロトコルを開発支援する初期段階で、ProVerifによる検証を行い、その後検証結果に基づいて、更に詳細な検証やセキュリティ特性の証明を、Tamarin proverで検証することを検討しています。それぞれのツールの使い所を考察した上で、バグの少ないセキュア・プロトコルの設計に役立つとことを議論しました。

[最後に]

今後も、実務で扱う暗号プロトコルの安全性評価とプロトコル開発設計の支援に向けて、両者の記述能力を探ることを実施していきます。更に、暗号の専門家に特化したモデル検証ツールや定理証明ツールだけではなく、これらツールの良い特徴を取り入れ、ITアーキテクトやエンジニアが求めている、検証結果が分かり易い自動検証ツールの新しい開発を模索し、安全性の保証がどこまで出来るのかを明確にしていきます。

[ナイトセッションでの発表(撮影は許可を頂いています)]

大勢の聴講者がいました。

この記事を書いた人

データ＆リサーチグループの三重野です
南の下田育ち、トレランと数学好きの企業研究者。現在は、信州大学大学院にて、セキュリティの基礎研究をしていますよ。