Formal Analysis of Secure Transaction Protocols

Abstract

In today’s information technology society, people are increasingly dependent on the internet for quality life. E-commerce systems have thus being presented attractive proliferation. The short list of facts below should be sufficient to place the current situation into perspective.

United States e-commerce transactions resulted in 707 million dollars in revenue in 1996, increasing to an impressive 2.6 billion dollars in 1997, and to an incredible high of 5.8 billion dollars in 1998. It is estimated that in 2007, nearly 40 million US households will book travel online, spending 86 billion on airline tickets, lodging, cars, intercity rail, cruises, and packages. (Forrester).

As a result, a significant amount of research in the field of e-commerce has been carried out in the past decade, resulting in a variety of algorithms and techniques for electronic trading on the internet. A key problem for e-commerce users is how to carry out trade transactions on the internet safely. The security problems of e-commerce have mainly arisen from the fact that:

• data can be divulged: some important commercial information, including account number, is transmitted in plain text.

• information and source can be shared: a number of users in different locations can freely access other computers.

Security in e-commerce is implemented by relying on a set of security protocols that meet the user’s expectation for secure business transactions. Communication between principals may be compromised without effective security protocols for key-exchange, authentication and privacy. Therefore security protocols, including cryptographic protocols and secure transaction protocols etc, have become the prime requisite of e-commerce systems. Ideally, these security policies should state the overall objectives of a transaction in terms of integrity, confidentiality and availability, and address the range of circumstances under which these objectives must be met.

Recently, there have been many remarkable efforts made on the security problem by developing methodologies, theories, logics, and other supporting tools. They are effective in overcoming the weakness and reducing the redundancies at the protocol design stage. However, there are also several instances of protocols advocated in [79, 120] which have been proved to be vulnerable to attack [65]. Therefore, it is so important to find ways to justify whether so-called secure protocols are secure. Without this justification, the users of electronic transactions will be on risk.

As already described, the existing approaches to validate security protocols can be mainly classified into three categories: attack-construction approaches, inference-construction approaches and proof-construction approaches. Although many subsequent methods are developed from them, as described in Chapter 2, they are subject to the exploration of search space, incomplete semantics or complexity. On the other hand, the features of electronic transaction cannot be handled by most of the traditional formal analysis of security protocols.

There have been attempts to analyse realistic e-commerce protocols, including the work of Kailar [82], Brackin [15], Meadows and Syverson [113] and Bolignano [10]. Recently, a number of approaches have been developed to analyse electronic commerce protocols from different aspects. An anonymous fair exchange e-commerce protocol that is claimed to satisfy fair exchange and customer’s anonymity is analysed using OTS/CafeOBJ method [88]. In [127], a formalism that provides an expressive message passing semantics and sophisticated constructs for modelling principals is presented. A formal analysis based on Casper and FDR2 is proposed to analyse two electronic payment protocols: Visa 3D Secure and MasterCard Secure Code. It highlights issues concerning payment security in the proposed protocols. As to the electronic transaction using mobile devices, this complements protocol analysis techniques in terms of state enumeration. However, these security protocols are highly susceptible to subtle errors in real-world transactions. There are also many technical issues arising from cryptographic algorithms and network communication protocols [8, 41]. The limitations in existing validating approaches have been described in the former chapters.

As we have seen, it is very difficult to develop a verification approach that is suitable for all related protocols. In this chapter, a logical framework, ENDL [29], is proposed for validating secure transaction protocols [30]. The ENDL is referred as an inference-construction approach. It is developed since NDL contains some limitations, 1) it is not considerate on some aspects of practical financial circumstance, such as the certificate authentication; 2) it has been unable to accommodate some potential threats such as collusion attacks. The accumulation rule is further classified in terms of corresponding situations, thereby it becomes more reasonable and applicable. By using the timestamp in validation, this can benefit the detection of replay attacks, which cannot be done by NDL.

Compared to traditional techniques, ENDL has some distinct features, such as fail-negate, dynamic, non-monotonic, freshness, identity and random number. Some properties are inherited from NDL. The timestamp has been used for modelling freshness in ENDL, which is the complement of BAN and GNY. These features enable us to solve the key problem of data integrity. To evaluate the logic, three practical instances of security protocols are illustrated. The results demonstrate that ENDL is effective and promising in analysing security protocols.

This chapter focuses on the design of a logical framework, ENDL. Several formal methods for analysing e-commerce protocols are presented in Section 3.2. Section 3.3 presents a computational model. In Section 3.4, a formal description of basic terms and statements of ENDL are provided. Section 3.5 establishes a basic inference framework and uses three practical transaction instances to evaluate ENDL. Section 3.6 concludes this chapter.