Interest Property of E-commerce Protocols and its Verification in Strand Space Model

The difficulties of e-commerce protocol security are mainly reflected in two aspects: First, the industry has not yet come to a uniform conclusion for the requirements of the security properties of e-commerce, while new properties are continually proposed and updated. The second is the difficulty of the protocol design and verification. This paper makes a new explanation of the protection of individual´s interests of e-commerce protocols that is defined as the active protection of individual´s interests + active capture of individual´s interests. Subsequently, the strand space model for the analysis of security protocols is extended. Afterwards, the theorem of the existence of sending edge and the theorem of the existence of receiving edge are presented. The extended strand space model can be applied to the analysis of the interest property of e-commerce protocols. Finally, an analysis and verification of ASW protocol are made. The result shows that this protocol is of security to the interest property.