Abstract
We present a refinement method for Java programs which is motivated by the challenge of verifying security protocol implementations. The method can be used for stepwise refinement of abstract specifications down to the level of code running in the real application. The approach is based on a calculus for the verification of Java programs for the concrete level and Abstract State Machines for the abstract level. In this paper we illustrate our method by the verification of a M-Commerce application for buying movie tickets using a mobile phone written in J2ME. For verification we use KIV, our interactive theorem prover [1].
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
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol. 1783, Springer, Heidelberg (2000)
Tickets on your Mobile. [last seen 2007-03-16] URL: http://www.beep.nl
Bolton, C., Davies, J., Woodcock, J.C.P.: On the refinement and simulation of data types and processes. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999. Proceedings of the International conference of Integrated Formal Methods, pp. 273–292. Springer, Heidelberg (1999)
Börger, E., Stärk, R.F.: Abstract State Machines—A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Breunesse, C., 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, Springer, Heidelberg (2002)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of jml tools and applications. In: Burdy, L., Arts, T., Fokkink, W. (eds.) FMICS ’03. Eighth International Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 80, Elsevier, Amsterdam (2003)
Burrows, M., Abadi, M., Needham, R.M.: A Logic of Authentication. Technical report, SRC Research Report, 39 (1989)
de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)
Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. FACIT. Springer, Heidelberg (2001)
Grandy, H., Haneberg, D., Reif, W., Stenzel, K.: Developing Provably Secure M-Commerce Applications. In: Müller, G. (ed.) ETRICS 2006. LNCS, vol. 3995, pp. 115–129. Springer, Heidelberg (2006)
Grandy, H., Moebius, N., Bischof, M., Haneberg, D., Schellhorn, G., Stenzel, K., Reif, W.: The Mondex Case Study: From Specifications to Code. Technical Report 2006-31, University of Augsburg (2006) URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications/
Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Technical Report 2006-32, University of Augsburg (2006) URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications/
Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 86. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Hubbers, E., Oostdijk, M., Poll, E.: Implementing a Formally Verifiable Security Protocol in Java Card. In: Hutter, D., Müller, G., Stephan, W., Ullmann, M. (eds.) Security in Pervasive Computing. LNCS, vol. 2802, Springer, Heidelberg (2004)
Huisman, M.: Verification of java’s abstractcollection class: a case study. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, Springer, Heidelberg (2002)
Jacobs, B., Marche, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)
Joy, B., Steele, G., Gosling, J., Bracha, G. (eds.): The Java (tm) Language Specification, 2nd edn. Addison-Wesley, Reading (2000)
KIV homepage, http://www.informatik.uni-augsburg.de/swt/kiv
Mantel, H.: Preserving Information Flow Properties under Refinement. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA (2001)
Marlet, R., Le Metayer, D.: Verification of Cryptographic Protocols Implemented in JavaCard. In: e-Smart 2003. Proceedings of the e-Smart conference, Sophia Antipolis (2003)
MasterCard International Inc. Mondex. URL: http://www.mondex.com
Mostowski, W.: Rigorous development of java card applications. In: Clarke, T., Evans, A., Lano, K. (eds.) Proceedings, Fourth Workshop on Rigorous Object-Oriented Methods, London (2002)
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security 6 (1998)
Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification Approach for Mondex Electronic Purses using ASMs. Technical Report 2006-27, Universität Augsburg (2006), http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications/
Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 16–31. Springer, Heidelberg (2006)
Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)
Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universität Augsburg, Fakultät für Angewandte Informatik (2005), http://www.opus-bayern.de/uni-augsburg/volltexte/2005/122/ , or http://www.informatik.uni-augsburg.de/forschung/dissertations/
Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000), http://www-users.cs.york.ac.uk/~susan/bib/ss/z/monog.htm
Tobler, B., Hutchison, A.: Generating Network Security Protocol Implementations from Formal Specifications. In: CSES 2004. 2nd International Workshop on Certification and Security in Inter-Organizational E-Services at IFIPWorldComputerCongress, Toulouse, France (2004)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)
Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer 39(10), 57–64 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Grandy, H., Stenzel, K., Reif, W. (2007). A Refinement Method for Java Programs. In: Bonsangue, M.M., Johnsen, E.B. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72952-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-72952-5_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72919-8
Online ISBN: 978-3-540-72952-5
eBook Packages: Computer ScienceComputer Science (R0)