NTT コミュニケーション科学基礎研究所 協創情報研究部 情報基礎理論研究グループ
Japanese
トップページ
組織
NTT コミュニケーション科学基礎研究所
メディア情報研究部
協創情報研究部
知能創発環境研究グループ
言語知能研究グループ
情報基礎理論研究グループ
人間情報研究部
守谷特別研究室
リンク
NTT
NTT 先端技術総合研究所
 
トップページ / ディペンダブル・セキュアコンピューティング

ディペンダブル・セキュアコンピューティング

ディペンダブル・セキュアコンピューティング理論の研究においては、フォーマルメソッドを用いたセキュリティの論理的検証や耐故障セキュアプロトコルの理論構築を行うことを目標としています。

  • 匿名性・プライバシの高精度検証に向かって
    －数理的技法と暗号理論の融合によるセキュリティ・プロトコルの高精度自動検証－
    NTTコミュニケーション科学基礎研究所 オープンハウス2010テーマ展示. [Web Page]
  • 論理×確率で安心・安全を極める～フォーマルメソッドと暗号理論の融合.
    NTTコミュニケーション科学基礎研究所 オープンハウス×未来想論2009 テーマ展示. [Web Page]
  • フォーマルメソッドの新潮流.
    NTTコミュニケーション科学基礎研究所 オープンハウス×未来想論2008 テーマ展示. [Web Page]

研究トピック

匿名性・プライバシのフォーマルメソッド

インターネット上で投票やショッピングなどのサービスを安心して利用するためには、匿名性やプライバシの十分な確保が不可欠です。そのためには、これらのネットワーク・サービスで用いられる暗号通信プロトコル（セキュリティプロトコル）が、匿名性（「誰が」の情報を漏洩しないこと）やプライバシ（「何をした」の情報を漏洩しないこと）に関する要件を正しく実現できているかどうかを、厳密に検証できるようになっていなければなりません。私たちは、情報システムの正しさや安全性を厳密に検証する技法であるフォーマルメソッド（Formal Methods, 形式手法／数理的技法とも訳されます）を用いて，匿名性とプライバシを厳密に定式化し検証する技術の研究を行なっています。これまでに、FOO（藤岡・岡本・太田によって1992年に考案された、大規模インターネット電子投票プロトコル）の匿名性とプライバシ（誰が誰に投票したかが第三者に漏れないこと）の検証に成功しています。

【関連する解説記事】
  • 塚田恭章, 真野健, 河辺義信, 櫻田英樹:
    匿名性とプライバシ保護の数理的技法. NTT技術ジャーナル, Vol.19, No.6, pp.38-40 (2007). [PDF]
  • 塚田恭章(編): 特集 フォーマルメソッドの新潮流.
    情報処理, Vol.49, No.5, pp.491-543 (2008). [Online Magazine]
  • 真野健: 匿名性とプライバシのためのフォーマルメソッド.
    情報処理, Vol.49, No.5, pp.530-536 (2008). [PDF]（※利用上の注意事項）
  • 【動画】匿名性とプライバシのためのフォーマルメソッド.
    匿名性・プライバシのフォーマルメソッド

フォーマルメソッドによる暗号プロトコルの安全性証明

暗号および暗号プロトコルの研究において、その安全性解析は研究の生命線と言えるものです。従来、安全性解析に対するアプローチは、暗号学者とフォーマルメソッド研究者の間で異なっていました。暗号学者によるアプローチは、根底にある暗号の脆弱性も考慮に入れつつ現実的な解析を行いますが、一般に煩雑なものとなり、しばしば解析に誤りが混入します。これに対してフォーマルメソッドによるアプローチでは、定理証明系やモデル検査系などのツールを用いて、厳密かつ機械的なプロトコル検証を可能にしています。しかしながら、このアプローチは根底にある暗号を理想化しているため、暗号の特徴を利用した攻撃を扱うことができないという欠点がありました。近年、これらふたつのアプローチを融合し、両者の「いいとこどり」を実現する試みが世界的に活性化しています。私たちも、フォーマルメソッドの立場から暗号理論の研究者と協力し、この新しい分野の進展に貢献したいと考えています。フォーマルメソッドの強力な検証技術を活用し、暗号理論に裏付けされたセキュリティを確立することに、積極的に取り組んでいきたいと思っています。

