Abstract
The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results.
First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study.
Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Burrows M, Abadi M, Needham R (1990) A logic of authentication. ACM Trans Comput Syst 8(1)
Bellare M, Canetti R, Krawczyk H (1996) Keying hash functions for message authentication. In: Koblitz N (eds) Advances in Cryptology—Crypto 96 Proceedings, vol 1109 of LNCS. Springer, Heidelberg
Balser M, Duelli C, Reif W, Schellhorn G (2002) Verifying concurrent systems with symbolic execution. J Logic Comput 12(4):549–560
Boiten E, Derrick J, Schellhorn G (2007) Relational concurrent refinement part ii: intenral operations and ouputs. FAC (under consideration)
Basin D, Mödersheim S, Viganò L (2003) An on-the-fly model-checker for security protocol analysis. In: Proceedings of Esorics’03, LNCS 2808, Springer, Heidelberg, pp 253–270
Börger E (2003) The ASM refinement method. Form Aspects Comput 15(1–2):237–257
Börger E, Rosenzweig D (1995) The WAM-definition and compiler correctness. In: Beierle C, Plümer L (eds) Logic Programming: Formal Methods and Practical Applications Studies in Computer Science and Artificial Intelligence 11. North-Holland, Amsterdam, pp 20–90
Börger E, Stärk RF (2003) Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg
Carlsen U (1994) Generating formal cryptographic protocol specifications. In: IEEE Symposium on Research in Security and Privacy. IEEE Computer Society, pp 137–146
UK ITSEC Certification Body (1999) UK ITSEC Scheme Certification Report No. P129 Mondex Purse. Technical report, UK IT Security Evaluation and Certification Scheme, URL: http://www.cesg.gov.uk/site/iacs/itsec/media/certreps/CRP129.pdf
Clarke EM, Jha S, Marrero W (1998) Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proceedings of the IFIP Working Conference in Programming Concepts and Methods (PROCOMET’98)
Clarke R (1996) The Mondex Value-Card Scheme, chap.~4. Xamax Consultancy Pty Ltd, URL: http://www.anu.edu.au/people/Roger.Clarke/EC/Mondex.html
CoFI (2004) (The Common Framework Initiative). Casl Reference Manual. LNCS 2960 (IFIP Series). Springer, Heidelberg
Cooper D, Stepney S, Woodcock J (2002) Derivation of Z refinement proof rules: forwards and backwards rules incorporating input/output refinement. Technical Report YCS-2002-347, University of York, URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/z/zrules.htm
Derrick J, Boiten E (2001) Refinement in Z and in Object-Z : foundations and advanced applications. FACIT. Springer, Heidelberg
Dolev D, Yao AC (1981) On the security of public key protocols. In: Proceedings of the 22nd IEEE symposium on foundations of computer science, pp 350–357
Farmer WM (1994) Theory interpretation in simple type theory. In: Heering J et al (eds) Higher-order algebra, logic, and term rewriting, vol 816. Lecture Notes in Computer Science. Springer, Heidelberg
Grandy H, Haneberg D, Reif W, Stenzel K (2006) Developing provably secure M-commerce applications. In: Müller G (eds). Emerging trends in information and communication security, vol 3995 of LNCS. Springer, Heidelberg, pp 115–129
Grandy H, Moebius N, Bischof M, Haneberg D, Schellhorn G, Stenzel K, Reif W (2006) The Mondex case study: from specifications to code. Technical Report 2006-31, University of Augsburg, URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications
Grandy H, Stenzel K, Reif W (2005) Object-oriented verification Kernels for secure Java applications. In: Aichering B, Beckert B (eds) SEFM 2005—3rd ieee international conference on software engineering and formal methods
Grandy H, Stenzel K, Reif W (2006) A refinement method for Java programs. Technical Report 2006-29, University of Augsburg URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications
Grandy H, Stenzel K, Reif W (2007) A refinement method for Java programs. In: Formal methods for open object-based distributed systems, vol 4468 of Lecture Notes in Computer Science. Springer, Heidelberg
Gurevich Y (1995) Evolving algebras 1993: Lipari guide. In: Börger E (eds) Specification and validation methods. Oxford University Press, Oxford, pp 9–36
Haneberg D (2006) Sicherheit von Smart Card—Anwendungen (in German). PhD thesis, University of Augsburg, Augsburg, Germany
Haneberg D, Grandy H, Reif W, Schellhorn G (2005) Verifying security protocols: an ASM approach. In: Beauquier D, Börger E, Slissenko A (eds) 12th International workshop on abstract state machines, ASM 05. University Paris 12, Val de Marne, Créteil, France
Haneberg D, Grandy H, Reif W, Schellhorn G (2007) Verifying smart card applications: an ASM approach. In: Gibbons J, Davies J (eds) Proceedings of the international conference on integrated formal methods (iFM) 2007, vol 4591 of LNCS. Springer, Heidelberg, pp 313–332
Jifeng H, Hoare CAR, Sanders JW (1986) Data refinement refined. In: Robinet B, Wilhelm R (eds) Proceedings of ESOP 86, vol 213 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 187–196
Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT, Cambridge
Jürjens J (2002) UMLsec: Extending UML for secure systems development. In: Jézéquel J-M, Hussmann H, Cook S (eds) UML 2002—The Unified Modeling Language 5th International Conference, Dresden, Germany, Springer, LNCS 2460
Jürjens J (2005) Secure systems development with UML. Springer, Heidelberg, ISBN: 3-540-00701-6
Web presentation of the mondex case study in KIV, URL: http://www.informatik.uni-augsburg.de/swt/projects/mondex.html
Kong W, Ogata K, Futatsugi K (2007) Algebraic approaches to formal analysis of the mondex electronic purse system. In: Gibbons J, Davies J (eds) Proceedings of the international conference on integrated formal methods (iFM) 2007, vol 4591 of LNCS. Springer, Heidelberg, pp 393–412
Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Tools and algorithms for the construction and analysis of systems (TACAS), vol 1055. Springer, Berlin
Marrero W, Clarke E, Jha S (1997) A model checker for authentication protocols. In: Proceedings of the DIMACS workshop on design and formal verication of security protocols
Moebius N, Haneberg D, Schellhorn G, Reif W (2007) A modeling framework for the development of provably secure E-Commerce applications. In: Proceedings of the international conference on software engineering advances 2007. IEEE Computer Society Press (accepted for publication)
Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur. 6
Paulson LC (1999) Inductive analysis of the Internet protocol TLS. ACM Trans Inf Syst Secur 2(3):332–351
Paulson LC (2001) Verifying the SET protocol. In: Gore R, Leitsch A, Nipkow T (eds) IJCAR 2001: international joint conference on automated reasoning, Siena, Italy. Springer, LNCS 2083
Ramananadro T, Jackson D (2006) Mondex, an electronic purse: specification and refinement checks with the alloy model-finding method, URL: http://www.eleves.ens.fr/home/ramanana/work/mondex
Ryan PYA, Schneider SA, Goldsmith MH, Lowe G, Roscoe B (2001) The modelling and analysis of security protocols: the CSP approach. Addison-Wesley, Reading
Reif W, Schellhorn G, Stenzel K, Balser M (1998) Structured specifications and interactive proofs with KIV. In: Bibel W, Schmitt P (eds) Automated deduction—a basis for applications, vol II: Systems and implementation techniques, Chap. 1: Interactive theorem proving. Kluwer, Dordrecht, pp 13–39
Schellhorn G, Ahrendt W (1997) Reasoning about abstract state machines: The WAM case study. J Univer Comput Sci (J.UCS) 3(4):377–413, URL: http://www.jucs.org
Schellhorn G, Ahrendt W (1998) The WAM case study: verifying compiler correctness for prolog with KIV. In: Bibel W, Schmitt P (eds) Automated deduction—a basis for applications. Kluwer, Dordrecht, pp 165–194
Song D, Berezin S, Perrig A (2001) Athena: a novel approach to efficient automatic security protocol analysis. J Comput Secur (Special Issue CSFW12) 9(1,2):47–74
Schellhorn G (1999) Verification of abstract state machines. PhD thesis, Universität Ulm, Fakultät für Informatik, URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications
Schellhorn G (2001) Verification of ASM refinements using generalized forward simulation. J Univ Comput Sci (J.UCS), 7(11):952–979, URL: http://www.jucs.org
Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. J Theor Comput Sci 336(2–3):403–435
Stepney S, Cooper D, Woodcock J (2000) An electronic purse specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory, URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/z/monog.htm
Schellhorn G, Grandy H, Haneberg D, Moebius N, Reif W (2007) A systematic verification approach for mondex electronic purses using ASMs. In: Glässer U, Abrial J-R (ed) Proceedings of the Dagstuhl seminar on rigorous methods for software construction and analysis, LNCS. Springer, Heidelberg (accepted, older version available as Techn. Report 2006-27 at [KIV])
Schellhorn G, Grandy H, Haneberg D, Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. In: Misra J, Nipkow T, Sekerinski E (eds) Formal methods 2006, Proceedings, vol 4085 of LNCS. Springer, Heidelberg, pp 16–31
Schellhorn G, Grandy H, Haneberg D, Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. Technical Report 2006-2, Universität Augsburg
Michael Spivey J (1992) The Z notation: a reference manual. International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs
Stenzel K (2004) A formally verified calculus for full Java card. In: Rattray C, Maharaj S, Shankland C (eds) Algebraic methodology and software technology (AMAST) 2004, Proceedings, Stirling Scotland. Springer, LNCS 3116
Thums A, Ortmeier F, Reif W, Schellhorn G (2004) Interactive verification of statecharts. In: Ehrig H (ed) Integration of software specification techniques for applications in engineering Springer, LNCS 3147, pp 355–373
Woodcock JCP, Davies J (1996) Using Z: Specification, proof and refinement. International Series in Computer Science. Prentice Hall, Englewood Cliffs
Woodcock J, Freitas L (2006) Z/eves and the mondex electronic purse. In: Cerone A, Barkaoui K, Cavalcanti A (eds) Theoretical aspects of computing—ICTAC 2006, 3rd international colloquium, LNCS 4281 Tunis. Springer, Heidelberg, pp 14–34
Zarba CG (1998) Model checking the Needham–Schroeder protocol, URL: http://www-step.stanford.edu/case-studies/security
Author information
Authors and Affiliations
Corresponding author
Additional information
J. C. P. Woodcock
Rights and permissions
About this article
Cite this article
Haneberg, D., Schellhorn, G., Grandy, H. et al. Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Form Asp Comp 20, 41–59 (2008). https://doi.org/10.1007/s00165-007-0057-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-007-0057-0