日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2009年度年会FAISオーガナイズド・セッション
日本応用数理学会2009年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2009年度年会が 2009.9.28(月)〜2009.9.30(水) に大阪大学
豊中キャンパスにて開催されます. 「数理的技法による情報セキュリティ」
(FAIS)研究部会も, 下記の日程でオーガナイズド・セッション(OS)を開催いた
します. 奮ってご参加下さいますようお願い申し上げます.
[年会 ホームページ]
http://www.jsiam.org/modules/eguide01/event.php?eid=47
[FAIS 研究部会ホームページ]
http://fais.jsiam.org/
【日時】
2009年9月28日(月) 14:10--17:00
【会場】
大阪大学 豊中キャンパス
【参加方法】
年会ホームページをご覧ください.
参加費割引期間は9月4日(金)までです(延長しました).
【プログラム】(○: 登壇者)
座長: 藤原 融 (大阪大学 大学院情報科学研究科)
14:10--15:10 (60分)
[OS 特別講演] 暗号プロトコル制度の視点から数理的技法研究に期待すること
○大塚 玲 (産業技術総合研究所 情報セキュリティ研究センター)
○松尾 真一郎 (独立行政法人 情報通信研究機構(NICT))
○宮崎 邦彦 (株式会社日立製作所システム開発研究所)
講演資料
座長: 竹内 泉 (産業技術総合研究所 情報技術研究部門)
15:10--15:30 (20分)
汎用的結合可能な安全性の形式的検証のための pattern 拡張に関する一考察
○鈴木 斎輝 (大阪大学 大学院情報科学研究科)
吉田 真紀 (大阪大学 大学院情報科学研究科)
藤原 融 (大阪大学 大学院情報科学研究科)
講演資料
15:30--15:40 (10分) 休憩
15:40--16:00 (20分)
非有界個のセッションの下で計算論的に健全な記号的匿名性
Hubert Comon-Lundh (ENS Cachan)
萩谷 昌己 (東京大学 大学院情報理工学系研究科)
○川本 裕輔 (東京大学 大学院情報理工学系研究科, 日本学術振興会特別研究員)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
講演資料
16:00--16:20 (20分)
形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証: BBS の事例
○Reynald Affeldt (レナルド・アフェルト)
(産業技術総合研究所 情報セキュリティ研究センター)
David Nowak (ダヴィッド・ノヴァック)
(産業技術総合研究所 情報セキュリティ研究センター)
山田 聖 (産業技術総合研究所 情報セキュリティ研究センター)
講演資料
16:20--16:40 (20分)
量子計算のための Hoare 論理
○角谷 良彦 (東京大学 大学院情報理工学系研究科)
講演資料
16:40--17:00 (20分)
CSF, FCC'09 参加報告
○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
講演資料
講演の概要については下記をご覧下さい.
都合によりプログラムが変更になる可能性があります.
最新情報は FAIS 研究部会のホームページでご確認ください.
【問い合わせ先】
塚田 恭章 (NTTコミュニケーション科学基礎研究所)
tsukada(at)theory.brl.ntt.co.jp
【備考】
FAIS OS での発表論文には, 電子ジャーナル JSIAM Letters 誌への投稿
機会が与えられます. ただし, 投稿資格は会員に限ります.
詳しくは JSIAM Letters 誌のホームページをご参照ください.
[JSIAM Letters ホームページ]
http://jsiam.amp.i.kyoto-u.ac.jp/letters/
【重要な日程】
2009年9月4日(金) 参加登録(事前支払い)締切(延長しました)
【講演概要】
--------------------------------------------------------------------
[OS 特別講演] 暗号プロトコル制度の視点から数理的技法研究に期待すること
○大塚 玲 (産業技術総合研究所 情報セキュリティ研究センター)
○松尾 真一郎 (独立行政法人 情報通信研究機構(NICT))
○宮崎 邦彦 (株式会社日立製作所システム開発研究所)
[講演概要]
電子政府推奨暗号の安全性を評価するプロジェクトである CRYPTREC
(Cryptography Research and Evaluation Committees)と，国際標準化
ISO/IEC 29128 (Verification of Cryptographic Protocols) の現状と動
向を紹介し，数理的技法研究への期待を述べる．
--------------------------------------------------------------------
汎用的結合可能な安全性の形式的検証のための pattern 拡張に関する一考察
○鈴木 斎輝 (大阪大学 大学院情報科学研究科)
吉田 真紀 (大阪大学 大学院情報科学研究科)
藤原 融 (大阪大学 大学院情報科学研究科)
[講演概要]
近年, 汎用的結合可能な安全性を記号的手法を用いて形式的に検証する
研究が行われている. 形式的検証の際には, 汎用的結合可能性の枠組みに
おける暗号文などの値が記号的表現に対応付けられる. その際, 環境が識
別不可能な2 つの値を同じ記号的表現へ対応付けるために, 関数 pattern
が定義される. これまでに, 暗号機能として, 公開鍵暗号とディジタル
署名を用いたプロトコルを検証するための pattern が定義されている.
多様なプロトコルの汎用的結合可能な安全性を検証するためには, プロ
トコルが利用する暗号機能に応じた pattern を定義する必要がある. そ
こで, 本発表では, 検証対象の拡張を容易にするために, pattern の定義
方針について考察する.
--------------------------------------------------------------------
非有界個のセッションの下で計算論的に健全な記号的匿名性
Hubert Comon-Lundh(ENS Cachan)
萩谷 昌己 (東京大学 大学院情報理工学系研究科)
○川本 裕輔 (東京大学 大学院情報理工学系研究科, 日本学術振興会特別研究員)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
[講演概要]
公開鍵暗号とリング署名を扱える applied pi-calculus を提案し，その
計算論的健全性，すなわち二つのプロセスが観測同値であるとき，能動的
攻撃者の下で計算量的に識別不能であることを示す．その際，非有界個の
セッションやメッセージの長さを記号的に扱うために，Comon-Lundh と
Cortier の枠組みを改良する．また，計算論的健全性の証明では，ビット
列を受け取り記号的表現を返す多項式時間計算可能パーズ関数を用いない
新たな手法を導入する．この手法は，ハッシュ関数や排他的論理和など，
BPW モデルで扱えない暗号プリミティブに対する計算論的に健全な記号モ
デルを得る上で有用だと考えられる．
--------------------------------------------------------------------
形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証: BBS の事例
○Reynald Affeldt (レナルド・アフェルト)
(産業技術総合研究所 情報セキュリティ研究センター)
David Nowak (ダヴィッド・ノヴァック)
(産業技術総合研究所 情報セキュリティ研究センター)
山田 聖 (産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
機密情報を扱う組込みシステムの普及に伴い，低レベルプログラムの安全
性の保証に対する重要性が高まっている．しかし暗号研究者らによる安全
性証明の対象はアルゴリズムであり，実際に動作するプログラムではない．
アセンブリ言語で実装された暗号プリミティブの安全性を保証するための，
暗号学的安全性証明の拡張方法を提案する．我々のアプローチは，証明可
能安全性のゲーム列による証明に，アセンブリプログラムの正しさの証明
を統合した，定理証明支援系 Coq 上に構成されたフレームワークに基づ
く．このアプローチの有効性を示すために，Blum-Blum-Shub 疑似乱数生
成器の，スマートカード用の MIPS アーキテクチャによる実装の，暗号学
的安全性の証明を行った．
--------------------------------------------------------------------
量子計算のための Hoare 論理
○角谷 良彦 (東京大学 大学院情報理工学系研究科)
[講演概要]
量子計算のプログラムを扱うことのできる Hoare 論理を提案する。この
論理は、確率的プログラムを扱う Hoare 論理の拡張であり、量子的プロ
グラムの確率的な性質を検証することが可能となっている。この論理を使っ
て、実際にいくつかのアルゴリズムを検証する例を紹介したいと思う。
--------------------------------------------------------------------
CSF, FCC'09 参加報告
○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
[講演概要]
CSF'09 (22nd IEEE Computer Security Foundations Symposium) および
その併設ワークショップ FCC'09 (5th Workshop on Formal and
Computational Cryptography) の参加報告を行う．
--------------------------------------------------------------------
最終更新: 2009.10.19
FAISホームページにもどる．