【関連する解説記事】
  • 特集 数理的技法による情報セキュリティ. 応用数理, Vol.17, No.4, pp.6-58 (2007). [Online Journal]
  • 真野健, 櫻田英樹, 河辺義信, 塚田恭章:
    ゲーム列による安全性証明の形式化と自動化. 応用数理, Vol.17, No.4, pp.38-46 (2007). [PDF]
  • 岡本龍明, 真鍋義文:
    汎用的結合可能性による暗号システムの安全性証明. 電子情報通信学会論文誌, Vol.J92-D, No.5, pp.587-595 (2009). [PDF] （※利用上の注意事項）
  • 萩谷昌己, 塚田恭章 (編):
    数理的技法による情報セキュリティ. 日本応用数理学会監修, シリーズ応用数理, 第1巻, 共立出版 (2010). [出版社のページ]
  • 真野健, 櫻田英樹, 河辺義信, 塚田恭章:
    ゲーム列による安全性証明の形式化と自動化 －確率Hoare論理と確率プロセス計算によるアプローチ. 萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 第4章, 共立出版, pp.65-86 (2010).
  • 岡本龍明, 真鍋義文:
    汎用的結合可能性による暗号システムの安全性証明. 萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 第6章, 共立出版, pp.111-136 (2010).
  • 長谷部浩二, 岡田光弘, ゲルゲイ・バナ:
    セキュリティプロトコルの論理的検証法. 萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 第9章, 共立出版, pp.185-202 (2010).
  • 塚田恭章:
    数理的技法による安全性証明. 太田和夫, 盛合志帆 (編), 電子情報通信学会知識ベース, 1群 3編 (暗号理論) 10章 (2010). [電子情報通信学会知識ベース フロントページ]

デジタル著作権管理のフォーマルメソッド

デジタル技術やインターネットの普及に従い、電子化された文章・動画・音楽などの著作物（デジタルコンテンツ）の利用（配布・再利用・改変など）の利便性は飛躍的に高まりました。これに伴い、デジタルコンテンツの利便性を損なうことなく著作者及び著作隣接権者の権利を保護する、DRM（Digital RightsManagement：デジタル著作権管理）技術の重要性も大きくなりつつあります。私たちはフォーマルメソッドを用いて、DRMが意図通りの機能を有していることを検証したり、DRMの有すべき機能とは何かを明確にすることを目標としています。

【関連する解説記事】
  • 藤田邦彦:
    フォーマルメソッドによるセキュリティ (特集 我が国の基礎・基盤研究の現状－NTTコミュニケーション科学基礎研究所－). ITUジャーナル, Vol.38, No.8, pp.22-23 (2008).
  • 藤田邦彦:
    ディジタル著作物の著作権管理とフォーマルメソッド. 電子情報通信学会誌, Vol. 92, No. 10, pp. 866-870 (2009). [PDF] （※利用上の注意事項）

耐故障ネットワークアルゴリズム・グラフ理論

ネットワークの耐故障性および安全性を向上させるアルゴリズムを分散アルゴリズム理論，暗号理論，ゲーム理論等を併用して導出する研究を行っています．また、ネットワークの幾何学的モデルであるグラフを対象として，それを空間に埋め込んだときの特性記述についても研究を行っています．現在は特にスタック・キュー・トラックのグラフレイアウトについて研究を進めています．

研究発表

2011

  • Comon-Lundh, H., Hagiya, M., Kawamoto, Y., Sakurada, H.: Computational Soundness without Symbolic Length Function (Abstract). Seventh Workshop on Formal and Computational Cryptography (FCC 2011) (2011).
  • Yamada, S., Kanno, J., and Miyauchi, M: Multi-sized Sphere Packing in Containers: Optimization Formula for Obtaining the Highest Density with Two Different Sized Spheres. IPSJ Transactions on Mathematical Modeling and Its Applications, Vol.4, No.2, pp.23-30 (2011)

2010

  • Tsukada, Y., Mano, K., Sakurada, H., and Kawabe, Y.: Anonymity, Privacy, Onymity, and Identity: A Modal Logic Approach. Transactions on Data Privacy, Vol.3, No.3, pp.177-198 (2010).
  • Fujita, K. and Tsukada, Y.: An Analysis of Interoperability between Licenses. Proc. of 10th ACM Workshop on Digital Rights Management (ACM-DRM 2010), pp.61-72 (2010).
  • Fujita, K. and Tsukada, Y.: A Notation for Policies using Feature Structures. Proc of 5th International Workshop on Data Privacy Management (DPM 2010), LNCS Vol.6514, pp.140-154 (2010).
  • Zhu, H., Araragi, T., Nishide, T., and Sakurai, K.: Composable Non-committing Encryptions in the Presence of Adaptive Adversaries. Proc. of the 5th International Conference on Security and Cryptography (SECRYPT 2010), pp.389-398, SciTePress (2010).
  • Zhu, H., Araragi, T., Nishide, T., and Sakurai, K.: Composable Non-interactive String-Commitment Protocols. Proc. of the 5th International Conference on Security and Cryptography (SECRYPT 2010), pp.354-361, SciTePress (2010).
  • Zhu, H., Araragi, T., Nishide, T., and Sakurai, K.: Adaptive and Composable Non-committing Encryptions. Proc. of the 15th Australasian Conference on Information Security and Privacy (ACISP 2010), LNCS Vol.6168, pp.135-144 (2010).
  • Mitsunaga, T., Manabe, Y., and Okamoto, T.: Efficient Secure Auction Protocols Based on the Boneh-Goh-Nissim Encryption. Proc. of IWSEC 2010, LNCS Vol.6434, pp.149-163 (2010).
  • Manabe, Y. and Okamoto, T.: Meta-envy-free Cake Cutting Protocols. Proc. of MFCS 2010, LNCS Vol.6281, pp.501-512 (2010).
  • Mitsunaga, T., Manabe, Y., and Okamoto, T.: Insatabity of a punishment strategy in correlated equilibria. Workshop on Algorithmic Game Theory: Dynamics and Convergence in Distributed Systems (AlgoGT 2010) (2010).
  • Hasuo, I., Kawabe, Y., and Sakurada, H.: Probabilistic Anonymity via Coalgebraic Simulations. Theoretical Computer Science, Vol.411 (22-24), pp.2239-2259 (2010).
  • 真野健: プライバシ侵害に係る定義の検討における数理的表現方法の利用 －同定可能性の問題を中心として－. 情報ネットワークローレビュー, Vol.9, No.2, pp.54-66 (2010).
  • Mano, K., Kawabe, Y., Sakurada, H., and Tsukada, Y.: Role Interchange for Anonymity and Privacy of Voting. Journal of Logic and Computation, Vol.20, No.6, pp.1251-1288 (2010).
  • Sakurada, H., Kawamoto, Y., Hagiya, M.: Computational Soundness of Symbolic XOR in the Presence of Active Attacker. Spring School and French-Japanese Collaboration Workshop on Computational and Symbolic Proofs of Security (CoSyProofs 2010) (2010).
  • Comon-Lundh, H., Hagiya, M., Kawamoto, Y., Sakurada, H.: Proving Computational Soundness of the Applied Pi-Calculus without Using Computable Parsing. Spring School and French-Japanese Collaboration Workshop on Computational and Symbolic Proofs of Security (CoSyProofs 2010) (2010).
  • Araragi, T. and Ito, T.: Application of Polynomially Accurate Simulation Relations to a Proof of UC Security: A Case Study of Group Key Exchange. Spring School and French-Japanese Collaboration Workshop on Computational and Symbolic Proofs of Security (CoSyProofs 2010) (2010).

2009

  • Comon-Lundh, H., Hagiya, M., Kawamoto, Y., and Sakurada, H.: Computational and Symbolic Anonymity in an Unbounded Network. Workshop on Formal and Computational Cryptography FCC'09, (2009).
  • Fujita, K., Endo H., and Tsukada, Y.: A Formal Approach to Interoperability between Licenses for Content Protection. Proc. of the 4th International Workshop on Security (IWSEC2009), pp. 81 - 98 (2009).
  • Yamada, S., Kanno, J., and Miyauchi, M.: Multi-Sized Sphere Packing. Proc. of the 7th Japan Conference on Computational Geometry and Graphs (JCCGG2009), pp.55-56 (2009).
  • Tsukada, Y., Mano, K., Sakurada, H., and Kawabe, Y.: Anonymity, Privacy, Onymity, and Identity: A Modal Logic Approach. Proc. of the 2009 IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT'09), IEEE Computer Society, pp.42-51 (2009).
  • Nakamura, J., Araragi, T., and Masuyama, S.: Acceleration of Byzantine Fault Tolerance by Parallelizing Consensuses. The Tenth International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2009), pp.80-87 (2009).
  • Kobayashi, M., Miyauchi, M., Mutoh, N., and Nakamura, G.: Generalization of Hadamard matrices and its applications (アダマール行列 の一般化とその応用), Proc. of Administration and Informatics, University of Shizuoka (静岡県立大学・経営情報学部/研究紀要), Vol.21, No.2, pp.15-27, 2009.
  • Kawamoto, Y., Sakurada, H. and Hagiya, M.: Computationally Sound Formal Rerandomizable Encryption. Special Issue On Computer Security, Lecture Notes in Computer Science, Vol.5458, pp.158-180 (2009).
  • Comon-Lundh, H., Kawamoto, Y., and Sakurada, H.: Computational and Symbolic Anonymity in an Unbounded Network. JSIAM Letters, Vol.1, pp.28-31 (2009). ＜Invited Paper＞
  • 岡本龍明, 真鍋義文: 汎用的結合可能性による暗号システムの安全性証明. 電子情報通信学会論文誌, Vol.J92-D, No.5, pp.587-595 (2009). ＜招待論文＞
  • Bana, G., Kawamoto, Y., and Sakurada, H.: Computational Soundness of (Interactive) Zero-Knowledge Proof Systems in Presence of Active Adversaries. Spring School and French-Japanese Collaboration Workshop on Computational and Symbolic Proofs of Security (CoSyProofs'09) (2009).
  • Comon-Lundh, H., Hagiya, M., Kawamoto, Y., and Sakurada, H.: Computationally Sound Symbolic Analysis of Anonymity in Presence of Active Adversaries. Spring School and French-Japanese Collaboration Workshop on Computational and Symbolic Proofs of Security (CoSyProofs'09) (2009).

利用上の注意事項（電子情報通信学会）

電子情報通信学会論文誌　copyright(C)1984-2009 IEICE [IEICE Transactions Onlne]

利用上の注意事項（情報処理学会）

ここに掲載した著作物の利用に関する注意：本著作物の著作権は（社）情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。
  Copyright (C) NTT Communication Science Laboratories