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.
Naipeng Dong, Hugo L. Jonker, Jun Pang