日本応用数理学会2021年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2021年度年会が2021年9月7日(火)～2021年9月9日(木)に
オンライン形式で開催されます：
＊年会webページ＊
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします:
【日時】
9月9日(木) 9:10-10:30 および 10:50-11:50
【会場】
オンライン開催
【参加方法】
年会webページをご覧ください.
【プログラム】
下記の2セッションを予定しています.
研究部会OS: 数理的技法による情報セキュリティ(1) ［9月9日：9:10-10:30：D］
座長: 米山 一樹 (茨城大学)
◎[企画講演]Tamarin proverとTamarin proverを用いた少ない入力で検証できる方法
○中林 美郷 (NTT 社会情報研究所)
研究部会OS: 数理的技法による情報セキュリティ(2) ［9月9日：10:50-11:50：D］
座長: 吉田 真紀 (情報通信研究機構)
◎一般化Merkle-Damgård構造に対する計算機支援証明
○福留 直宙 (茨城大学), 米山 一樹 (茨城大学)
ProVerifを用いたPolicy-based Chameleon Hashによる修正可能なブロックチェーンの形式化
○杉山 航平 (信州大学), 荒井 研一 (長崎大学大学院工学研究科), 岡崎 裕之 (信州大学), 布田 裕一 (東京工科大学コンピュータサイエンス学部), 三重野 武彦 (エプソンアヴァシス株式会社)
解読不能なY00量子暗号装置とそのセッション鍵合意に向けて
○岩越 丈尚 (三重大学)
【講演概要】
◎[企画講演]Tamarin proverとTamarin proverを用いた少ない入力で検証できる方法
○中林 美郷 (NTT 社会情報研究所)
[概要]
Tamarin proverは暗号プロトコルの形式検証ツールの一つであり，
Dolev-Yaoモデルと呼ばれる暗号プリミティブを理想化したモデルに対して
安全性検証を行うことができる．しかし，その利用にあたって，入力コード
に含める必要のある情報が多いという問題がある．本発表では，Tamarin
proverの概要と，上記問題に対するアプローチであるTamarin proverを用い
たプロトコルの仕様のみから安全性検証を行う方法について述べる．
--------------------------------------------------------------------------
◎一般化Merkle-Damgård構造に対する計算機支援証明
○福留 直宙 (茨城大学), 米山 一樹 (茨城大学)
[概要]
Merkle-Damgård(MD)構造は定義域拡張の一種であり、多くのハッシュ関数の
基礎になっている。Backesらは定理証明支援系であるEasyCryptを用いて、
耐衝突性とIndifferentiabilityを厳密に証明した。一方、MD構造には多く
の実用的な亜種と、これらの亜種を捉えた一般化Merkle-Damgård(GMD)構造
が知られている。本稿では、GMD構造の耐衝突性をEasyCryptによって証明す
る。
--------------------------------------------------------------------------
ProVerifを用いたPolicy-based Chameleon Hashによる修正可能なブロックチェーンの形式化
○杉山 航平 (信州大学), 荒井 研一 (長崎大学大学院工学研究科), 岡崎 裕之 (信州大学), 布田 裕一 (東京工科大学コンピュータサイエンス学部), 三重野 武彦 (エプソンアヴァシス株式会社)
[概要]
ブロックチェーンは登録されたデータの変更ができないが，Derlerらによる
Policy-based Chameleon Hash(PCH) は，アクセスポリシーを満たすユーザ
によるブロックチェーンの修正を可能にした．また，ProVerifはBlanchetら
が開発した暗号プロトコルの自動検証ツールであり，暗号プロトコルの秘匿
や認証などの安全性要件を検証することができる．本稿では，PCHによる修
正可能なブロックチェーンをProVerifで形式化する方法について検討する．
--------------------------------------------------------------------------
解読不能なY00量子暗号装置とそのセッション鍵合意に向けて
○岩越 丈尚 (三重大学)
[概要]
代表的な量子暗号である量子鍵配送は、情報理論的安全として注目を浴びて
いるものの、認証鍵の合意方法が見つからず、計算量的安全な耐量子暗号に
よる認証の提案がなされている。一方、既存の通信インフラと親和性の良い
Y00量子暗号は情報理論的安全な設計可能性が示唆されたが具体的構成が不
明である。しかし実現した場合には情報理論的安全な鍵合意もY00量子暗号
で実行可能と示唆された。本講演では上記Y00通信機の設計の指針を概説す
る。
【問い合わせ先】
FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます)
代表：
吉田 真紀（情報通信研究機構）
幹事（五十音順）：
櫻田 英樹（日本電信電話(株) NTTコミュニケーション科学基礎研究所）
花谷 嘉一（(株)東芝 研究開発センター）
山本 光晴（千葉大学 大学院理学研究院）
米山 一樹（茨城大学 工学部 情報工学科）