Relevant Publications
Journal Papers
- Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada,
Role interchange for anonymity and privacy of voting,
Journal of Logic and Computation
(March 2010).
[DOI:10.1093/logcom/exq013]
Abstract.
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 with known anonymity properties
that are also defined in multiagent systems. Moreover, we
define privacy in a way that is symmetric with anonymity,
and show that exploiting this symmetry is useful for
deriving anonymity and privacy from role
interchangeability. Next we show a way of verifying the
new property. We show that role interchangeability in a
multiagent system is characterized by the existence of
role-interchange functions on the set of traces
corresponding to the system. In addition, a simulation
proof method is presented to prove the existence of the
functions for a protocol described as an automaton.
Finally, as a case study, we apply our method to the
formal verification of the FOO electronic voting protocol.
- Kunihiko Fujita and Yasuyuki Tsukada,
A formal foundation for Creative Commons legal codes
(in Japanese),
IPSJ Journal, Vol. 49, No. 9 (September 2008) 3165-3179.
[Online Journal]
Abstract.
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 providing easier. Creative
Commons supplies the condition of license providing as the
legal codes. They are written, however, in natural
language, so that it will cost expensive and be difficult
to automate processes related to license providing. In
this paper, we provide a formal semantics for them by
using many-sorted first-order logic. This will enable us
to verify the logical consistency of the legal codes and
automate processes related to license providing.
- Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada,
On backward-style anonymity verification,
IEICE Transactions on Fundamentals of Electronics,
Communications and Computer Sciences,
Vol. E91-A, No. 9 (September 2008) 2597-2606.
[DOI:10.1093/ietfec/e91-a.9.2597]
[JOI:JST.JSTAGE/transfun/E91.A.2597]
Abstract. 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 formulation of
anonymity by Schneider and Sidiropoulos, this paper
presents an inductive method based on backward anonymous
simulations. We show that the existence of an image-finite
backward anonymous simulation implies trace anonymity. We
also demonstrate the anonymity verification of an e-voting
protocol (the FOO protocol) with our backward anonymous
simulation technique. When proving the trace anonymity,
this paper employs a computer-assisted verification tool
based on a theorem prover.
- Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada,
Theorem-proving anonymity of infinite-state systems,
Information Processing Letters, Vol. 101, Issue 1 (January 2007) 46-51.
[DOI:10.1016/j.ipl.2006.06.016]
Abstract. 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 by Schneider and Sidiropoulos to
devise the concept of trace anonymity, which is
defined with the set of traces of an I/O-automaton. Then,
we introduce a proof technique with an anonymous
simulation, which is an inductive method for proving
trace anonymity. We show the existence of an anonymous
simulation implies trace anonymity. We also demonstrate
theorem-proving anonymity for an infinite-state system.
- Yasuyuki Tsukada,
Proof hiding in interactive proof-carrying code and its applications
(in Japanese),
IPSJ Journal, Vol. 46, No. 1 (January 2005) 236-246.
[Online Journal]
[MR2124285 (2006b:94057) (Reviewer: Tsuyoshi Takagi)]
[CiNii]
Abstract. 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 complex and often larger than the
codes themselves and hence proof checking would be an
intractable task for each code consumer. This problem was
solved by extending the simple certification mechanism of
PCC to make it interactive and probabilistic. Another
problem is that safety proofs are open and can be used by stealth.
To solve this problem, the present paper proposes the use
of zero-knowledge protocols, with which proofs in the
interactive and probabilistic extension of PCC can be hidden. The
proposed mechanism is shown to have a potential
application to the proofs-as-copyrights interpretation. In
other words, the proposed mechanism has an advantage in
that it not only efficiently ensures ``safety'' (which is
requested from the code consumer's side) but also
guarantees ``copyright'' (which is important for the code
producer's side) at the same time.
- Yasuyuki Tsukada,
Interactive and probabilistic proof of mobile code safety,
Automated Software Engineering, Vol. 12, No. 2 (April 2005) 237-257.
[DOI:10.1007/s10515-005-6207-9]
Abstract. 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 interactive
proof-carrying code (iPCC). With iPCC, a code
consumer is convinced, with overwhelming probability, of
the existence and validity of a safety proof of a
transmitted code through interaction with a code producer.
The iPCC mechanism theoretically solves the problem of
proof explosion with PCC and can be used to efficiently
prove a greater variety of safety properties that may
require longer proofs. Technically, the class (PSPACE) of
safety properties that are efficiently provable by iPCC is
larger than the class (NP) efficiently provable by PCC.
To illustrate the power of iPCC, this paper demonstrates
that the verification of certain basic safety properties
of typical machine instruction codes needs co-NP-complete
computation, and shows how these safety properties can be
efficiently verified by the iPCC mechanism.
- Yasuyuki Tsukada,
Martin-Löf's type theory as an open-ended framework,
International Journal of Foundations of Computer Science,
Vol. 12, No. 1 (February 2001) 31-67.
[DOI:10.1142/S0129054101000400]
[MR1814284 (2002h:03014) (Reviewer: Peter G. Hancock)]
Abstract. 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) persistently valid inference rules.
The class of expression systems is introduced here
to define an open-ended body of languages underlying the
theory. Each expression system consists of two parts: the
computational part is a structured lazy evaluation system
with a bisimulation-like program equivalence; the
structural part is a system of strictly positive inductive
definitions for type constructors in terms of partial
equivalence relations. Types and their objects are
uniformly and inductively constructed from a given
expression system as a type system, which can
provide a semantics of the theory. Building on these
concepts, this paper presents two main results. First,
all the inference rules of the theory are sound;
that is, they remain valid in every type system built from
an extension of an initial expression system. This result
gives a characterization of the class of types that can be
introduced into the theory. Second, each type system is
complete with respect to the underlying
bisimulation-like program equivalence. This result
provides a useful form of type-free equational reasoning
in the theory.
Errata,
International Journal of Foundations of Computer Science,
Vol. 12, No. 5 (October 2001) 695.
[DOI:10.1142/S0129054101000722]
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 the IJFCS website.
[Corrected Online Version (PDF)]
International Conference Papers
- Kunihiko Fujita, Hiroki Endo, and Yasuyuki Tsukada,
A formal approach to interoperability between licenses for content protection,
in:
Proceedings of the Fourth International Workshop on Security (IWSEC 2009)
(ISBN 978-4-915256-76-9, Information Processing Society of Japan, October 2009)
pp. 81-98. (Short Paper)
Abstract.
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 for formally examining license
interoperability by using many-sorted first-order logic. We show how the
framework can be used to formalize two actual licenses and examine
the interoperability between them. The results show that the framework
reveals the relationship between licenses.
- Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe,
Anonymity, privacy, onymity, and identity: A modal logic approach,
in:
Proceedings of the 2009 IEEE International Conference on
Privacy, Security, Risk and Trust (PASSAT-09)
(IEEE Computer Society Press, August 2009) pp. 42-51.
[DOI:10.1109/CSE.2009.251]
[Slides (PDF)]
Abstract. 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. Intuitively, anonymity means the
property of hiding who performed a certain specific
action, privacy hiding what was performed by a certain
specific agent, onymity disclosing who performed a certain
specific action, and identity disclosing what was
performed by a certain specific agent. Building on
Halpern and O'Neill's work, we provide formal definitions
of these properties and study the logical structure
underlying them. In particular, we show that some weak
forms of anonymity and privacy are compatible with some
weak forms of onymity and identity, respectively. We also
discuss relationships between our definitions and existing
standard terminology, in particular Pfitzmann and Hansen's
consolidated proposal.
- Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada,
Backward simulations for anonymity,
in:
D. Gollmann and J. Jürjens, editors,
Sixth IFIP WG 1.7, GI FoMSESS
Workshop on Issues in the Theory of Security (WITS '06)
(March 2006) pp. 206-220.
Abstract. 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 extension
of the formulation of anonymity by Schneider and
Sidiropoulos, this paper presents an inductive method
based on backward anonymous simulations. We show that the
existence of an image-finite backward anonymous simulation
implies trace anonymity. We also demonstrate the
theorem-proving of the anonymity of an e-voting protocol,
which is called FOO, with the backward anonymous
simulation technique. When proving the trace anonymity, we
employ a formal verification tool called IOA-Toolkit.
- Hideki Sakurada and Yasuyuki Tsukada,
A role-based specification of the SET payment transaction protocol,
in:
B. De Decker, F. Piessens, J. Smits, and E. Van Herreweghen, editors,
Advances in Network and Distributed Systems Security,
IFIP TC11 WG11.4 First Annual Working Conference on Network Security
(Kluwer Academic Publishers, The Netherlands, November 2001) pp. 1-13.
Abstract. 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 Visa and MasterCard.
In our language, a protocol is specified as a collection
of processes. Each process expresses the role of a
participant. In the role-based specification, the
components that a participant sees in a message can be
stated explicitly. This is important in specifying
protocols like that for the SET payment transactions
because in such protocols some message components are
encrypted and invisible to some participants.
We simplify the SET payment transaction protocol into the
exchanges of six messages. Because our future goal is to
formally analyze the security properties that Meadows and
Syverson discussed, we make the simplified protocol
contain the parameters used in their security properties.
And we also refrain from excessive simplification. For
example, we use dual signature in the payment request
message as it is specified in the SET specification books,
while most of the other works do not use it. Our
specification can serve as a starting point for a formal
analysis of the protocol.
Addendum. Based on this specification, the SET
payment transaction protocol has been formally analyzed in
the following paper:
Hideki Sakurada,
Verification of secrecy of the SET payment protocol (in Japanese),
IPSJ Journal, Vol. 44, No. 8 (August 2003) 2106-2116.
[Online Journal]
[CiNii]
- Yasuyuki Tsukada,
Interactive and probabilistic proof of mobile code safety,
in:
Electronic Proceedings of the Second International Conference
on Advances in Infrastructure for Electronic Business, Science, and Education
on the Internet
(ISBN 88-85280-61-7, Scuola Superiore Guglielmo Reiss Romoli, L'Aquila, Italy, August 2001)
Paper No. 120.
Abstract. This paper presents interactive proof-carrying code
(iPCC), an interactive and probabilistic extension of the
proof-carrying code (PCC) mechanism. With iPCC, a code
consumer is convinced, with overwhelming probability, of
the existence and validity of a safety proof of a
transmitted code through interaction with a code producer.
To illustrate the power of iPCC, this paper demonstrates
that the verification of certain basic safety properties
of typical machine instruction codes needs co-NP-complete
computation, and shows how these safety properties can be
efficiently verified by the iPCC mechanism. This
mechanism can also be extended to devise zero-knowledge
proof-carrying code (zkPCC), which has a potential
application to the proofs-as-copyrights interpretation.
- Yasuyuki Tsukada,
Mobile codes with interactive proofs:
An approach to provably safe evolution of distributed software systems,
in: T. Katayama, T. Tamai, and N. Yonezaki, editors,
2000 International Symposium on Principles of Software Evolution
(IEEE Computer Society Press, February 2001)
pp. 23-27.
[DOI:10.1109/ISPSE.2000.913217]
Abstract. 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 code with
interactive proof (CIP). With CIP, a code consumer is
convinced, with overwhelming probability, of the existence
and validity of a safety proof of a transmitted code
through interaction with a code producer. The class of
safety properties that are provable by CIP is larger than
the class provable by PCC, provided that each code
consumer is allowed to spend a reasonable amount of time
on verification. Moreover, CIP can be further extended to
devise code with zero-knowledge interactive proof
(CZKIP). This concept is useful, for example, when the
code producer wants to use the safety proof as a kind of
``copyright'' of the code.
- Yasuyuki Tsukada,
Type-free equational reasoning in the theory of inductively defined types,
in: M. Sato and Y. Toyama, editors,
Third Fuji International Symposium on Functional and Logic Programming
(World Scientific, Singapore, April 1998) pp. 227-246.
[MR1661817 (2000h:03021) (Reviewer: Martin Hofmann)]
Abstract. 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 (programs) and their types
(specifications), we can freely replace redexes with
contracta (and vice versa) instead of restricting
ourselves to using ordinary logical inference rules. This
form of type-free equational reasoning was previously
validated for the part of Martin-Löf's type theory
having a specific collection of type constructors. In the
present paper the range of application is shown to be
extendable to a general class of inductively defined
types. This is proved ``uniformly'' (instead of ``on a
case-by-case basis'') based on the uniform construction of
types.
Review Papers
- Ken Mano, Hideki Sakurada, Yoshinobu Kawabe, and Yasuyuki Tsukada,
Formalization and automation of security proof by sequences of games
(in Japanese),
Bulletin of the Japan Society for Industrial and Applied Mathematics,
Vol. 17, No. 4 (December 2007) 38-46.
[CiNii]
Abstract. 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 symbolic methods such as the
Dolev-Yao model and justify it computationally. The other
is to re-formulate traditional computational arguments in
an appropriate formal system and apply symbolic
methods. The former approach is called indirect while the
latter is called direct. This paper introduces the direct
approach. Three studies on the direct approach are dealt
with here, namely those by Corin and den Hartog, by
Blanchet and Pointcheval, and by Canetti et al. They all
formalize security proofs by sequences of games in
different formal systems. We describe the formal systems
they use, how they formalize probabilistic aspects and
computational intractability assumptions, and the
possibility of obtaining formal security proofs
automatically.
- Yasuyuki Tsukada, Ken Mano, Yoshinobu Kawabe, and Hideki Sakurada,
Formal approach to anonymity and privacy
(in Japanese),
NTT GIJUTU Journal,
Vol. 19, No. 6 (June 2007) 38-40.
[Online Article (PDF)]
[CiNii]
- Yasuyuki Tsukada,
Proof-based approach to mobile code safety
(in Japanese),
NTT R&D,
Vol. 51, No. 10 (October 2002) 765-771.
[CiNii]
Abstract. 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 unreliable and possibly malicious foreign
programs transmitted by untrusted hosts. Proof-carrying
code (PCC) is a promising new mechanism that guarantees a
higher level of mobile code safety than the cryptographic
code signing mechanism. There is, however, a practical
problem with PCC. That is, the safety proof carried by a
code is inherently complex and often larger than the code
itself. This paper presents an interactive and
probabilistic extension of PCC and demonstrates that it
solves the problem of proof explosion with PCC.
Thesis
- Yasuyuki Tsukada,
Proof-based Approach to Safe Software Distribution,
Ph.D. Thesis,
Department of Computer Science, Tokyo Institute of Technology
(March 2006).
Abstract.
With the recent advances in 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 unreliable and possibly malicious foreign
programs transmitted by untrusted hosts. How can we
produce, transmit, and execute only those programs that
can be proven to be safe? This question motivates the
study of the framework of provably safe software
distribution---the theme of this thesis.
This framework can be divided into the three main phases.
The first phase concerns the production of correct and
safe source programs from specifications including safety
policies, the second the compilation of programs with
their safety proofs into native machine codes (or
architecture-neutral virtual machine codes) with their
corresponding safety proofs, and the third the
transmission of machine codes with their lengthy safety
proofs in a feasible manner, or in other words, a method
of efficiently convincing each code consumer of the safety
of machine codes.
This framework provides several explicit advantages over
existing technologies; however, it is faced with the
problem of logical and computational complexity arising
from the heavy use of the concept of proofs. The aim of
this thesis is to contribute to our understanding of how
this complexity can be handled. In particular, this thesis
addresses, from a theoretical viewpoint, issues concerning
the first and third phases of the framework, that is,
issues concerning proof generation for source programs and
proof checking for machine codes.
Type theories play a central role in the first phase
because they provide a theoretical basis for developing
programs and their proofs. Since program development with
proofs involves more complex and intricate inferences than
ordinary programming without proofs, some helpful
mechanisms are desired for type theories. Based on the
view that programs and proofs are always enhanced by
continual modification of their parts, this thesis
proposes a new mechanism for supporting this dynamic
aspect of program and proof development. Specifically,
this thesis treats Martin-Löf's type theory as an
example of a type theory and shows that the following form
of inference is valid in the theory
(improvement-evolution theorem): if the correctness
of program f is guaranteed by proof p in
language L and if program f' and proof
p' are obtained in language L'---an
extension or evolution from
L---by improving f and p,
respectively, then the correctness of program f' is
guaranteed by proof p' in language L'. This
form of inference is shown to be useful for developing
programs and proofs that are continually improved in a
series of evolved languages.
On the other hand, proofs of correctness or safety are
inherently complex and large. In fact, one of the
significant problems with the third phase concerning code
transmission is that safety proofs can be exponentially
large with respect to codes themselves. This means that
if each code consumer is allowed to spend only a
reasonable amount of time on verification, the standard
proof-carrying code (PCC) mechanism can be applied only to
codes that are equipped with reasonably short safety
proofs. This thesis addresses this problem and proposes a
theoretical solution to it. Specifically, this thesis
extends the simple certification mechanism of PCC to make
it interactive and probabilistic, thereby devising
interactive proof-carrying code (iPCC). The iPCC
mechanism theoretically solves the problem of proof
explosion with PCC and can be used to efficiently prove a
greater variety of safety properties that may require
longer proofs. To illustrate the power of iPCC, this
thesis demonstrates that the verification of certain basic
safety properties of typical machine instruction codes
needs co-NP-complete computation, and shows how these
safety properties can be efficiently verified by the iPCC
mechanism. This thesis also presents an extension of
iPCC, zero-knowledge proof-carrying code (zkPCC).
This extension enables us to prevent malicious users from
tampering with codes based on proof information. In
addition, the zkPCC mechanism is shown to have a potential
application to the proofs-as-copyrights interpretation; in
other words, it has an advantage in that it not only
efficiently ensures ``safety'' (which is requested from
the code consumer's side) but also guarantees
``copyright'' (which is important for the code producer's
side) at the same time.
Miscellaneous Notes
Yasuyuki Tsukada