Design and verification of a secure electronic auction protocol

Auctions are an important and common form of commerce today. A difficult aspect of auctions is that the bidder must be present at the site of the auction. This reduces the appeal of auction and restricts the number of people who would otherwise participate in if. An auction over an electronic network is, therefore, an attractive way of conducting : business. In this paper the author proposes a protocol for electronic auctions. This protocol ensures: (a) anonymity of the customer, (b) security from passive attacks, active attack, message corruption, and loss of messages, (c) customer's privacy, and (d) atomicity (i.e., under all circumstances, the transaction is either completed or aborted). A logic is developed based on the semantics of BAN-style [4] logic. Using this logic, the properties of anonymity, security, privacy, and atomicity are proved for the proposed protocol.