 |
| @Braga, Portugal |
|
|
Yoshinobu Kawabe |
|
|
Welcome!
I am interested in the formal verification of computer programs.
Currently, I am engaged in trust computations and verifying the security properties of communication protocols.
|
|
Research Interests
| "Are the rescue requests found on the social networking site genuine?" |
| "How can we make communicating programs correct?" |
| "Is this communication protocol secure? How can you explain it?" |
The use of formal methods, which is a methodology to prove the correctness of various software systems, can answer these questions.
Formally, for example, we can confirm that a security protocol does not leak private information on the Internet, where we can see that the leakage of confidential information is due to a "bug" of the protocol.
My research concerns human trust, information security, formal verification of security protocols, and the foundation of computer science.
- Trust computation:
Suppose you found the following messages on social networking services immediately after a disaster.
Which of these is the most urgent "rescue request"?
| "Due to the torrential rain disaster, we will be closed tomorrow." |
| "Please be careful." |
| "We're at 1-2-3 Dokoka-cho, Dokoka-shi. The water's getting higher. Please Help!" |
It is essential to correctly evaluate which messages are "believable as a rescue request" from the vast number of messages exchanged during a disaster to deliver to first responders (firefighters, police officers, etc.).
We are working to develop technology to calculate, infer, and predict trust for messages correctly.
We have developed a new trust representation (called two-dimensional trust value) that incorporates psychology and fuzzy logic results.
We are also developing a technique to verify the properties of trust transitions, such as "never reaching an untrustworthy state" and "becoming trustworthy someday." We believe the verification is possible by applying results in theories of computer programs and distributed algorithms to trust calculations.
- Security and privacy verification:
There are services and protocols where we should provide anonymity.
For example, electronic voting should prevent the disclosure of who voted for which candidate.
We are developing a technique to verify the anonymity of security protocols.
We proved the anonymity of an e-voting protocol called FOO with a theorem prover (a proof script is here).
This experiment confirmed that our technique is available for authentic security protocols.
- Process algebra and network programming language:
We have developed a programming system named Nepi, a distributed implementation of the pi-calculus.
We can describe and analyze communicating processes in the pi-calculus and run the operations 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 sub-sorts, gives a foundation for 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 technique in proving modularity results.
We also introduced the currying of order-sorted term rewriting systems, transforming order-sorted rewrite systems to handle higher-order functions.
Recent Publications
- M. Jahanian, T. Hasegawa, Y. Kawabe, Y. Koizumi, A. Magdy, M. Nishigaki, T. Ohki and K. K. Ramakrishnan, "DiReCT: Disaster Response Coordination with Trusted Volunteers",
6th International Conference on Information and Communication Technologies for Disaster Management, {ICT-DM} 2019, pages 1-8, 2019.
- Y. Kawabe, Y. Koizumi, T. Ohki, M. Nishigaki, T. Hasegawa and T. Oda, "On Trust Confusional, Trust Ignorant, and Trust Transitions",
Trust Management XIII: Proceedings of the 13th IFIP WG 11.11 International Conference on Trust Management (IFIPTM 2019), IFIP Advances in Information and Communication Technology (IFIP AICT) Book Series, pages 178-195. Springer, 2019.
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Theorem-proving Receipt-freeness of an e-voting Protocol" (In Japanese),
IPSJ Journal, volume 52, No. 9, pages 2549-2561, 2011.
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Anonymity, privacy, onymity, and identity: a modal logic approach",
Transactions on Data Privacy, volume 3, No. 3, pages 177-198, 2010.
- K. Mano, Y. Kawabe, H. Sakurada and Y. Tsukada, "Role interchange for anonymity and privacy of voting",
Journal of Logic and Computation, volume 20, No. 6, pages 1251-1288, 2010.
- 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.
Contact Address
Dept. of Information Science,
Aichi Institute of Technology.
1247 Yachigusa Yakusa-Cho
Toyota, 470-0392, JAPAN
Email: kawabe [at] aitech.ac.jp
Updated: May 4, 2022