Title：On-the-Fly Model Checking of Security Protocols

Speaker：Guoqiang Li

Time：3:30 pm, Monday, November 30

Venue：Lecture Room,State Key Lab of Computer Science, Level 3 Building #5

Abstract：

Design and analysis of security protocols prove to be a challenging problem over 30 years. Many formalisms have been adopted to describe security protocols, and been analyzed by various automatic and semi-automatic techniques. Due to the complication of the network, methodologies for the analysis should be carefully designed to represent each infinity factor one assumed, such as, an unbounded number of sessions one principal participates, an unbounded number of principals one principal communicates with, and an unbounded number of messages intruders and dishonest principals produce.

This talk introduces a sound and complete model checking method to analyze various security properties under certain assumptions. That is, when flaws are not detected, the protocol is guaranteed to be secure under these assumptions. When various security properties of security protocols are analyzed under different assumptions, infinity factors are abstracted to be finite by several techniques, so that security properties can be checked automatically by a sound and complete on-the-fly model checking under these assumptions, including,

(i) secrecy and authentication properties in bounded sessions,

(ii) authentication property for recursive protocols, and

(iii) non-repudiation and fairness properties in bounded sessions.

Among them, (ii) and (iii) are first analyzed by model checking methods. The methodology is implemented by Maude. By the facility of the reachability analysis in Maude (implemented as search), each property can be checked at the same time when a model is generated.

Biography：

Guoqiang Li is an assistant professor in Shanghai Jiao Tong University. He received M.E. in 2005 from the same University, and Ph.D degree in 2008 from Japan Advanced Institute of Science and Technology. He had also worked in NagoyaUniversity as a PostDoc researcher. His research interests include formal verification, such as model checking and theorem proving, process calculus, and game theory, etc..