研究発表

学術雑誌論文

• 河辺義信, 真野健, 櫻田英樹, 塚田恭章, 電子投票プロトコルに対する無証拠性の定理証明, 情報処理学会論文誌, Vol. 52, No. 9 (September 2011) 2549-2561. [Online Journal] [CiNii]
  
  あらまし. 電子投票システムの満たすべき性質に，無証拠性が挙げられる．これは匿名性の拡張で，「プロトコルを観測して得られる情報に加えて，別の付加的な情報を投票者が外部に与えたとしても，ある投票パターンと別の(結果が同じとなる)投票パターンが区別できない」という性質である．本稿では，Leeらの電子投票プロトコルを題材とし，その無証拠性を定理証明器で形式的に検証する．
  
  
• 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.
  
  
• 藤田邦彦, 塚田恭章, クリエイティブ・コモンズ利用許諾の形式意味論, 情報処理学会論文誌, Vol. 49, No. 9 (September 2008) 3165-3179. [研究会推薦論文] [Online Journal] [CiNii]
  
  あらまし. 近年のコンテンツ流通環境においては，コンテンツの鑑賞だけでなく，その二次利用や再配信等への要求が高まっている．このような要求を支援するために，ライセンスの付与を容易に行える法的な枠組みを提供するプロジェクトがクリエイティブ・コモンズである．クリエイティブ・コモンズでは，ライセンス付与の条件を利用許諾という文書にまとめているが，自然言語で記述されているため，ライセンス付与に関連する処理の自動化等は困難であった．そこで我々は，利用許諾を多種論理を用いて定式化し，厳密な形式意味論を与えた．これにより，ライセンス付与に関連する処理の自動化や，利用許諾の内容の論理的検証に向けた基礎付けを行うことができた．本論文では，その結果を例を挙げて紹介する．
  
  
• 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.
  
  
• 塚田恭章, 対話型安全性証明つきプログラム配信方式における証明の秘匿とその応用, 情報処理学会論文誌, Vol. 46, No. 1 (January 2005) 236-246. [Online Journal] [MR2124285 (2006b:94057) (Reviewer: Tsuyoshi Takagi)] [CiNii]
  
  あらまし. 悪性プログラムから計算機を守るためプログラム本体とそれが正しく安全に動作することの数学的証明を同時に流通させる方式（Proof-Carrying Code）が近年提案され，電子署名に基づく現行方式より高い安全性を保証する新技術として期待が集まっている．この方式の課題であった証明サイズの爆発の問題も，対話的・確率的手法に基づく効率的な証明検証技法を応用した対話型安全性証明つきプログラム配信方式の適用により対処できる．しかし，証明をそのまま流通させることは証明の盗用や悪用（たとえば証明を利用したリバースエンジニアリングなど）を招く恐れがある．この問題を解決するため，本論文において，安全性証明の存在をゼロ知識対話型プロトコルを利用して保証する方式を提案する．本方式により，証明の盗用・悪用を防ぐことができる．特に，証明の所有者が正規のプログラム開発者に限られるため，証明の所有をプログラム著作権の保持と見なすことも可能となる．すなわち，提案方式は，プログラムの安全性を効率的に検証したいという利用者側の要求とプログラムの著作権を保護したいという開発者側の要求を同時に満たすことができる．
  
  
• 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]

国際会議論文

• 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.
  
  追記. 本仕様記述に基づいた SET 支払いプロトコルの秘 匿性検証は以下の論文で報告されました．
  
  櫻田英樹, SET 支払いプロトコルの秘匿性検証, 情報処理学会論文誌, 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.

編著書・分担執筆

• 塚田恭章, 数理的技法による安全性証明, 太田和夫, 盛合志帆 (編), 電子情報通信学会知識ベース, 1群 3編 (暗号理論) 10章 (August 2010). [電子情報通信学会知識ベース フロントページ]
  
  
• 真野健, 櫻田英樹, 河辺義信, 塚田恭章, ゲーム列による安全性証明の形式化と自動化 −確率Hoare論理と確率プロセス計算によるアプローチ, 萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 日本応用数理学会監修, シリーズ応用数理, 第1巻, 共立出版 (July 2010) pp. 65-86.
  
  
• 萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 日本応用数理学会監修, シリーズ応用数理, 第1巻, 共立出版 (July 2010). (ISBN 978-4-320-01950-8) [出版社のページ]

解説論文

• 塚田恭章, 真野健, 櫻田英樹, フォーマルメソッドによるセキュリティ＆プライバシ, NTT技術ジャーナル, Vol. 23, No. 9 (September 2011) 22-25. [Online Article (PDF)] [CiNii]
  
  あらまし. 電子商取引・電子政府・電子医療などのサービスを提供するICTシステムから，重要な個人情報やプライバシ情報が漏洩しないことを，フォーマルメソッド（形式手法，数理的技法）を用いて厳密に証明する手法について解説します．
  
  
• 真野健, 櫻田英樹, 河辺義信, 塚田恭章, ゲーム列による安全性証明の形式化と自動化, 応用数理, 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.
  
  
• 塚田恭章, 真野健, 河辺義信, 櫻田英樹, 匿名性とプライバシ保護の数理的技法, NTT技術ジャーナル, Vol. 19, No. 6 (June 2007) 38-40. [Online Article (PDF)] [CiNii]
  
  あらまし. 電子投票や電子オークションなどで用いられるセキュリティプロトコルが，匿名性（「誰が」の情報が漏洩しないこと）やプライバシ（「何をした」の情報が漏洩しないこと）に関する要件を正しく実現できているかどうかを，数理論理学・計算機科学の手法を駆使して厳密に検証する技術を紹介します．
  
  
• 塚田恭章, 安全なモバイルプログラム方式の理論, NTT R&D, Vol. 51, No. 10 (October 2002) 765-771. [CiNii]
  
  あらまし. ネットワークの発展に伴い大量のプログラムが流通する時代を迎え，破壊的な外部プログラムから計算機を守る新しい技術が必要になっている．近年，プログラム本体とそれが安全に動作することの数学的証明を同時に流通させる方式が提案され，電子署名に基づく現行技術の問題点を解決した革新的技術として期待が集まっている．しかし，一般に安全性証明はプログラムに比べて巨大になるため，安全性が効率的に検証可能となるプログラムには理論的限界が存在する．この限界を打破するため，証明それ自体を流通させる代わりに簡単な通信により証明の存在を保証する手法を提案する．この手法により，従来方式では指数オーダのサイズとなるメモリ安全性の証明が，効率的に検証可能となることを示す．

学位論文

• Yasuyuki Tsukada, Proof-based Approach to Safe Software Distribution, 東京工業大学大学院情報理工学研究科計算工学専攻博士論文 (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.

その他

• 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]
  
  
• 塚田恭章, 編集にあたって---特集 フォーマルメソッドの新潮流, 情報処理, Vol. 49, No. 5 (May 2008) 491-492. [Online Magazine] [CiNii]
  
  
• 塚田恭章, 「数理的技法による情報セキュリティ」研究部会の紹介, 応用数理, Vol. 17, No. 1 (March 2007) 85-86. [CiNii]