Implementing a Formally Verifiable Security Protocol in Java Card

  • Engelbert Hubbers
  • Martijn Oostdijk
  • Erik Poll
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2802)


This paper describes a case study in refining an abstract security protocol description down to a concrete implementation on a Java Card smart card. The aim is to consider the decisions that have to be made in the development of such an implementation in a systematic way, and to investigate the possibilities of formal specification and verification in the design process and for the final implementation.


Model Checker Smart Card Security Protocol Security Property Java Modeling Language 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. In: Proc. Royal Soc. Series A, vol. 426, pp. 233–271 (1989)Google Scholar
  2. 2.
    Ryan, P., Schneider, S., Goldschmith, M., Lowe, G., Roscoe, A.W.: The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, Reading (2001)Google Scholar
  3. 3.
    Leavens, G., Baker, A., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06q, Dep. of Comp. Sci., Iowa State Univ. (2002)Google Scholar
  4. 4.
    Cheon, Y., Leavens, G.: A Runtime Assertion Checker for the Java Modeling Language (JML). In: Arabnia, H., Mun, Y. (eds.) International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, June 2002, pp. 322–328. CSREA Press (2002)Google Scholar
  5. 5.
    Compaq Systems Research Center: Extended Static Checker for Java (2001), version 1.2.4,
  6. 6.
    Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (1997),
  7. 7.
    Lowe, G.: Casper: A Compiler for the Analysis of Security Protocols, version 1.5 (2001),
  8. 8.
    Formal Systems: FDR2, Failures Divergence Refinement, version 2.78 (2000),
  9. 9.
    Cataño, N., Huisman, M.: Formal specification of Gemplus’s electronic purse case study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 272–289. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Poll, E., van den Berg, J., Jacobs, B.: Formal specification of the Java Card API in JML: the APDU class. Computer Networks 36, 407–421 (2001)CrossRefGoogle Scholar
  11. 11.
    Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Domingo-Ferrer, J., Chan, D., Watson, A. (eds.) Fourth Smart Card Research and Advanced Application Conference (CARDIS 2000), pp. 135–154. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  12. 12.
    Marlet, R., Metayer, D.L.: Security properties and java card specificities to be studied in the secsafe project. Technical Report SECSAFE-TL-006, Trusted Logic (2001), Available from
  13. 13.
    Uppaal: An integrated tool environment for modeling, validation and verification of real-time system modeled as networks of timed automata, extended with data types, version 3.2.11 (2002),
  14. 14.
    Jacobs, B., et al.: Reasoning about classes in Java (preliminary report). In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA, pp. 329–340. ACM Press, New York (1998)Google Scholar
  15. 15.
    Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, USA (1999), Available at
  16. 16.
    Breunesse, C.B., Jacobs, B., van den Berg, J.: Specifying and verifying a decimal representation in Java for smart cards. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 304–318. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Engelbert Hubbers
    • 1
  • Martijn Oostdijk
    • 1
  • Erik Poll
    • 1
  1. 1.Nijmegen Institute for Information and Computing SciencesUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations