Formal modelling and analysis of receipt-free auction protocols in applied pi

We formally study two privacy-type properties for e-auction protocols: bidding-price-secrecy and receipt-freeness. These properties are formalised as observational equivalences in the applied pi calculus. We analyse two receipt-free auction protocols: one proposed by Abe and Suzuki in 2002 (AS02) and the other by Howlader et al. in 2014 (HRM14). Bidding-price-secrecy of the AS02 protocol is verified using the automatic verifier ProVerif, whereas receipt-freeness of the two protocols, as well as bidding-price-secrecy of the HRM14 protocol, are proved manually.