SCIS 2023 研究成果発表 in 小倉

DAR 三重野 武彦です。

信州大学とセキュリティの共同研究を実施しています。
2023 Symposium on Cryptography and Information Securityが、2023年1月24日～27日に、小倉の「リーガロイヤルホテル小倉」で開催されました。

こちらの学会には,国内外から約2,000人の参加者、78の主要なセッションが含まれ、234の技術・研究・パネルセッション、および基調講演とナイトセッションが行われました。

1984年から毎年1回ずつ日本国内で開催されているシンポジウムです。
暗号と情報セキュリティ技術に関する最新の研究成果を発表し、情報交換の場を提供しているものです。


私は3日目の1月26日に研究内容を発表してきました。
[SCIS2023](https://www.iwsec.org/scis/2023/SCIS_2023_program.html)

[発表内容]

[Tamarin-prover を用いたAEAD の形式的安全性検証]
David Basin らが開発したシンボリックモデルにもとづいて、暗号プロトコルの安全性検証を自動で行うツールの1つである Tamarin-proverを用いて、TLS1.3 で採用されている、Authenticated Encryption with Associated Data (AEAD) の構造を主に形式化し、秘匿性と完全性について形式検証を行い、安全性検証の過程とその結果について考察しました。
安全性要件の実行記述証明方法と観測等価性についても、手動証明を用いた安全性の検証を行い発表を致しました。

[今後の課題]

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

更に複雑なプロトコルであるAES-GCM(NIST-SP 800-38D), ChaCha20-Poly1305 等の形式検証を行い、Merkle-Damgard や CBCなどの繰り返し構造をどの程度形式化できるかを調査します。
今まで実施してきたモデル検査ツールProVerif による形式化技法と比較し、記述能力や検証結果の違いを明確にします。
そして検証結果を元に、モジュールへの安全性検証に使用できるツールの優位性や使い分けなどを引き続き探っていきます。

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

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

この記事を書いた人

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