日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2009年春の研究部会連合発表会
日本応用数理学会2009年春の研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)セッション
表記の研究集会を下記のとおり開催しますので, ご案内申し上げます.
【日時】
2009年3月7日(土) 10:00--12:30
なお, 研究部会連合発表会の全体の開催期間は
2009年3月7日(土)〜8日(日) 9:00--18:00 となっております.
【会場】
京都大学 理学部 6号館
アクセス: http://www.kyoto-u.ac.jp/ja/access/campus/map6r_n.htm
【参加費】
学生会員 ¥0, 一般会員 ¥1,000
学生非会員 ¥1,000, 一般非会員 ¥2,000
【講演申込】
締め切りました.
参考: 講演募集のご案内
http://fais.jsiam.org/2009-spring-jsiam-cfp.html
【プログラム】(○: 登壇者)
3月7日(土)
座長: 竹内 泉 (産業技術総合研究所 情報技術研究部門)
10:00--10:30
汎用的結合可能な鍵交換の安全性検証法【30分】
○鈴木 斎輝 (大阪大学大学院情報科学研究科)
吉田 真紀 (大阪大学大学院情報科学研究科)
藤原 融 (大阪大学大学院情報科学研究科)
講演資料
10:30--10:50
暗号プロトコルに対する公理的安全性検証法の主要処理の改良と実装【20分】
○鎌野 善樹 (大阪大学大学院情報科学研究科)
鈴木 斎輝 (大阪大学大学院情報科学研究科)
吉田 真紀 (大阪大学大学院情報科学研究科)
藤原 融 (大阪大学大学院情報科学研究科)
講演資料
10:50--11:00
休憩
11:00--11:30
CPA 安全な暗号とゼロ知識証明から構成される CCA1 安全な暗号の
確率的ホーア論理を用いた形式的検証【30分】
○久保田 貴大 (東京大学大学院情報理工学系研究科)
川本 裕輔 (東京大学大学院情報理工学系研究科)
萩谷 昌己 (東京大学大学院情報理工学系研究科)
講演資料
11:30--12:00
CryptoVerif の証明能力の改良：誤った判定の回避【30分】
○花谷 嘉一 ((株)東芝 研究開発センター)
角野 陽輔 (電気通信大学)
米山 一樹 (電気通信大学)
太田 和夫 (電気通信大学)
講演資料
12:00--12:30
暗号学的に安全な擬似乱数生成器の正しい実装に向けて【30分】
○山田 聖 (産業技術総合研究所 情報セキュリティ研究センター)
David NOWAK(ダヴィッド ノヴァック)
(産業技術総合研究所 情報セキュリティ研究センター)
講演資料
【備考】
1. 同日午後には「数論アルゴリズムとその応用」(JANT)研究部会
のセッションがございます.
2. プログラムは随時更新します.
最新情報は下記のホームページに掲載いたします.
FAIS ホームページ:
http://fais.jsiam.org/
2009年春の研究部会連合発表会ホームページ(準備中):
http://www.jsiam.org/modules/eguide01/event.php?eid=46
【問い合わせ先】
塚田恭章
NTTコミュニケーション科学基礎研究所
tsukada(at)theory.brl.ntt.co.jp
【講演概要】
-------------------------------------------------------
汎用的結合可能な鍵交換の安全性検証法
○鈴木 斎輝 (大阪大学大学院情報科学研究科)
吉田 真紀 (大阪大学大学院情報科学研究科)
藤原 融 (大阪大学大学院情報科学研究科)
[講演概要]
近年, 汎用的結合可能性の枠組みにおける安全性を記号的手法を
用いて形式的に検証する研究が行われている. 従来研究として,
相互認証プロトコルと鍵交換プロトコルを対象とする検証法が提
案されている. 本研究は, さまざまな暗号機能の汎用的結合可能
な安全性を検証可能とすることを目標とし, 我々の研究グループ
が提案した記号的手法 (公理的安全性検証法と呼ぶ) を用いるこ
とを考える. 今後多様な暗号機能を検証可能とするための知見を
得ることを目的とし, これまでに, 相互認証プロトコルを対象と
した検証法を提案した. 本発表では, 鍵交換プロトコルを対象と
した検証法を提案する.
-------------------------------------------------------
暗号プロトコルに対する公理的安全性検証法の主要処理の改良と実装
○鎌野 善樹 (大阪大学大学院情報科学研究科)
鈴木 斎輝 (大阪大学大学院情報科学研究科)
吉田 真紀 (大阪大学大学院情報科学研究科)
藤原 融 (大阪大学大学院情報科学研究科)
[講演概要]
近年, 計算量的安全性を記号的手法を用いて形式的に検証する研
究が活発に行われている. 我々の研究グループで用いている記号
的手法(公理的安全性検証法と呼ぶ)は, 他グループの手法と同等
の検証能力を有しているが未実装である. そこで本発表では, 公
理的安全性検証法の高速実装を目標とし, 本検証法で繰り返し実
行される主要処理を改良し実装する. そして検証例としてよく用
いられるプロトコルに対して検証時間を実測する.
-------------------------------------------------------
CPA 安全な暗号とゼロ知識証明から構成される CCA1 安全な暗号の
確率的ホーア論理を用いた形式的検証
○久保田 貴大 (東京大学大学院情報理工学系研究科)
川本 裕輔 (東京大学大学院情報理工学系研究科)
萩谷 昌己 (東京大学大学院情報理工学系研究科)
[講演概要]
暗号スキームは、IND-CPA や IND-CCA のようなゲームによって
定式化される標準的な安全性の証明とともに、提案されなければ
ならない。しかし、安全性の指標となる攻撃ゲームにおいて、一
般に攻撃者はさまざまな種類のオラクルにアクセスできるため、
安全性の証明は複雑になりやすく、検証が難しい。確率的ホーア
論理は、これまでゲームに基づいた安全性証明の中でも比較的単
純なものの形式化に用いられているが、より複雑なオラクルアク
セスを含む証明に対する有効性は明らかではない。そこで、本論
文ではゲームに基づく証明を扱うように確率的ホーア論理を拡張
し、CPA 安全な公開鍵暗号スキームとある特定の健全性(weak
simulation-soundness)をもつ適応的非対話ゼロ知識証明系から
構成される CCA 安全公開鍵暗号スキームの安全性を形式化する。
-------------------------------------------------------
CryptoVerif の証明能力の改良：誤った判定の回避
○花谷 嘉一 ((株)東芝 研究開発センター)
角野 陽輔 (電気通信大学)
米山 一樹 (電気通信大学)
太田 和夫 (電気通信大学)
[講演概要]
CSS 2008 において，CryptoVerif は安全性が成立しない状況
で安全であると判定し誤った証明を行う場合があることが指摘
された．誤った判定の原因として，otheruses 関数の使い方に
あるのではないかと推測されている．本発表では，otheruses
関数の処理内容を詳細に解析する．そして，誤った証明を行う
原因を特定し，その回避法を議論する．
-------------------------------------------------------
暗号学的に安全な擬似乱数生成器の正しい実装に向けて
○山田 聖 (産業技術総合研究所・情報セキュリティ研究センター)
David NOWAK(ダヴィッド ノヴァック)
(産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
現在，我々は，暗号論的疑似乱数生成器 Blum Blum Shub を ア
センブリ言語で実装し，その正しさ，すなわち生成列の予測不可
能性の形式的証明を進めている．我々は既に，Saabas と
Uustalu により示された，アセンブリ言語に対する合成可能な
big-step セマンティクス[1]とプロパティを定理証明支援機 coq
を用いて形式化した．現在，それに基づき Blum Blum Shub の実
装の一部分から，その正しさの証明を始めている．我々の目標は，
このような小さな断片に対する我々のセマンティクスと証明から，
完全な仕様と完全なコードの正しさの証明を得ることである．
[1] A. Saabas and T. Uustalu.
A compositional natural semantics and Hoare logic for low-level languages.
Theor. Comput. Sci., 373:273--302 (2007).
-------------------------------------------------------
最終更新: 2009.3.18
FAISホームページにもどる．