日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2018年度年会FAISオーガナイズド・セッション
日本応用数理学会2018年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2018年度年会が2018年9月3日(月)～2018年9月5日(水)に
名古屋大学東山キャンパス（愛知県名古屋市千種区不老町）にて開催されます：
年会webページ http://annual2018.jsiam.org/
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします:
奮ってご参加下さいますようお願い申し上げます.
【日時】
9月5日(水) 9:30-10:50 および 11:00-12:20 (各80分)
【会場】
名古屋大学東山キャンパス
〒464-0814 愛知県名古屋市千種区不老町
http://www.engg.nagoya-u.ac.jp/access/campusmap.html
【参加方法】
年会webページをご覧ください.
★今回は同種写像暗号について高島克幸様(三菱電機/九州大学)に,
TLS1.3の形式検証について荒井研一様(長崎大学)にそれぞれ招待講演をお願いしております!★
近年，NISTの耐量子暗号標準化が始まり盛り上がっておりますが，
国内では格子関連の講演やチュートリアルは多く行われるものの，
それ以外のプリミティブについてはあまり講演がありませんでした．
高島様には最近注目を集めている耐量子暗号候補である同種写像暗号について，
数理的な側面と応用的な側面から最近のご研究内容を含めてご講演いただく予定です．
TLS1.3は先頃標準規格として承認され, 今後広く用いられることは確実です.
荒井様にはこのタイムリーな時期にTLS1.3の形式検証に関して,
研究グループにおけるこれまでの活動を総括してご講演いただく予定です.
技術的な観点だけではなく形式検証や暗号プロトコルの産業上の観点でも
大変興味深い内容となると思われます.
【プログラム】(○:登壇者)
研究部会 OS: 数理的技法による情報セキュリティ(1) ［9月5日：09:30-10:50：E］
座長: 山本 光晴 (千葉大学)
09:30-10:10
★招待講演★ ProVerifを用いたTLS1.3ハンドシェイクプロトコルの形式検証 (40分)
○荒井 研一 (長崎大学大学院工学研究科), 岡崎 裕之 (信州大学大学院理工学系研究科), 布田 裕一 (東京工科大学コンピュータサイエンス学部)
10:10-10:30
ProVerifの検証過程の可視化 (20分)
○吉田 真紀 (情報通信研究機構)
10:30-10:50
Scyther toolの検証過程の可視化 (20分)
○吉田 真紀 (情報通信研究機構)
研究部会 OS: 数理的技法による情報セキュリティ(2) ［9月5日：11:00-12:20：E］
座長: 花谷 嘉一 （(株)東芝 研究開発センター）
11:00-11:40
★招待講演★ 同種写像暗号の数理 (40分)
○高島 克幸 (三菱電機)
11:40-12:00
Groebner基底を用いた同種写像核計算 (20分)
○髙橋 康 (九州大学大学院数理学府), 安田 雅哉 (九州大学IMI研究所)
12:00-12:20
DeepLLLの改良とBKZへの組込みの提案 (20分)
○中邑 聡史 (九州大学大学院数理学府), 安田 雅哉 (九州大学IMI研究所)
【講演概要】
★招待講演★ ProVerifを用いたTLS1.3ハンドシェイクプロトコルの形式検証
○荒井 研一 (長崎大学大学院工学研究科), 岡崎 裕之 (信州大学大学院理工学系研究科), 布田 裕一 (東京工科大学コンピュータサイエンス学部)
[概要]
ProVerifはBlanchetらが開発した形式モデル(Dolev-Yaoモデル)での暗号プ
ロトコルの安全性自動検証ツールである．TLS 1.3はIETFにおいて2014年よ
り標準化の議論が進められており，2018年3月にdraft-28が標準規格として
承認された．講演者らは，これまでにProVerifを用いてTLS 1.3ハンドシェ
イクプロトコルを形式的に記述し，その安全性検証をdraft-06から継続的に
行ってきた．本講演では，講演者らのこれまでの取り組みを紹介する．
--------------------------------------------------------------------------
ProVerifの検証過程の可視化
○吉田 真紀 (情報通信研究機構)
[概要]
本研究では，一般にブラックボックスである安全性検証ツールの検証過程を
可視化することで検証結果の理解に貢献することを目的とする．本稿では，
安全性検証ツールとして ProVerif 1.92を対象とし，検証過程で生成される
情報（以降，内部情報）の抽出と可視化の手法を提案する．内部情報の抽出
では，処理の順序や論理的構造を木構造として表現し，可視化では，ソフト
ウェアのバージョン管理の可視化に使われるツールを応用してアニメーショ
ンとして表示する．そして，代表的な暗号プロトコルの検証過程を可視化し
た結果を示す．
--------------------------------------------------------------------------
Scyther toolの検証過程の可視化 (20分)
○吉田 真紀 (情報通信研究機構)
[概要]
本研究では，一般にブラックボックスである安全性検証ツールの検証過程を
可視化することで検証結果の理解に貢献することを目的とする．本稿では，
安全性検証ツールとして Scyther tool v1.1.3を対象とし，検証過程で生成
される情報（以降，内部情報）の抽出と可視化の手法を提案する．内部情報
の抽出では，処理の順序や論理的構造を木構造として表現し，可視化では，
ソフトウェアのバージョン管理の可視化に使われるツールを応用してアニメー
ションとして表示する．そして，代表的な暗号プロトコルの検証過程を可視
化した結果を示す．
--------------------------------------------------------------------------
★招待講演★ 同種写像暗号の数理
○高島 克幸 (三菱電機)
[概要]
量子計算機の出現に備えて, 量子計算機でも効率的に破れない公開鍵暗号の
研究が活発に行われている. 本講演では, その候補である同種写像暗号につ
いて概説する. 同種写像の計算法, 同種写像問題の困難性, そして同種写像
を使った暗号系とその安全性などに関して紹介する. また, 同種写像がなす
グラフには, ラマヌジャングラフや火山型グラフが現れて, それらは, 数理
的に興味深いだけでなく, 同種写像暗号を理解する上でも重要である. その
紹介と共に, 関連する私の研究成果についても触れる予定である.
--------------------------------------------------------------------------
Groebner基底を用いた同種写像核計算
○髙橋 康 (九州大学大学院数理学府), 安田 雅哉 (九州大学IMI研究所)
[概要]
超楕円曲線間の同種写像核計算問題（CSSI問題）に対しては現在，量子計算
機でも指数時間の攻撃法しか知られていない．そのため，CSSI問題を安全性
の根拠とする暗号方式である同種写像暗号は，耐量子暗号の一つとして期待
されている．本稿では，CSSI問題に対するGroebner基底計算を用いた求解方
法を提案する．さらに，Jaoらの提案した同種写像暗号（SIKE）に対する，
提案したCSSI問題求解法を用いた解読実験結果を報告する．
--------------------------------------------------------------------------
DeepLLLの改良とBKZへの組込みの提案
○中邑 聡史 (九州大学大学院数理学府), 安田 雅哉 (九州大学IMI研究所)
[概要]
格子暗号の安全性を支える最短ベクトル問題(SVP)の求解法として, LLLや
BKZなどが代表的である.LLLの自然拡張であるDeepLLLをBKZに組込んだ
“DEEP-BKZ”によるSVPチャレンジ記録更新が SCIS2018で報告された. 本稿
では, DeepLLLの簡約条件を強めた 改良DeepLLLとそれをBKZに組込んだ“改
良DEEP-BKZ”を提案する. また, 出力格子ベクトルの最小ノルムと実行時間
について, 既存方式と今回の提案方式を比較し,提案手法の有効性を検証す
る.
【問い合わせ先】
FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます)
代表：
吉田 真紀（情報通信研究機構）
幹事（五十音順）：
櫻田 英樹（日本電信電話(株) NTTコミュニケーション科学基礎研究所）
花谷 嘉一（(株)東芝 研究開発センター）
山本 光晴（千葉大学 大学院理学研究院）
米山 一樹（茨城大学 工学部 情報工学科）
最終更新: 2018.7.26
FAISホームページにもどる．