A Research On Formal Analysis Of Authentication Protocols With CSP Approach

With computer network and communication network getting even more complex today, the variety and quantity of protocols have increased to an astounding degree, so it is with their size and scale. How to design a communication protocol, which is functionally reliable and logically correct, and can be easily verified, tested and implemented, has become a very challenging problem. So a new-emerging branch subject of software engineer-- Protocol Engineer come into our sight.As a formalized development process for communication protocols, it applied formal methods in every steps and links of protocol design and maintenance. Also, Formal description techniques take up the core of protocol engineer. At present, the most common used formal methods are: Finite State Machine, Petri model and LOTOS, CAPSL etc, all of which have its own plus and minus. Thus we have all the more reason to study and seek some new theories and methods in this field.Based on a sturdy research into Communicating Sequential Process, especially in modeling and analysis for authentication protocols, we carefully study and compare the frequently used formal methods for protocol specification along with their own limitation. Then through modeling Yahalom protocol with CSP approach, a set of general steps and techniques on how to apply CSP in authentication protocol modeling is given.On top of these, CSP approach has even been extended to depict the ordinary communication protocols like RIP, from which, a set of general technique of modeling protocols with CSP is concluded. At last, due to the inconsistence between protocol specification and specific implementation, a CSP development framework is therefore presented here .Even though still remaining in theory, it brought a new idea on how to completely incorporate formal methods and programming language into a framework, which aids to carry out the smooth transition from formal specification to protocol implementation Besides, it can be conveniently used to translate CSP-verified protocols specification into its specific version, avoiding the possibility of bringing new security problem in the translation process.