
@Braga, Portugal 


Yoshinobu Kawabe 

Welcome!
I am interested in formal verification of computer programs.
Currently, I am engaged in work on verifying security properties of communication protocols.


Research Interests
"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 evoting 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 picalculus.
We can describe and analyse communicating processes in the picalculus, 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.
 Ordersorted term rewriting:
Ordersorted 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 ordersorted rewrite systems, and we employed the method in proving modularity results.
We also introduced currying of ordersorted term rewriting systems, which is a transformation to handle higherorder functions.
Recent Publications
 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. 2224, pages 22392259, 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 93100. 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 (PASSAT09), pages 4251. IEEE Computer Society Press, 2009.
 Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "On backwardstyle anonymity verification",
IEICE Trans., volume E91A, No. 9, pages 25972606, 2008.
 Y. Kawabe and H. Sakurada, "An adversary model for simulationbased anonymity proof",
IEICE Trans., volume E91A, No. 4, pages 11121120, 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 203212. 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 379394. SpringerVerlag, 2007.
 Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "Theoremproving anonymity of infinite state systems",
Information Processing Letters, volume 101, No. 1, pages 4651, 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 206220.
 Y. Kawabe and K. Mano, "Verifying trace equivalence of a sharedmemorystyle communication system",
IEICE Trans., volume E88A, No. 4, pages 915922, 2005.
 A. Mizuno, K. Mano, Y. Kawabe, H. Kuwabara, S. Yuen and K. Agusa, "Namepassing style GUI programming in the picalculusbased network language Nepi",
Electronic Notes in Theoretical Computer Science, volume 139, pages 145168. Elsevier Science, 2005.
 Y. Kawabe, K. Mano, E. Horita and K. Kogure, "Name creation implements restriction in the picalculus",
Systems and Computers in Japan, volume 36, No. 2, pages 7891, 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 287292. IEEE Computer Society Press, 2004.
Contact Address
Dept. of Information Science,
Aichi Institute of Technology.
1247 Yachigusa YakusaCho
Toyota, 4700392, 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