An Approach To Automatic Security Protocol Analysis Based On Authentication Tests

A security protocol, consisting of two or more participants, is a series of message exchange, in which encryption is used to authenticate participants or to distribute session keys between participants for new conversations.How is a protocol proven correct? It is one of the most complex and error-prone processes in computing.Three decades has passed since the beginning of security protocols studying, there are mainly three methods to analyze them now:BAN-like logic, model checking and theorem proving. Among them, theorem proving is more significant due to its precise semantics and complete rules. Though based on theorem proving, strand space is complex and not suitable to automatically verify the correctness of security protocols. In2000, Guttman and Thayer proposed a simplified theory named authentication tests, which is based on strand space. Due to its simplified rules, it becomes possible to analyze protocol automatically. But authentication tests theory is not suitable for analyzing all protocols. It has flaws in processing session keys and must be improved.This thesis is mainly about how to improve the theory of authentication tests, aiming to make security protocol more effective by using authentication tests. Besides, the current methods of analyze protocol are primarily manual and far from satisfactory. This paper expands automatic security protocol analysis on the basis of preliminary works. With this approach, users only need to input desired security protocol and set security requirements and then software shows the evidence of protocols correct or unsafe parameters. Designing efficient algorithms for automatic protocol analysis is very difficult and a type-flaw checking algorithm is included.