I am interested in formal verification of computer programs.
Currently, I am engaged in work on verifying security properties of communication protocols.
|"How can we make communicating programs correct?"|
|"Is this communication protocol really secure? How can we prove it?"|
The use of formal methods, which is a methodology to prove the correctness of various software systems, can give an answer to these questions.
With a formal method, for example, we can prove that a security protocol does not leak private information on the Internet, where we can see that the leakage of private information is due to a "bug" of the protocol.
My research concerns formal verification of security protocols, web services and distributed systems.
The research can be classified into:
- Security verification:
There are services and protocols where anonymity should be provided.
For example, an electronic voting should guarantee to prevent the disclosure of who voted for which candidate.
We are developing a technique to verify anonymity of security protocols.
We proved the anonymity of an e-voting protocol, which is called FOO, with a theorem prover (a proof script is here).
This experiment confirmed that our technique is available for real security protocols.
- Process algebras and network programming languages:
We have developed a programming system named Nepi, which is a distributed implementation of the pi-calculus.
We can describe and analyse communicating processes in the pi-calculus, and we can run the processes with Nepi.
We formally verified the correctness of Nepi language implementation.
In this verification, we employed a theorem prover.
- Order-sorted term rewriting:
Order-sorted term rewriting system, which is an extension of term rewriting with sorts and subsorts, gives a foundation of formal specification languages such as CafeOBJ, CASL and Maude.
We introduced a proof method for confluence and termination of order-sorted rewrite systems, and we employed the method in proving modularity results.
We also introduced currying of order-sorted term rewriting systems, which is a transformation to handle higher-order functions.
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Anonymity, privacy, onymity, and identity: a modal logic approach",
Transactions on Data Privacy, to appear.
- K. Mano, Y. Kawabe, H. Sakurada and Y. Tsukada, "Role interchange for anonymity and privacy of voting",
Journal of Logic and Computation, to appear.
- I. Hasuo, Y. Kawabe and H. Sakurada, "Probabilistic anomymity via coalgebraic simulations",
Theoretical Computer Science, volume 411, No. 22-24, pages 2239-2259, 2010.
- Y. Kawabe, N. Ito and N. Ishii, "On formal modeling of TOPPERS embedded software",
8th International Conference on Software Engineering Research, Management and Applications (SERA '10), pages 93-100. IEEE Computer Society Press, 2010.
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Anonymity, privacy, onymity and identity: a modal logic approach",
IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09), pages 42-51. IEEE Computer Society Press, 2009.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "On backward-style anonymity verification",
IEICE Trans., volume E91-A, No. 9, pages 2597-2606, 2008.
- Y. Kawabe and H. Sakurada, "An adversary model for simulation-based anonymity proof",
IEICE Trans., volume E91-A, No. 4, pages 1112-1120, 2008.
- Y. Kawabe and H. Sakurada, "A formal approach to designing anonymous software",
5th International Conference on Software Engineering Research, Management and Applications (SERA '07), pages 203-212. IEEE Computer Society Press, 2007.
- I. Hasuo and Y. Kawabe, "Probabilistic anomymity via coalgebraic simulations",
16th European Symposium on Programming (ESOP '07), Lecture Notes in Computer Science, volume 4421, pages 379-394. Springer-Verlag, 2007.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "Theorem-proving anonymity of infinite state systems",
Information Processing Letters, volume 101, No. 1, pages 46-51, 2007.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "Backward simulations for anonymity",
6th International IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS '06), pages 206-220.
- Y. Kawabe and K. Mano, "Verifying trace equivalence of a shared-memory-style communication system",
IEICE Trans., volume E88-A, No. 4, pages 915-922, 2005.
- A. Mizuno, K. Mano, Y. Kawabe, H. Kuwabara, S. Yuen and K. Agusa, "Name-passing style GUI programming in the pi-calculus-based network language Nepi",
Electronic Notes in Theoretical Computer Science, volume 139, pages 145-168. Elsevier Science, 2005.
- Y. Kawabe, K. Mano, E. Horita and K. Kogure, "Name creation implements restriction in the pi-calculus",
Systems and Computers in Japan, volume 36, No. 2, pages 78-91, 2005.
- K. Mano and Y. Kawabe, "The Nepi network programming system: a programming environment for distributed systems",
3rd IEEE International Symposium on Network Computing and Applications (NCA '04), pages 287-292. IEEE Computer Society Press, 2004.
Dept. of Information Science,
Aichi Institute of Technology.
1247 Yachigusa Yakusa-Cho
Toyota, 470-0392, JAPAN
Email: kawabe [at] aitech.ac.jp
More Info. (under construction)
- Full list of publications
- How to use a theorem prover
- My hobby
Updated: September 1, 2010