Automatic Verification Of Security Protocols Based On Tree Automata

In this thesis, we present a method, which is based on tree automata and term rewriting systems, to analyze security protocols. First, protocol steps are operationally described using term rewriting systems and the initial set of communication requests is described by a tree automaton. After that, according to term rewriting systems, the tree automaton iterates and reduces to over-approximate the set of exchanged messages. Finally, the automaton is terminated, it is easy to prove security properties by showing that the intersection between the approximation and a set of prohibited behaviors is empty or not.Under the above principle, this paper designs a system called TAVS(Tree Automata Verification System) to verify security protocols automatically. This system introduces approximation rules to traditional tree automata, and is more efficient.TAVS could model protocols, prove security goals and construct intruder traces automatically. It can verify authentication protocols, key exchange protocols and etc. In the final, the LPD-IMSR protocol is verified and a new man-in-the-middle attack on authentication is found. An improved scheme with signature on certain fields is also proposed to prevent the attack.