Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus

Abstract. We 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. We analyse 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.

• Type: Journal
• Year: 2010
• Where: IFIP
• Authors: Naipeng Dong, Hugo L. Jonker, Jun Pang
• Keywords: Auction Protocol, IFIP 2010, Online Auction Protocols, Programming Languages, Receipt-free Auction Protocol