As the growth of Internet applications, more cryptographic protocols have been used to achieve on the open network, and they have been the basis of many distributed applications. Unfortunately, the analysis and design of cryptographic protocols are very difficult due to the complexity of the protocol execution. Some researchers introduced formal methods for analyzing cryptographic protocols, and achieved many significant results by building formal models and automatic verifying tools. However, there are still a number of unsolved problems in this field.In this thesis, a new formal model is built for cryptographic protocol analysis, and some theoretic results are reached based on the model; an automatic verification technique is presented for the analysis of security protocols; In this thesis the following results are achieved:(1) By building a new algebra called Cryptographic Protocol Algebra (CPA), we have proposed a novel formal model for cryptographic protocol analysis. In the model, knowledge sets of participants are characterized with some algebraic notions such as... |