The application of formal methods to security protocol analysis has
attracted increasing attention in the past two decades, and recently has
been sh- ing signs of new maturity and consolidation. The development of
these formal
methodsismotivatedbythehostilenatureofsomeaspectsofthenetworkand the
persistent e?orts of intruders, and has been widely discussed among -
searchers in this ?eld. Contributions to the investigation of novel and
e?cient ideas and techniques have been made through some important
conferences and journals, such asESORICS, CSFW andACM Transactions in
Computer Systems. Thus, formal methods have played an important role in
a variety of applications such as discrete system analysis for
cryptographic protocols, - lief logics and state exploration tools. A
complicated security protocol can be
abstractedasamanipulationofsymbolsandstructurescomposedbysymbols. The
analysis of e-commerce (electronic commerce) protocols is a particular
case of such symbol systems. There have been considerable e?orts in
developing a number of tools for ensuring the security of protocols,
both specialized and general-purpose, such as belief logic and process
algebras. The application of formal methods starts with the analysis of
key-distribution protocols for communication between two principals at
an early stage. With the performance of transactions - coming more and
more dependent on computer networks, and cryptography becoming more
widely deployed, the type of application becomes more varied and
complicated. The emerging complex network-based transactions such as
?nancial transactionsand secure groupcommunication have not only brought
innovationstothecurrentbusinesspractice, butthey alsoposeabigchallenge
to protect the information transmitted over the open network from
malicious attack
