Key Issues Of Formal Analysis For Seciruty Protocols

Even proved to be an efficient method for safety testing on security protocols, the formal analysis method of security protocols still exhibits limitation. According to analysis and summarization of current formal analysis methods, this thesis proposes a formal analysis method aimed at three key issues:parallel sessions, algebraic properties and security properties. Based on above, solutions to algebra and security properties problems are presented and their efficiency is verified in the testing afterwards. Following are the main results of this thesis.(1) Constructs a formal basic model for security protocols.According to the assumptions of security protocols formal analysis, this thesis constructs a formal basic model for security protocols without limitation of parallel sessions numbers, which formally describes protocol model with rewriting rules, and describes attacker model with tree automata.(2) Presents a formal description method of algebraic properties.After research on backgrounds of algebraic properties issue in detail, this thesis expands formal basic model of security protocols by adding rewriting rules to basic model. The rewriting rules are inverted from algebraic properties according to rewriting theory.(3) Presents a formal description method of security properties.After research on authentication property and secrecy property in detail, this thesis gives formal description based on terms, and adds it to the set of rewriting rules, and then expands the formal basic model of security protocols further. This thesis also presents the formal description of authentication property and secrecy property based on tree automata.(4) Presents an analysis and testing method for security protocol formulizing.This method starts from the modified basic model, deduces the tree automata to describe the approximate knowledge set of attacker by apply the rewriting rules into the tree automata, then run the intersection between this tree automata and security properties tree automata. And then make the analysis and testing for security properties. This method takes algebraic properties into account without limitation of parallel sessions numbers. The result of the test proves the efficiency of the key solution presented in this thesis, which can detect attacks based on algebraic properties.