Auctions have a long history, having been recorded as early as 500 B.C.. With the rise of Internet, electronic auctions have been a great success and are increasingly used. Many cryptographic protocols have been proposed to address the various security requirements of these electronic transactions. We propose a formal framework to analyze and verify security properties of e-Auction protocols. We model protocols in the Applied π-Calculus and define privacy notions, which include secrecy of bids, anonymity of the participants, receipt-freeness and coercion-resistance. We also discuss fairness, non-repudiation and non-cancellation. Additionally we show on two case studies how these properties can be verified automatically using ProVerif, and discover several attacks. © 2013 Springer-Verlag.
CITATION STYLE
Dreier, J., Lafourcade, P., & Lakhnech, Y. (2013). Formal verification of e-Auction protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7796 LNCS, pp. 247–266). https://doi.org/10.1007/978-3-642-36830-1_13
Mendeley helps you to discover research relevant for your work.