Relevant Publications

Journal Papers

• Kunihiko Fujita and Yasuyuki Tsukada, An approach to the formal analysis of license interoperability, Computers and Electrical Engineering, Vol. 38, No. 6 (November 2012) 1670-1686. [DOI:10.1016/j.compeleceng.2012.07.003]
  
  Abstract. 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 authors many choices, the obstruction of smooth content distribution may occur if the relationships between licenses are not revealed because of differences between the restrictions imposed by each license. To activate digital content distribution, license interoperability must be revealed. In this paper, we propose a framework for formally examining license interoperability by using many-sorted first-order logic. We formalize five actual licenses and examine their interoperability to prove the effectiveness of our proposed framework. The results show that the framework reveals the relationships between licenses.
  
  
• Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Theorem-proving receipt-freeness of an e-voting protocol (in Japanese), IPSJ Journal, Vol. 52, No. 9 (September 2011) 2549-2561. [Online Journal] [CiNii]
  
  Abstract. 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 scope of the protocol. In this paper, we deal with an e-voting protocol by Lee et al., and we theorem-prove the receipt-freeness of the protocol formally.
  
  
• Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe, Anonymity, privacy, onymity, and identity: A modal logic approach, Transactions on Data Privacy, Vol. 3, Issue 3 (December 2010) 177-198. [Online Journal]
  
  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 involves hiding what was performed by a certain specific agent, onymity refers to disclosing who performed a certain specific action, and identity relates to 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 the relationships between our definitions and existing standard terminology, in particular Pfitzmann and Hansen's consolidated proposal.
  
  
• Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada, Role interchange for anonymity and privacy of voting, Journal of Logic and Computation, Vol. 20, Issue 6 (December 2010) 1251-1288. [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] [CiNii]
  
  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 Version (PDF) on the author's website] [Corrected Version (PDF) on the IJFCS website]

International Conference Papers

• Yasuyuki Tsukada, Hideki Sakurada, Ken Mano, and Yoshifumi Manabe, An epistemic approach to compositional reasoning about anonymity and privacy, in: Burkhard C. Schipper, editor, Proceedings of the Fourteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013) (ISBN 978-0-615-74716-3, January 2013) pp. 239-248. [Online Version (PDF) on the TARK website]
  
  Abstract. 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 observation reveals that anonymity and privacy are not necessarily sequentially compositional; this means that even though a system comprising several sequential phases satisfies a certain unlinkability property in each phase, the entire system does not always enjoy a desired unlinkability property. We show that the compositionality can be guaranteed provided that the phases of the system satisfy what we call the independence assumptions. More specifically, we develop a series of theoretical case studies of what assumptions are sufficient to guarantee the sequential compositionality of various degrees of anonymity, privacy, onymity, and/or identity properties. Similar results for parallel composition are also discussed.
  
  
• Kunihiko Fujita and Yasuyuki Tsukada, An analysis of interoperability between licenses, in: Hongxia Jin and Marc Joye, editors, Proceedings of the Tenth Annual ACM Workshop on Digital Rights Management (ACM-DRM 2010) (ACM, October 2010) pp. 61-72. [DOI:10.1145/1866870.1866884]
  
  Abstract. 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 examining license interoperability by using many-sorted first-order logic. We show how the framework can be used to formalize three actual licenses and examine the interoperability between them. The results show that the framework reveals the relationship between licenses.
  
  
• Kunihiko Fujita and Yasuyuki Tsukada, A notation for policies using feature structures, in: Joaquin Garcia-Alfaro and Guillermo Navarro-Arribas, editors, Proceedings of the Fifth International Workshop on Data Privacy Management (DPM 2010), Lecture Notes in Computer Science, Vol. 6514 (Springer, February 2011) pp. 140-154. [DOI:10.1007/978-3-642-19348-4_11]
  
  Abstract. 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 paper, we focus on access control because this is the underlying core technology to enforce security and privacy. Access control decides permit or deny according to access control policies. Since notations of policies are specialized in each system, it is difficult to ensure consistency of policies that are stated in different notations. In this paper, we propose a readable notation for policies by adopting the concept of feature structures, which has mainly been used for parsing in natural language processing. Our proposed notation is also logically well-founded, which guarantees strict access control decisions, and expressive in that it returns not only a binary value of permit or deny but also various result values through the application of partial order relations of the security risk level. We illustrate the effectiveness of our proposed method using examples from P3P.
  
  
• Kunihiko Fujita, Hiroki Endo, and Yasuyuki Tsukada, A formal approach to interoperability between licenses for content protection, in: Short Papers 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.
  
  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.

Books and Book Chapters

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

Review Papers

• Yasuyuki Tsukada, Ken Mano, and Hideki Sakurada, Formal methods for security and privacy (in Japanese), NTT GIJUTU Journal, Vol. 23, No. 9 (September 2011) 22-25. [Online Article (PDF)] [CiNii]
  
  
• 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

• Akiko Orita, Ken Mano, and Yasuyuki Tsukada, Translation of essential terms to Japanese, in: A. Pfitzmann and M. Hansen, A terminology for talking about privacy by data minimization: Anonymity, Unlinkability, Undetectability, Unobservability, Pseudonymity, and Identity Management, Version v0.34 (August 2010) pp. 74-78. [Anon Terminology Website]
  
  
• Yasuyuki Tsukada, Foreword to the Special Features on New Trends in Formal Methods (in Japanese), IPSJ Magazine, Vol. 49, No. 5 (May 2008) 491-492. [Online Magazine] [CiNii]
  
  
• Yasuyuki Tsukada, Activities of the Special Interest Group on Formal Approach to Information Security (in Japanese), Bulletin of the Japan Society for Industrial and Applied Mathematics, Vol. 17, No. 1 (March 2007) 85-86. [CiNii]