Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Krishna, V.: Auction Theory. Academic Press (2002)
Brandt, F.: A verifiable, bidder-resolved auction protocol. In: Proceedings of the 5th AAMAS Workshop on Deception, Fraud and Trust in Agent Societies, pp. 18–25 (2002)
Brandt, F.: How to obtain full privacy in auctions. International Journal of Information Security 5, 201–216 (2006)
Brandt, F., Sandholm, T.: On the existence of unconditionally privacy-preserving auction protocols. ACM Trans. Inf. Syst. Secur. 11, 6:1–6:21 (2008)
Passch, C., Song, W., Kou, W., Tan, C.-J.: Online Auction Protocols: A Comparative Study. In: Kou, W., Yesha, Y., Tan, C.J.K. (eds.) ISEC 2001. LNCS, vol. 2040, pp. 170–186. Springer, Heidelberg (2001)
Curtis, B., Pieprzyk, J., Seruga, J.: An efficient eauction protocol. In: ARES, pp. 417–421. IEEE Computer Society (2007)
Franklin, M., Reiter, M.: The design and implementation of a secure auction service. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy, pp. 2–14 (May 1995)
Harkavy, M., Tygar, J.D., Kikuchi, H.: Electronic auctions with private bids. In: Proceedings of the 3rd USENIX Workshop on Electronic Commerce, pp. 61–74 (1998)
Kikuchi, H., Harkavy, M., Tygar, J.D.: Multi-round anonymous auction protocols. In: Proceedings of the First IEEE Workshop on Dependable and Real-Time E-Commerce Systems, pp. 62–69. Springer (1998)
Lee, B., Kim, K., Ma, J.: Efficient Public Auction with One-Time Registration and Public Verifiability. In: Pandu Rangan, C., Ding, C. (eds.) INDOCRYPT 2001. LNCS, vol. 2247, pp. 162–174. Springer, Heidelberg (2001)
Omote, K., Miyaji, A.: A Practical English Auction with One-Time Registration. In: Varadharajan, V., Mu, Y. (eds.) ACISP 2001. LNCS, vol. 2119, pp. 221–234. Springer, Heidelberg (2001)
Abe, M., Suzuki, K.: Receipt-Free Sealed-Bid Auction. In: Chan, A.H., Gligor, V.D. (eds.) ISC 2002. LNCS, vol. 2433, pp. 191–199. Springer, Heidelberg (2002)
Stubblebine, S.G., Syverson, P.F.: Fair On-Line Auctions without Special Trusted Parties. In: Franklin, M.K. (ed.) FC 1999. LNCS, vol. 1648, pp. 230–240. Springer, Heidelberg (1999)
Subramanian, S.: Design and verification of a secure electronic auction protocol. In: Proceedings of the 17th IEEE Symposium on Reliable Distributed Systems, SRDS 1998, pp. 204–210. IEEE Computer Society (1998)
Dong, N., Jonker, H., Pang, J.: Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 223–238. Springer, Heidelberg (2011)
Küsters, R., Truderung, T., Vogt, A.: Accountability: definition and relationship to verifiability. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pp. 526–535. ACM (2010)
Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF 2008, pp. 195–209 (2008)
Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17, 435–487 (2009)
Dreier, J., Lafourcade, P., Lakhnech, Y.: Vote-Independence: A Powerful Privacy Notion for Voting Protocols. In: Garcia-Alfaro, J., Lafourcade, P. (eds.) FPS 2011. LNCS, vol. 6888, pp. 164–180. Springer, Heidelberg (2012)
Dreier, J., Lafourcade, P., Lakhnech, Y.: Defining Privacy for Weighted Votes, Single and Multi-voter Coercion. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 451–468. Springer, Heidelberg (2012)
Dreier, J., Lafourcade, P., Lakhnech, Y.: A formal taxonomy of privacy in voting protocols. In: First IEEE International Workshop on Security and Forensics in Communication Systems, ICC 2012 WS - SFCS (2012)
Küsters, R., Truderung, T.: An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols. In: S&P 2009, pp. 251–266. IEEE Computer Society (2009)
Smyth, B., Cortier, V.: Attacking and fixing helios: An analysis of ballot secrecy. In: CSF 2011, pp. 297–311. IEEE (2011)
Klay, F., Vigneron, L.: Formal aspects in security and trust, pp. 192–209. Springer (2009)
Liu, J., Vigneron, L.: Design and verification of a non-repudiation protocol based on receiver-side smart card. Information Security, IET 4(1), 15–29 (2010)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104–115. ACM, New York (2001)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: CSFW 2001, pp. 82–96. IEEE Computer Society, Cape Breton (2001)
Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1), 3–51 (2008)
Dreier, J., Lafourcade, P., Lakhnech, Y.: Formal verification of e-auction protocols. Technical Report TR-2012-17, Verimag Research Report (October 2012), http://www-verimag.imag.fr/TR/TR-2012-17.pdf
Dreier, J.: The proverif code used to automatically verify the examples is available at http://www-verimag.imag.fr/~dreier/papers/post-code.zip (2012)
Klus, P., Smyth, B., Ryan, M.D.: Proswapper: Improved equivalence verifier for proverif (2010), http://www.bensmyth.com/proswapper.php
Arapinis, M., Ritter, E., Ryan, M.D.: Statverif: Verification of stateful processes. In: CSF 2011, pp. 33–47. IEEE Computer Society (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dreier, J., Lafourcade, P., Lakhnech, Y. (2013). Formal Verification of e-Auction Protocols. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)