Abstract: Formal method and automated tools arc both necessary and efficient for analyzing practical security protocols. Theorem proving theory has been studied intensively because it can verify infinite-state system. But there are still limitations when verifying large scale system automatically. A formal model for security protocols was proposed based on theorem proving and rewriting approximation theory. It utilizes term rewriting system and tree automata to model protocol and the knowledge of intruder. An automatic generated approximation algorithm was designed to calculate the fix-point tree automata. In this model, secrecy and authentication were discussed. By a case of study, NSPK was analyzed effectively.

Key words: Security protocol, TRS, Tree automata, Tree language, Approximation, Secrecy, Authentication