Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus
The authors formally study two privacy-type properties in online auction protocols, bidding-price-secrecy and receipt-freeness. These properties are formalised as observational equivalences in the applied ? calculus. They analyze the receipt-free auction protocol by Abe and Suzuki. Bidding-price-secrecy of the protocol is verified using ProVerif, whereas receipt-freeness of the protocol is proved manually. Auctions are ways to negotiate the exchange of goods and commodities. In an auction, a seller offers an item for bid, buyers submit bids, and the seller sells the item to the buyer with the highest bid. Nowadays, with the widely spread use of the Internet, online auctions are more and more often used as a convenient way to trade.