Skip to main content
SpringerLink
Log in

Secure Recharge of Disposable RFID Tickets

  • Conference paper
Formal Aspects of Security and Trust (FAST 2011)

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

Included in the following conference series:

Abstract

We study the Mifare Ultralight cards in detail, and we present a new secure method for the recharge of these RFID disposable tickets that also extends to the case of multiple resources on a single device. We specify a formal but yet realistic semantics of these cards, and we also define a simple imperative language suitable to program secure APIs. In fact, the language is provided with a type-system enforcing security properties on resources stored in the card.

Work partially supported by the RAS Project “TESLA: Techniques for Enforcing Security in Languages and Applications”.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. Moscow metro: the worlds first major transport system to operate fully contactless with nxps mifare technology. press statement (2009), http://www.nxp.com/news/content/file_1518.html

  2. Mifare ultralight contactless single-ticket IC, Product data sheet. Rev. 3.8 028638 (December 22 , 2010), www.nxp.com/documents/data_sheet/MF0ICU1.pdf

  3. Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Resource-aware Authorization Policies for Statically Typed Cryptographic Protocols. In: Proc. of 24th IEEE Symposium on Computer Security Foundations (2011)

    Google Scholar 

  4. Centenaro, M., Focardi, R., Luccio, F., Steel, G.: Type-Based Analysis of PIN Processing APIs. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 53–68. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Gordon, A., Jeffrey, A.: A Type and Effect Analysisof Security Protocols. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 432. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Siekerman, P., van der Schee, M.: Security evaluation of the disposable ov-chipkaart v1.7. Research Project, University of Amsterdam (2007), http://staff.science.uva.nl/~delaat/sne-2006-2007/p41/Report.pdf

  7. Steel, G.: Formal Analysis of PIN Block Attacks. Theoretical Computer Science 367(1-2), 257–270 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  8. Tanenbaum, A.: Dutch public transit card broken (2008), http://www.cs.vu.nl/~ast/ov-chip-card/

  9. Verdult, R.: Proof of concept, cloning the ov-chip card, Technical report, Radboud University Nijmegen (2008), http://www.cs.ru.nl/~flaviog/OV-Chip.pdf

Download references

Author information

Authors and Affiliations

  1. DAIS, Università Ca’ Foscari Venezia, Italy

    Riccardo Focardi & Flaminia L. Luccio

Authors
  1. Riccardo Focardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Flaminia L. Luccio
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Universidad Politecnica de Madrid, Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Carnegie Mellon University, NASA Research Park, Bldg. 23 (MS 23-11), P.O. Box 1, 94035-0001, Moffet Field, CA, USA

    Anupam Datta

  3. Faculty of Mathematics and Computer Science, Embedded Systems Security Group, Technical University of Eindhoven, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Sandro Etalle

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Focardi, R., Luccio, F.L. (2012). Secure Recharge of Disposable RFID Tickets. In: Barthe, G., Datta, A., Etalle, S. (eds) Formal Aspects of Security and Trust. FAST 2011. Lecture Notes in Computer Science, vol 7140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29420-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-29420-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-29419-8

  • Online ISBN: 978-3-642-29420-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation