NTT Communication Science Laboratories Innovative Communication Laboratory Computing Theory Research Group
English Japanese
home
NTT Communication Science Laboratories
Media Information Laboratory
Innovative Communication Laboratory
Learning and Intelligent Systems Research Group
Linguistic Intelligence Research Group
Computing theory research Group
Human and Information Science Laboratory
Moriya Research Laboratory
NTT
NTT Science and Core Technology Laboratory Group
 
Home / Dependable and Secure Computing

Dependable and Secure Computing

Dependable and secure computing research aims at formal security verification of cryptographic protocols and a theoretical foundation of fault-tolerant and secure protocols.

Research Topics

Formal Approach to Anonymity and Privacy

One of the formal definitions of the anonymity of a communications system is that a certain participant's specific action can be ``simulated'' by another arbitrary participant's corresponding action. Building on this definition, we have proposed an inductive method of proving anonymity, which can be applied to a system with an unbounded number of participants. We have also extended the proof method so that probabilistic anonymity can also be treated. To obtain this extension, we have fully exploited a generic, coalgebraic theory of traces and simulations.

Furthermore, we have discussed anonymity and privacy in terms of a new fundamental concept called role interchangeability, which can be defined in an epistemic logic. More specifically, we have treated privacy as a kind of ``dual'' of anonymity and have shown that exploiting this duality is useful for deriving anonymity and privacy from role interchangeability. We have also devised a method of proving role interchangeability, thereby demonstrating the anonymity and privacy of the FOO (Fujioka, Okamoto, and Ohta) electronic voting protocol.

Computationally Sound Formal Analysis of Cryptographic Protocols

The security of cryptographic protocols has become indispensable in modern network society. To analyze cryptographic protocols, researchers have developed two approaches: formal and computational. The formal approach is based on a symbolic (Dolev-Yao) model of protocol executions, where cryptographic primitives are treated as black boxes. With this approach, security proofs are simplified significantly and can often be automated; however, the guarantees that this approach provides with respect to a deployed protocol have been rather unclear. The computational approach is based on a computational (complexity-theoretic) model where adversaries are treated as probabilistic polynomial-time interactive Turing machines. This approach captures a strong concept of security; however, proofs in this model are rather complicated and less successful for complex protocols.

Recently, the relationship between the symbolic model and the computational model has been being actively investigated. For example, in some cases the symbolic analysis is shown to be ``sound'' with respect to the computational model. We have so far provided computational soundness results for various cryptographic primitives. These include symbolic blind signatures, rerandomizations, ring signatures, and zero-knowledge proofs. We expect that our efforts will lead to a computationally sound framework of automated security analysis for complex cryptographic protocols.

Formal Foundations for Digital Rights Management (DRM)

With the spread of information and communications technology, the convenience of using composed electronic works such as music and animations has improved rapidly. Therefore, the importance of DRM technology, which seeks to protect the rights of creators without ruining the convenience of digital contents, is growing. Our research objectives are to verify that the function provided by DRM is compatible with a creator's intention and to precisely define the function DRM should have by using formal methods.

We have investigated licenses for content that is redistributed, used, and modified by many users on the Internet. More specifically, we have formalized the legal codes of the Creative Commons (CC) licenses using many-sorted first-order predicate logic. The CC licenses are widely used for content such as documents, movies, and songs on blogs and movie-sharing sites. Toward the automatic processing of CC licenses, we have also provided an algorithm to verify that given operations, such as content redistribution and modification, are allowed under a CC license.

Network Algorithm Theory and Graph Theory

We are conducting research to develop new algorithms for secure and fault-tolerant networks using cryptography, distributed algorithms, and game theory.

As another research field, we are examining various kinds of graph layouts as theoretical models of graph networks. We are now studying stack,queue, and track layout problems of graphs.

Publications

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).
  • 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]
  • Okamoto, T. and Manabe, Y.: Security Proof of Cryptographic Systems Using Universally Composability Theory (in Japanese), IEICE Transactions on Information and Systems, Vol.J92-D, No.5, pp.587-595 (2009). [Invited Paper]
  • 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) NTT Communication Science Laboratories