日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2014年研究部会連合発表会
日本応用数理学会2014年研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)セッション
表記の研究集会を下記のとおり開催しますので, ご案内申し上げます.
【日時】
2014年3月19日(水) 9:20--11:50
なお, 研究部会連合発表会の全体の開催期間は
2014年3月19日(水)〜20日(木) となっております.
【会場】
京都大学吉田キャンパス本部構内（京都市左京区吉田本町）総合研究8号館, 工学部総合校舎
http://chaosken.amp.i.kyoto-u.ac.jp/jsiam2014spring/
【参加費】
会員 学生¥1000/一般¥2000; 非会員 学生¥2000/一般¥4000
（＊参加費は当日受付にてお支払い下さい）
【詳細情報】
2014年研究部会連合発表会ホームページ:
http://chaosken.amp.i.kyoto-u.ac.jp/jsiam2014spring/
【プログラム】(○: 登壇者)
3月19日(水)
[9:20--10:20 数理的技法による情報セキュリティ(1)]
座長: 櫻田英樹（NTT）
9:20--9:40 (20分)
Externalized Universally Composable の枠組みに対する記号的モデル
○吉田真紀(情報通信研究機構)，鈴木斎輝(大阪大学)，藤原融(大阪大学)
9:40--10:00 (20分)
情報理論的に安全なSecret Handshake
○齋藤匡恭(千葉大学大学院 理学研究科)，多田充(千葉大学 統合情報センター)
講演資料
10:00--10:20 (20分)
negligible function の形式定義について
○岡崎裕之(信州大学)，布田裕一(北陸先端技術大学院大学)
講演資料
10:20--10:30
休憩
[10:30--11:50 数理的技法による情報セキュリティ (2)]
座長: 萩谷昌己 (東京大学)
10:30--11:00 (30分)
ProVerifによるワンタイムパスワード認証方式に対する形式的な安全性検証
○荒井研一(東京理科大学)，岩本智裕(東京理科大学大学院理工学研究科)，金子敏信(東京理科大学)
講演資料
11:00--11:30 (30分)
量子暗号プロトコルの形式的検証のための確率双模倣
○久保田貴大(東京大学)，角谷良彦(東京大学)，加藤 豪(NTT)，河野 泰人(NTT)，櫻田 英樹(NTT)
講演資料
11:30--11:50 (20分)
スケジューラを用いた量子プロセス間の観測同値
○安田和矢(東京大学 B4)，久保田貴大(東京大学 D3)，角谷良彦(東京大学)
講演資料
【備考】
プログラムは随時更新します. 最新情報は下記のホームページに掲載いたします.
FAIS ホームページ:
http://fais.jsiam.org/
【講演概要】
Externalized Universally Composable の枠組みに対する記号的モデル
○吉田真紀(情報通信研究機構)，鈴木斎輝(大阪大学)，藤原融(大阪大学)
概要:
暗号プロトコルの計算論的安全性を検証する際の重要な課題の一つとして，マッピング
補題が成立する記号的モデルを定義することが挙げられる．ここでマッピング補題が
成立するとは，元となる計算論的モデルにおいて無視できない確率で起きる実行状況が，
その記号的モデルにおいて起きる実行状況に対応付けられることである．これによって，
記号化による攻撃見逃しが無いことが保証される．本発表では，Externalized Universally
Composability (EUC) のモデルに対してマッピング補題が成立する記号的モデルを提案する．
EUC はPKIのようなグローバルな情報共有を想定したモデルであり，現在定式化されている
実用的な安全性の中で最も強いことが示されている．EUC安全な暗号プリミティブ
（公開鍵暗号や電子署名）の構成は未解決であるため，一般的な安全性をもつ
暗号プリミティブを使用するプロトコルを対象とした．
情報理論的に安全なSecret Handshake
○齋藤匡恭(千葉大学大学院 理学研究科)，多田充(千葉大学 統合情報センター)
概要:
本論文は，2003年にBalfanzらが提唱した相互匿名認証Secret Handshakeを，
情報理論的安全性の観点で考察する。現在用いられている暗号技術の多くは
計算量的な仮定をその安全性の根拠としているが，計算機を進歩を考慮すると
長期的な安全性の確保は困難となる。本論文では，Secret Handshakeに対する
情報理論的安全性を定義し，その安全性を満たす方式を構築する。提案方式は
文書復元型グループ署名を用いたものであり，2009年に清藤らが提案した
情報理論的に安全なグループ署名方式を，2009年に焦らが述べた「Secret
Handshakeに用いる文書復元型グループ署名方式の安全性の要件」を満たすように，
変形し利用する。
negligible function の形式定義について
○岡崎裕之(信州大学)，布田裕一(北陸先端技術大学院大学)
概要:
著者等は定理証明システムを用いた安全性証明検証システムの開発を進めている．
暗号理論において，必要不可欠であるnegligible functionの定義を行うにあたり，
形式言語上で記述を行うためには，一般的に知られているnegligible functionの定義
では必ずしも十分に厳密とは言えない．そこで，本研究では形式化に適し，かつ既存の
暗号理論体系に大きな影響を与えないような新たなnegligible functionの形式定義を
提案し、一般的な定義との比較および提案する定義についての考察を行う．
ProVerifによるワンタイムパスワード認証方式に対する形式的な安全性検証
○荒井研一(東京理科大学)，岩本智裕(東京理科大学大学院理工学研究科)，金子敏信(東京理科大学)
概要:
ProVerifは，Blanchetらが開発した形式モデル(Dolv-Yaoモデル)での暗号プロトコルの
自動検証ツールであり，Horn節を用いたプロトコル表現に基づいている．ProVerifは，
暗号プロコルに要求される秘匿や認証などの安全性検証を自動で行うことができ，
様々な暗号プロトコルの検証が可能である．また，ワンタイムパスワード認証方式は，
セッション毎にパスワードを変更することにより，通信路が盗聴されたとしても安全性を
保つことのできる認証方式であり，様々な方式が提案されている．本発表では，
ワンタイムパスワード認証方式についてProverifを用いて形式的に記述し，
安全性検証を行う．
量子暗号プロトコルの形式的検証のための確率双模倣
○久保田貴大(東京大学)，角谷良彦(東京大学)，加藤 豪(NTT)，河野 泰人(NTT)，櫻田 英樹(NTT)
概要:
量子プロトコルの検証において、プロトコルの等価関係が議論されることがある。
量子プロセス計算qCCSでは、プロトコルの等価関係は、それらを形式化した
コンフィグレーションの双模倣関係として表すことができる。従来の双模倣関係は、
コンフィグレーションたちが外から見て同じように振る舞うという意味であった。
本研究ではその条件を弱め、無視できる確率を除いて同じように振る舞うという、
確率双模倣関係を定義した。そして、この概念を用いてShorとPreskillによる
BB84鍵配送プロトコルの安全性証明におけるModified Lo-Chauプロトコルが安全
であることを形式的に検証した。
スケジューラを用いた量子プロセス間の観測同値
○安田和矢(東京大学 B4)，久保田貴大(東京大学 D3)，角谷良彦(東京大学)
概要:
量子プロセス計算において、bisimulationやbarbed congruenceといった量子プロセス間の
等価関係が定義されてきた。しかし、直感的には等価だといえるような量子プロセスで
あっても、これらの関係では等価とみなすことのできないものがある。そこで、観測同値
という等価関係を量子プロセス計算qCCSに導入する。観測同値では量子プロセス内部の
状態遷移を考慮せず、量子プロセス外部から観測可能な情報のみを考慮に入れる。
量子プロセスの状態遷移には確率的な遷移と非決定的な遷移が存在するため、
非決定性を解消して量子プロセス状態の確率分布を得るものとしてスケジューラを導入する。
観測同値はスケジューラの制限によって変化するため、それらの関係を調べる。
--------------------------------------------------------------------------
【問い合わせ先】
櫻田英樹 (NTTコミュニケーション科学基礎研究所)
sakurada.hideki(at)lab.ntt.co.jp
最終更新: 2014.2.20
FAISホームページにもどる．