Skip to main content
SpringerLink
Log in

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

  • Conference paper
Book cover Formal Aspects of Security and Trust (FAST 2010)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 6561))

Included in the following conference series:

Abstract

We formally study two privacy-type properties for 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Harkavy, M., Tygar, J.D., Kikuchi, H.: Electronic auctions with private bids. In: Proc. 3rd USENIX Workshop on Electronic Commerce, pp. 61–74 (1998)

    Google Scholar 

  2. Cachin, C.: Efficient private bidding and auctions with an oblivious third party. In: Proc. CCS 1999, pp. 120–127. ACM Press, New York (1999)

    Google Scholar 

  3. Naor, M., Pinkas, B., Sumner, R.: Privacy preserving auctions and mechanism design. In: Proc. ACM-EC 1999, pp. 129–139. ACM Press, New York (1999)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Lipmaa, H., Asokan, N., Niemi, V.: Secure vickrey auctions without threshold trust. In: Blaze, M. (ed.) FC 2002. LNCS, vol. 2357, pp. 87–101. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Chen, X., Lee, B., Kim, K.: Receipt-free electronic auction schemes using homomorphic encryption. In: Lim, J.-I., Lee, D.-H. (eds.) ICISC 2003. LNCS, vol. 2971, pp. 259–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  8. Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multi-party contract signing. In: Proc. CSFW 2004, pp. 266–279. IEEE CS, Los Alamitos (2004)

    Google Scholar 

  9. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. POPL 2001, pp. 104–115. ACM, New York (2001)

    Google Scholar 

  10. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. CSFW 2001, pp. 82–96. IEEE CS, Los Alamitos (2001)

    Google Scholar 

  11. Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Computer Security 17(4), 435–487 (2009)

    Article  MATH  Google Scholar 

  12. Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Jonker, H.L., Mauw, S., Pang, J.: A formal framework for quantifying voter-controlled privacy. J. Algorithms 64(2-3), 89–105 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  14. Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Information Theory 29(2), 198–207 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  15. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  16. Backes, M., Hriţcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Proc. CSF 2008, pp. 195–209. IEEE CS, Los Alamitos (2008)

    Google Scholar 

  17. Küsters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: Proc. S&P 2009, pp. 251–266. IEEE CS, Los Alamitos (2009)

    Google Scholar 

  18. Küsters, R., Truderung, T., Vogt, A.: A game-based definition of coercion-resistance and its applications. In: Proc. CSF 2010, pp. 122–136. IEEE CS, Los Alamitos (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Sciences, Technology and Communication, University of Luxembourg, Luxembourg

    Naipeng Dong, Hugo Jonker & Jun Pang

Authors
  1. Naipeng Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hugo Jonker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jun Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Largo Bruno Pontecorvo, 3, 56127, Pisa, Italy

    Pierpaolo Degano

  2. Faculty of Mathematics and Computer Science, Technical University of Eindhoven, P.O. Box 513, 5600, Eindhoven, MB, The Netherlands

    Sandro Etalle

  3. Computer Science, Worcester Polytechnic Institute, 100 Institute Road, 01609, Worcester, MA, USA

    Joshua Guttman

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dong, N., Jonker, H., Pang, J. (2011). Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus. In: Degano, P., Etalle, S., Guttman, J. (eds) Formal Aspects of Security and Trust. FAST 2010. Lecture Notes in Computer Science, vol 6561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19751-2_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-19751-2_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-19750-5

  • Online ISBN: 978-3-642-19751-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation