TSUKADA Yasuyuki

J-GLOBAL         Last updated: Sep 22, 2018 at 19:15
 
Avatar
Name
TSUKADA Yasuyuki
E-mail
tsukadakanto-gakuin.ac.jp
URL
http://home.kanto-gakuin.ac.jp/~tsukada/
Affiliation
Kanto Gakuin University
Section
College of Science and Engineering
Job title
Professor
Degree
Ph.D.(Tokyo Institute of Technology), M.S.(Tokyo Institute of Technology)

Profile

I received my B.S. and M.S. degrees in Information Science from the Tokyo Institute of Technology in 1988 and 1990, respectively, under the supervision of Prof. Masako Takahashi-Horai. I also earned my Ph.D. degree in Computer Science from the Tokyo Institute of Technology in 2006 under Prof. Naoki Yonezaki's supervision. From 1990 to 2017, I worked for the Nippon Telegraph and Telephone (NTT) Corporation as a computer science researcher. Currently, I am a Professor of Science and Engineering at the Kanto Gakuin University. My research interests lie broadly in theoretical computer science with a particular emphasis on logic, semantics, and verification. My recent work has focused on formal approaches to security, privacy, and trust. (I am also interested in establishing a semantically self-contained logical theory, which does not need to have interpretations in any other logical theories. This is essentially the same as making computers attribute meanings to symbols by themselves!) I am a member of the Japan Society for Software Science and Technology (JSSST), the Japan Society for Industrial and Applied Mathematics (JSIAM), the Information Processing Society of Japan (IPSJ), and the Association for Computing Machinery (ACM).

Research Areas

 
 

Academic & Professional Experience

 
Apr 1990
 - 
Jan 1999
Information Science Research Laboratory, NTT Basic Research Laboratories
 
Jan 1999
 - 
Mar 2000
Human and Information Science Laboratory, NTT Communication Science Laboratories
 
Apr 2000
 - 
Mar 2009
Senior Research Scientist, Human and Information Science Laboratory, NTT Communication Science Laboratories
 
Apr 2009
 - 
Sep 2010
Senior Research Scientist, Innovative Communication Laboratory, NTT Communication Science Laboratories
 
Sep 2009
 - 
Feb 2016
Part-time Lecturer, Department of Applied Informatics, Faculty of Science and Engineering, Hosei University
 
Oct 2010
 - 
Jun 2014
Senior Research Scientist, Supervisor, Innovative Communication Laboratory, NTT Communication Science Laboratories
 
Jul 2014
 - 
Mar 2017
Senior Research Scientist, Supervisor, Media Information Laboratory, NTT Communication Science Laboratories
 
Apr 2017
 - 
Today
Professor, Networking and Multimedia Course, College of Science and Engineering, Kanto Gakuin University
 
Apr 2018
 - 
Today
Professor, Master's Course in Informatics, Graduate School of Engineering, Kanto Gakuin University
 
Apr 2018
 - 
Today
Professor, Doctoral Course in Interdisciplinary Engineering, Graduate School of Engineering, Kanto Gakuin University
 
Apr 2018
 - 
Today
Chair, Master's Course in Informatics, Graduate School of Engineering, Kanto Gakuin University
 

Education

 
Apr 1984
 - 
Mar 1988
Department of Information Science, Awarded B.S. in Information Science, Faculty of Science, Tokyo Institute of Technology
 
Apr 1988
 - 
Mar 1990
Department of Information Science, Awarded M.S. in Information Science, Graduate School of Science and Technology, Tokyo Institute of Technology
 

Committee Memberships

 
 
   
 
CoSyProofs 2009 (Spring School and Workshop on Computational and Symbolic Proofs of Security)  Member of the organizing committee
 
 
   
 
PASSAT (IEEE/ASE International Conference on Privacy, Security, Risk, and Trust) 2010, 2011, 2012, 2013  Member of the program committee
 
 
   
 
DPM (International Workshop on Data Privacy Management) 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018  Member of the program committee
 
 
   
 
ICISSP (International Conference on Information Systems Security and Privacy) 2015, 2016, 2017, 2018, 2019  Member of the program committee
 

Published Papers

 
Yasuyuki Tsukada, Hideki Sakurada, Ken Mano, and Yoshifumi Manabe
Annals of Mathematics and Artificial Intelligence   78(2) 101-129   Oct 2016   [Refereed]
In this paper, we exploit epistemic logic (or the modal logic of knowledge) for multiagent systems to discuss the compositionality of several privacy-related information-hiding/disclosure properties. The properties considered here are anonymity, p...
Kunihiko Fujita and Yasuyuki Tsukada
IPSJ Journal   55(9) 2081-2091   Sep 2014   [Refereed]
New security and privacy enhancing technologies are demanded in the new information and communication environments where a huge number of computers interact with each other in a distributed and ad hoc manner to access various resources. In this pa...
Kunihiko Fujita and Yasuyuki Tsukada
Computers and Electrical Engineering   38(6) 1670-1686   Nov 2012   [Refereed]
With recent advances in information and telecommunications technologies, a large range of digital content is distributed over the Internet. Whereas diverse licenses are provided to protect the content legally and have the advantage of offering aut...
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
IPSJ Journal   52(9) 2549-2561   Sep 2011   [Refereed]
Receipt-freeness is an important property for an e-voting protocol. This is an extension of anonymity and means that two voting patterns with the same result cannot be distinguishable, even if the voter supplies additional information outside the ...
Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe
Transactions on Data Privacy   3(3) 177-198   Dec 2010   [Refereed]
In this paper, we propose a taxonomy of privacy-related information-hiding/disclosure properties in terms of the modal logic of knowledge for multiagent systems. The properties considered here are anonymity, privacy, onymity, and identity. Intuiti...
Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada
Journal of Logic and Computation   20(6) 1251-1288   Dec 2010   [Refereed]
We propose a new information-hiding property called role interchangeability for the verification of the anonymity and privacy of security protocols. First we formally specify the new property in multiagent systems, and describe its relationship wi...
Kunihiko Fujita and Yasuyuki Tsukada
IPSJ Journal   49(9) 3165-3179   Sep 2008   [Refereed]
Recently, the demands not only for appreciating contents but also for deriving and re-distributing them are increasing in the content distribution environment. To support such demands, Creative Commons offers a legal framework that makes license p...
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences   E91-A(9) 2597-2606   Sep 2008   [Refereed]
Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an extension of the formulati...
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Information Processing Letters   101(1) 46-51   Jan 2007   [Refereed]
This paper presents an inductive method for verifying the anonymity of distributed systems with a theorem prover. We employ an I/O-automaton to describe a distributed, possibly infinite-state, system. We first extend the formulation of anonymity b...
Yasuyuki Tsukada
IPSJ Journal   46(1) 236-246   Jan 2005   [Refereed]
Proof-carrying code (PCC) is a promising new mechanism that can protect computers from unreliable and possibly malicious foreign programs transmitted by untrusted hosts. One problem with PCC is that safety proofs carried by codes are inherently co...
Yasuyuki Tsukada
Automated Software Engineering   12(2) 237-257   Apr 2005   [Refereed]
This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising i...
Yasuyuki Tsukada
International Journal of Foundations of Computer Science   12(1) 31-67   Feb 2001   [Refereed]
This paper treats Martin-Löf's type theory as an open-ended framework composed of (i) flexibly extensible languages into which various forms of objects and types can be incorporated, (ii) their uniform, effectively given semantics, and (iii) persi...
International Journal of Foundations of Computer Science   12(5) 695   Oct 2001
The paper, Martin-Löf's type theory as an open-ended framework, by Yasuyuki Tsukada, published in Vol. 12, No. 1 (2001) 31-67, had several incorrect "=3D" characters scattered throughout the text. A corrected version of this paper will appear on t...
Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Trust Management XI: Proceedings of the 11th IFIP WG 11.11 International Conference on Trust Management (IFIPTM 2017), IFIP Advances in Information and Communication Technology (IFIP AICT) Book Series (Springer)   505 135-151   Jun 2017   [Refereed]
We present a mathematical formulation of a trust metric using a quality and quantity pair. Under a certain assumption, we regard trust as an additive value and define the soundness of a trust computation as not to exceed the total sum. Moreover, w...
Yasuyuki Tsukada, Hideki Sakurada, Ken Mano, and Yoshifumi Manabe
Proceedings of the Fourteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013)   239-248   Jan 2013   [Refereed]
In this paper, we present an epistemic logic approach to the compositionality of several privacy-related information-hiding/disclosure properties. The properties considered here are anonymity, privacy, onymity, and identity. Our initial observatio...
Kunihiko Fujita and Yasuyuki Tsukada
Proceedings of the Tenth Annual ACM Workshop on Digital Rights Management (ACM-DRM 2010)   61-72   Oct 2010   [Refereed]
The emergence of different licenses has led to problems with the smooth flow of digital content across them. To activate digital content distribution, license interoperability must be revealed. In this paper, we present a framework for formally ex...
Kunihiko Fujita and Yasuyuki Tsukada
Proceedings of the Fifth International Workshop on Data Privacy Management (DPM 2010), Lecture Notes in Computer Science (Springer)   6514 140-154   Feb 2011   [Refereed]
New security and privacy enhancing technologies are demanded in the new information and communication environments where a huge number of computers interact with each other in a distributed and ad hoc manner to access various resources. In this pa...
A formal approach to interoperability between licenses for content protection
Kunihiko Fujita, Hiroki Endo, and Yasuyuki Tsukada
Short Papers Proceedings of the Fourth International Workshop on Security (IWSEC 2009) [ISBN 978-4-915256-76-9]   81-98   Oct 2009   [Refereed]
The emergence of different licenses has led to problems with the smooth flow of digital content across different licenses. To activate digital content distribution, license interoperability must be revealed. In this paper, we present a framework f...
Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe
Proceedings of the 2009 IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09) (IEEE Computer Society Press)   42-51   Aug 2009   [Refereed]
In this paper, we propose a taxonomy of privacy-related information-hiding/disclosure properties in terms of the modal logic of knowledge for multiagent systems. The properties considered here are anonymity, privacy, onymity, and identity. Intuiti...
Backward simulations for anonymity
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Sixth IFIP WG 1.7, GI FoMSESS Workshop on Issues in the Theory of Security (WITS '06)   206-220   Mar 2006   [Refereed]
There are many services and protocols on the Internet where anonymity should be provided. For example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an e...
A role-based specification of the SET payment transaction protocol
Hideki Sakurada and Yasuyuki Tsukada
Advances in Network and Distributed Systems Security, IFIP TC11 WG11.4 First Annual Working Conference on Network Security (Kluwer Academic Publishers)   1-13   Nov 2001   [Refereed]
In this paper, we define a language for specifying security protocols concisely and unambiguously. We use this language to formally specify the protocol for payment transactions in Secure Electronic Transaction (SET), which has been developed by V...
Yasuyuki Tsukada
2000 International Symposium on Principles of Software Evolution (IEEE Computer Society Press)   23-27   Feb 2001   [Refereed]
This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising c...
Type-free equational reasoning in the theory of inductively defined types
Yasuyuki Tsukada
Third Fuji International Symposium on Functional and Logic Programming (World Scientific)   227-246   Apr 1998   [Refereed]
In this paper the semantics of inductively defined types in terms of partial equivalence relations is shown to be complete with respect to a coinductively defined, bisimulation-like program equivalence. Using this result in reasoning about objects...

Books etc

 
Information security by formal methods (in Japanese) [K. Ohta and S. Moriai, editors, IEICE Knowledge-Base, Group 1, Part 3 (Cryptography)]
Yasuyuki Tsukada (Part:Contributor, Chapter 10)
IEICE   Aug 2010   
Formal Approach to Information Security (in Japanese), Industrial and Applied Mathematics Series, Vol. 1
Masami Hagiya and Yasuyuki Tsukada, editors (Part:Joint Editor)
Kyoritsu Shuppan   Jul 2010   ISBN:978-4-320-01950-8
Formalization and automation of security proof by sequences of games (in Japanese) [M. Hagiya and Y. Tsukada, editors, Formal Approach to Information Security, Industrial and Applied Mathematics Series, Vol. 1]
Ken Mano, Hideki Sakurada, Yoshinobu Kawabe, and Yasuyuki Tsukada (Part:Contributor, Chapter 4 (pp. 65-86))
Kyoritsu Shuppan   Jul 2010   

Misc

 
Kunihiko Fujita and Yasuyuki Tsukada
Business Review, Faculty of Business Administration, Bunkyo Gakuin University   26(1) 13-21   Dec 2016
In this study, we propose an access control model in which patients license medical information for healthcare providers. In our model, appropriate settings of access rights to medical information are formulated as corresponding license interopera...
Yasuyuki Tsukada, Ken Mano, and Hideki Sakurada
NTT GIJUTU Journal   23(9) 22-25   Sep 2011
Ken Mano, Hideki Sakurada, Yoshinobu Kawabe, and Yasuyuki Tsukada
Bulletin of the Japan Society for Industrial and Applied Mathematics   17(4) 38-46   Dec 2007
Recently extensive research has been undertaken on the computational foundations of symbolic proof methods for security protocols. There are two approaches to providing such foundations. One is to give a probabilistic re-interpretation to existing...
Yasuyuki Tsukada, Ken Mano, Yoshinobu Kawabe, and Hideki Sakurada
NTT GIJUTU Journal   19(6) 38-40   Jun 2007
Proof-based approach to mobile code safety (in Japanese)
Yasuyuki Tsukada
NTT R&D   51(10) 765-771   Oct 2002
With the recent development of network computing, it has become quite common for a program produced by one host to be sent to and executed by others. This situation has created a demand for new technologies that can protect computers from unreliab...
Yasuyuki Tsukada
Bulletin of the Japan Society for Industrial and Applied Mathematics   24(2) 1   Jun 2014
Akiko Orita, Ken Mano, and Yasuyuki Tsukada
A terminology for talking about privacy by data minimization: Anonymity, Unlinkability, Undetectability, Unobservability, Pseudonymity, and Identity Management, Version v0.34   74-78   Aug 2010
Yasuyuki Tsukada
IPSJ Magazine   49(5) 491-492   May 2008
Yasuyuki Tsukada
Bulletin of the Japan Society for Industrial and Applied Mathematics   17(1) 85-86   Mar 2007

Conference Activities & Talks

 
Many-Valued Extension of Trust using Pair of Quality and Quantity (in Japanese)
Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Proceedings of the Computer Security Symposium 2016 (Information Processing Society of Japan), Vol. 2016, No. 2, pp. 1153-1160   Oct 2016   
In CSS2015, we presented a formulation of a trust and its composition operators using a pair of quality and quantity, and proved their basic properties. We also proposed a trust computation protocol, and proved its correctness using the properties...
Formulation of Trust using Pair of Quality and Quantity (in Japanese)
Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Proceedings of the Computer Security Symposium 2015 (Information Processing Society of Japan), Vol. 2015, No. 3, pp. 755-762   Oct 2015   
We present a mathematical formulation of a trust using a pair of quality and quantity. Under a certain assumption, we regard a trust as an additive value and define the soundness of trust computation as not to exceed the summation. Moreover, we po...