by Professor Kazuhiro Ogata, Japan Advanced Institute of Science and Technology (JAIST)

Abstract:
We use a few simple security protocols to describe how we formally specify security protocols in Maude with the presence of an attacker, where an attacker is formalized as the Dolev-Yao generic intruder model. Maude is a formal specification language as well as a programming language and one direct successor of OBJ3, the well-know algebraic specification language. The Maude system is equipped with model checking facilities: a linear temporal logic (LTL) model checkers and a reachability analyzer (the search command). We use the search command as an invariant model checker. We conduct model checking experiments that security protocols enjoy some security properties. We briefly introduce some advanced topics about security protocol formal verification.

Short bio:
Kazuhiro Ogata received the B.S., M.S., and Ph.D. degrees in engineering from Keio University, in 1990, 1992, and 1995, respectively. He is currently a Professor with the Japan Advanced Institute of Science and Technology (JAIST). He is also the director of Research Center for Advanced Computing Infrastructure, JAIST. His research interests include applications of formal methods to systems, such as distributed systems and security protocols.