A Method For Formal Analysis Of E-commerce Security Protocol

With the rapid development of network, e-commerce has become a widely accepted business model. The importance of e-commerce security protocol is self-evident as a key factor to ensure the information and data security, and to safeguard the vital interests of both sides. Therefore, a growing number of cryptotechnique are widely used in e-commerce security protocol. However, with various attacks against the security protocol, there have been higher requirements for the analysis of it. Formal method is an effective way of security protocol's analysis,its strand space model and related theories has significantly promoting the analysis .First, this dissertation analyzes the e-commerce security protocol and its significant influence on e-commerce, and then it makes an introduction to the strand space model and its authentication test. In respect of e-commerce security protocol based on the rich cryptography primitives,the original strand space model cannot make analyses and description of the more complex operations in cryptography primitives, such as sign operation, DH calculation, hash functions, etc.; therefore, this dissertation makes Formal definitions of sign operation, DH calculation, hash functions in the first place. By expanding the strand space model, including the massage term, the in-term relation and penetrator's model, it correspondingly expands the authentication test method, including input test, output test and unsolicited test, and puts forward a way to expand the authentication test method that is based on the rich cryptographic primitives. At last, it analyzes SSL3.0 and TLS1.0 handshaking protocol with primitive message structure rich in cryptographic primitives, and validates the authentication properties of the protocol; furthermore, it proves the correctness of the strand space model and its authentication test method through case analysis.This dissertation extends the strand space model and its authentication test, which can enhance the analyses and description of some cryptographic primitives rich in cryptographic primitives. It has been proven by instances that the extended model and method can better analyze and describe the security of e-commerce security protocol, and be applied in wider fields.