日本応用数理学会2008年度年会
FAIS オーガナイズド・セッション
「数理的技法による情報セキュリティ」
日本応用数理学会2008年度年会が 2008年9月17(水)から9月19日(金)にかけて,
東京大学 柏キャンパスにて開催されます.
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッションを開催いたします.
奮ってご参加下さいますようお願い申し上げます.
[年会ホームページ]
http://www.jsiam.org/modules/eguide01/event.php?eid=39
[FAIS 研究部会ホームページ]
http://fais.jsiam.org/
【日時】
2008年9月18日(木) 11:10〜11:50 および 14:30〜15:50 (午前40分, 午後80分)
【会場】
東京大学 柏キャンパス (千葉県柏市柏の葉 5-1-5)
【参加方法】
年会ホームページをご覧ください.
参加費割引期間は8月18日(月)までです.
【プログラム】(○: 登壇者)
座長: 赤間 陽二 (東北大学 大学院理学研究科)
[午前の部]
11:10--11:30 (20分)
Towards Verification with no False Attack of Security Protocols in
First-order Logic
○Reynald AFFELDT (レナルド・アフェルト)
(産業技術総合研究所 情報セキュリティ研究センター)
Hubert COMON-LUNDH (ウベール・コモン-ルンド)
(産業技術総合研究所 情報セキュリティ研究センター)
11:30--11:50 (20分)
リング署名の計算論的に健全な形式化
○川本 裕輔 (東京大学 大学院情報理工学系研究科)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学 大学院情報理工学系研究科)
[午後の部]
14:30--14:50 (20分)
A Verification Toolbox for Cryptographic Primitives
○David NOWAK (ダヴィッド・ノヴァック)
(産業技術総合研究所 情報セキュリティ研究センター)
<a href="doc/20080918-nowak.pdf">講演資料</a>
14:50--15:10 (20分)
統計的シミュレーション関係の証明能力について
○古田 憲一郎 (東芝研究開発センター)
花谷 嘉一 (東芝研究開発センター)
大熊 建司 (東芝研究開発センター)
村谷 博文 (東芝研究開発センター)
15:10--15:30 (20分)
FCS-ARSPA-WITS, CSF, FCC'08 参加報告---安全性の形式化について
○川本 裕輔 (東京大学 大学院情報理工学系研究科)
Reynald AFFELDT (産業技術総合研究所 情報セキュリティ研究センター)
15:30--15:50 (20分)
FCS-ARSPA-WITS, CSF, FCC'08 参加報告---自動検証と形式的証明について
○Reynald AFFELDT (産業技術総合研究所 情報セキュリティ研究センター)
川本 裕輔 (東京大学 大学院情報理工学系研究科)
講演の概要については下記をご覧下さい.
都合によりプログラムが変更になる可能性があります.
最新情報は FAIS 研究部会のホームページでご確認ください.
【問い合わせ先】
塚田 恭章 (NTTコミュニケーション科学基礎研究所)
tsukada(at)theory.brl.ntt.co.jp
(「数理的技法による情報セキュリティ」セッション オーガナイザ)
【備考】
FAIS オーガナイズド・セッションでの発表論文は, 2009年1月創刊
予定の電子ジャーナル JSIAM Letters 誌への投稿機会が与えられます.
詳しくは JSIAM Letters 誌のホームページをご参照ください.
[JSIAM Letters ホームページ]
http://jsiam.amp.i.kyoto-u.ac.jp/letters/
【講演概要】
--------------------------------------------------------------------
Towards Verification with no False Attack of Security Protocols in
First-order Logic
○Reynald AFFELDT (レナルド・アフェルト)
(産業技術総合研究所 情報セキュリティ研究センター)
Hubert COMON-LUNDH (ウベール・コモン-ルンド)
(産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
It is possible to model security protocols and their properties using
first-order logic. Out of such models, it is even possible to get
automatically security proofs using theorem provers for first-order
logic. Yet, this approach sometimes fails to produce security proofs
despite the correctness of the protocol. This is because of the
detection of false attacks that originate from abstractions made for
the purpose of modeling. We show that we get rid
of some false attacks by using the notion of ``rigid variable'' to model
protocols. Thanks to a simple translation to first-order logic, it
turns out that automatic verification with rigid variables can be
implemented using standard techniques.
--------------------------------------------------------------------
リング署名の計算論的に健全な形式化
○川本 裕輔 (東京大学大学院情報理工学系研究科)
櫻田 英樹 (NTTコミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学大学院情報理工学系研究科)
[講演概要]
リング署名は、グループの中の誰かが署名したことは確認できるが、
実際の署名者を特定できないという匿名性を満たす電子署名である。
本発表では、能動的攻撃者の下でのリング署名の偽造不能性と匿名
性の両方を扱う記号モデルを提案し、このモデルが、偽造不能性と
匿名性に対応する二種類の計算論的健全性を満たすことを述べる。
一つ目の健全性は、計算論的トレースが記号トレースに対応しない
確率が無視できるという性質（マッピング健全性）である。二つ目
の健全性は、記号的に識別不能であるならば計算論的に識別不能で
あるという性質であり、Abadi-Rogaway流の健全性を能動的攻撃者
の場合に拡張したものである。
--------------------------------------------------------------------
A Verification Toolbox for Cryptographic Primitives
○David NOWAK (ダヴィッド・ノヴァック)
(産業技術総合研究所情報セキュリティ研究センター)
[講演概要]
Cryptographic primitives are fundamental components for information
security. In many cases, their security proof consists in showing
that they are reducible to a computational hardness assumption such as
Diffie-Hellman problems or integer factorization. Those reductions
involve various mathematical theories such as probability theory,
number theory or group theory. This does not make proofs easily
checkable. Bellare and Rogaway even claimed in 2004 that ``many
proofs in cryptography have become essentially unverifiable.'' They,
but also Shoup, have argued that game-based proofs might be a remedy.
In 2005, Halevi has advocated the need for a software which can take
care of the mundane part of writing and checking game-based security
proofs. We have followed Halevi by giving a formal semantics to games
(in cryptographers' papers, this is usually either left implicit or,
at best, informally explained in English); by building a framework on
top of the proof assistant Coq; and by applying it to some
cryptographic primitives.
--------------------------------------------------------------------
統計的シミュレーション関係の証明能力について
○古田 憲一郎 (東芝研究開発センター)
花谷 嘉一 (東芝研究開発センター)
大熊 建司 (東芝研究開発センター)
村谷 博文 (東芝研究開発センター)
[講演概要]
タスク PIOA の枠組では, 最終的に示したい Implementation 関
係の確認はシミュレーション関係の確認により行われる場合があ
り, シミュレーション関係成立範囲の拡張は証明適用範囲の拡張
につながる. 本稿では, このような拡張を目指して提案した統計
的シミュレーション関係の有用性を確認するために, 同じ目的で
拡張された近似的シミュレーション関係との比較を行う. 比較の
尺度としては MAP1 の証明において重要な役割を果たしている量
をとる. 近似的関係が恒等関係であるという条件を加えると比較
の尺度とした量がともに negligible 関数となり, MAP1 の証明
に類する証明を行う能力が同じになることが分かる.
--------------------------------------------------------------------
FCS-ARSPA-WITS, CSF, FCC'08 参加報告---安全性の形式化について
○川本 裕輔 (東京大学 大学院情報理工学系研究科)
Reynald AFFELDT (産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
CSF'08 (the 21st IEEE Computer Security Foundations Symposium) is a
major venue where presented results are relevant to the special
interest group JSIAM-FAIS (Formal Approach to Information
Security). In this presentation, we report on CSF'08 and its satellite
workshops FCS-ARSPA-WITS'08 and FCC'08. We focus here on results about
formalization of security properties; results about automated
verification and certification are covered in the next presentation.
Regarding formalization of security properties, we observe that much
work now deals with faithful formalizations in the computational
model. Such formalizations can be direct (giving for example deductive
methods for provable security) or indirect (through so-called
computational soundness results). The more traditional line of
research in the symbolic model is thriving with, for example,
numerous expressiveness enhancements to information-flow security and
authorization logics.
--------------------------------------------------------------------
FCS-ARSPA-WITS, CSF, FCC'08 参加報告---自動検証と形式的証明について
○Reynald AFFELDT (産業技術総合研究所 情報セキュリティ研究センター)
川本 裕輔 (東京大学 大学院情報理工学系研究科)
[講演概要]
CSF'08 (the 21st IEEE Computer Security Foundations Symposium) is a
major venue where presented results are relevant to the special
interest group JSIAM-FAIS (Formal Approach to Information
Security). In this presentation, we report on CSF'08 and its satellite
workshops FCS-ARSPA-WITS'08 and FCC'08. We focus here on results about
automated verification and certification; results about formalization
of security properties are covered in the previous presentation.
Regarding verification of security properties, we observe that much
effort is put on the development of verification frameworks for the
computational model in proof-assistants. This is still work in
progress with very little automation. In contrast, for the symbolic
model in proof-assistants, full automation is demonstrated for
verification of protocols. As for the traditional line of research in
the symbolic model using non-certified tools, it is shown to tackle
realistic use-cases, such as verification of industrial-use APIs or
verification of source code up to hundreds of lines.
--------------------------------------------------------------------
最終更新: 2008.10.21