• エンジニアブログ

2023.09.07

CSCE 2023 国際学会で研究成果を発表

mienotakehiko_sam23_005.jpg 三重野 武彦です。
信州大学とセキュリティの共同研究を実施しています。

昨年に続き、2023 World Congress in Computer Science, Computer Engineering, and Applied Computing の国際会議が、2023年7月24日～27日に、米国ネバダ州ラスベガスの「Luxor by MGM Resorts International」で開催されました。

この会議はセキュリティを始め、コンピューター サイエンス、コンピューター エンジニアリング、データ サイエンス、人工知能、STEM、および応用コンピューティングの研究者が年に1度集まって開催される主要5大会議の1つです。
約75の国と地域からの参加者が来ています。
コロナが明け大勢の参加者が集い、期間中毎日活発な議論が行われていました。
多数の基調講演とチュートリアルや、パネルセッションも同時に実施されているので、まるで大きな展示会の様相でした。

私は2日目の7月25日に登壇。
[CSCE2023] (https://www.american-cse.org/csce2023/program)

    [研究内容]
今回は技術的な内容に特化して発表をしてきました。
mienotakehiko_sam23_001.jpgmienotakehiko_sam23_002.jpg
TLS1.3 で採用されている Authenticated Encryption with Associated Data (AEAD) の構造を形式化し、秘匿性と完全性について形式検証を行い、安全性検証の過程とその結果について考察した内容です。
このような形式化を行っている理由ですが、現在開発中の認証プロトコルに、暗号プロトコル評価フレームワークの国際標準ISO/IEC29128を適用するため、設計プロセスに自動検証ツールの導入を検討しているからです。
他にも多々実施することがあるのですが、現在は、暗号プロトコルの自動検証ツールである Tamarin-proverを用い、検証出来る能力を探っています。

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

    [風景(砂漠地帯でも、大量の電力を消費しています。)]
mienotakehiko_sam23_003.jpg

この記事を書いた人

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

戻る