The Application Study On Formalism Of Electronic Commerce Protocols Based On SVO Logic

Formal analysis of E-commerce protocols is an important aspect of E-commerce study,the E-commerce protocols is a cryptographic protocol of E-commerce,a secure E-commerce protocol is the foundation of E-commerce.Study on formal analysis of E-commerce protocols has profound effects both in theory and realizable application,it's the technical indemnification for E-commerce opertion.Formal methods are the most important methods to analysis an verify the security protocols.Such as the provable theory, BANS logic, model check and theorem proves.The dissertation mainly studies the applications of logic and model checking methods in formal analysis of E-commerce protocols, especially studies on SVO logic method and the application of SVO logic on E-commerce formal analyzing of timeliness. In general,the author studies the related formal analysis technology of E-commerce protocols from two aspects,theory and application.The main works and results are as follows:(1) Sum up the status of the reseach in electronic commerce protocols and formal analysis method.(2) Studies the advantages and disadvantages on BAN logic,and extends part of axiom ruls.Studies the advantages and disadvantages on SVO logic,and improve part of disadvantages to formally analyze the timeliness of E-commerce protocols.(3) Introduces the work of model-checking tool Spin.Through studies its model language Promela,we discover it is very difficult to completely simulate the time section,but we can simulate parts of the time section by some programme sleights to simulate the time characteristic of protocols.(4) Improves Kerberos authentication protocol based on public key cryptography, exactly describes and proves the security of improved Kerberos protocol by using BAN logic.(5) Studies classic E-commerce protocols: NZG protocol and ISI protocol, analyzes their advantages and disadvantages, designs a new E-commerce protocol which has such characters: security, non-repudiation, and timeliness.(6) Extends SVO logic to formally analyze E-commerce protocols besides it's timeliness, and analyze the new E-commerce protocol by using SPIN to prove that this improvement is successful.