On-the-Fly Model Checking of Security Protocols

Title:On-the-Fly Model Checking of Security Protocols
Speaker:李国强（上海交通大学BASICS实验室）
Time:15:30,Monday，November 30th
Venue:Lecture Room 334,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS

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. etc..