{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:58:21Z","timestamp":1748350701338},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-007-0057-0","type":"journal-article","created":{"date-parts":[[2007,12,7]],"date-time":"2007-12-07T10:52:08Z","timestamp":1197024728000},"page":"41-59","source":"Crossref","is-referenced-by-count":22,"title":["Verification of Mondex electronic purses with KIV: from transactions to a security protocol"],"prefix":"10.1145","volume":"20","author":[{"given":"Dominik","family":"Haneberg","sequence":"first","affiliation":[{"name":"Lehrstuhl f\u00fcr Softwaretechnik und Programmiersprachen, Universit\u00e4t Augsburg, D-86135, Augsburg, Germany"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[{"name":"Lehrstuhl f\u00fcr Softwaretechnik und Programmiersprachen, Universit\u00e4t Augsburg, D-86135, Augsburg, Germany"}]},{"given":"Holger","family":"Grandy","sequence":"additional","affiliation":[{"name":"Lehrstuhl f\u00fcr Softwaretechnik und Programmiersprachen, Universit\u00e4t Augsburg, D-86135, Augsburg, Germany"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[{"name":"Lehrstuhl f\u00fcr Softwaretechnik und Programmiersprachen, Universit\u00e4t Augsburg, D-86135, Augsburg, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Burrows M Abadi M Needham R (1990) A logic of authentication. ACM Trans Comput Syst 8(1)","DOI":"10.1145\/77648.77649"},{"key":"e_1_2_1_2_2_2","volume-title":"Advances in Cryptology\u2014Crypto 96 Proceedings, vol 1109 of LNCS","author":"Bellare M","year":"1996"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.4.549"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Boiten E Derrick J Schellhorn G (2007) Relational concurrent refinement part ii: intenral operations and ouputs. FAC (under consideration)","DOI":"10.1016\/j.entcs.2006.08.043"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Basin D M\u00f6dersheim S Vigan\u00f2 L (2003) An on-the-fly model-checker for security protocol analysis. In: Proceedings of Esorics\u201903 LNCS 2808 Springer Heidelberg pp 253\u2013270","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0012-7"},{"key":"e_1_2_1_2_7_2","first-page":"20","volume-title":"Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence 11","author":"B\u00f6rger E","year":"1995"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Carlsen U (1994) Generating formal cryptographic protocol specifications. In: IEEE Symposium on Research in Security and Privacy. IEEE Computer Society pp 137\u2013146","DOI":"10.1109\/RISP.1994.296586"},{"key":"e_1_2_1_2_10_2","unstructured":"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"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"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\u201998)","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"e_1_2_1_2_12_2","unstructured":"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"},{"key":"e_1_2_1_2_13_2","unstructured":"CoFI (2004) (The Common Framework Initiative). C asl Reference Manual. LNCS 2960 (IFIP Series). Springer Heidelberg"},{"key":"e_1_2_1_2_14_2","unstructured":"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"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and in Object-Z : foundations and advanced applications. FACIT","author":"Derrick J","year":"2001"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"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\u2013357","DOI":"10.1109\/SFCS.1981.32"},{"key":"e_1_2_1_2_17_2","volume-title":"Higher-order algebra, logic, and term rewriting, vol 816. Lecture Notes in Computer Science","author":"Farmer WM","year":"1994"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/11766155_9","volume-title":"Emerging trends in information and communication security, vol 3995 of LNCS","author":"Grandy H","year":"2006"},{"key":"e_1_2_1_2_19_2","unstructured":"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"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Grandy H Stenzel K Reif W (2005) Object-oriented verification Kernels for secure Java applications. In: Aichering B Beckert B (eds) SEFM 2005\u20143rd ieee international conference on software engineering and formal methods","DOI":"10.1109\/SEFM.2005.28"},{"key":"e_1_2_1_2_21_2","unstructured":"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"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-540-72952-5_14"},{"key":"e_1_2_1_2_23_2","first-page":"9","volume-title":"Specification and validation methods","author":"Gurevich Y","year":"1995"},{"key":"e_1_2_1_2_24_2","unstructured":"Haneberg D (2006) Sicherheit von Smart Card\u2014Anwendungen (in German). PhD thesis University of Augsburg Augsburg Germany"},{"key":"e_1_2_1_2_25_2","unstructured":"Haneberg D Grandy H Reif W Schellhorn G (2005) Verifying security protocols: an ASM approach. In: Beauquier D B\u00f6rger E Slissenko A (eds) 12th International workshop on abstract state machines ASM 05. University Paris 12 Val de Marne Cr\u00e9teil France"},{"key":"e_1_2_1_2_26_2","first-page":"313","volume-title":"Proceedings of the international conference on integrated formal methods (iFM) 2007, vol 4591 of LNCS","author":"Haneberg D","year":"2007"},{"key":"e_1_2_1_2_27_2","first-page":"187","volume-title":"Proceedings of ESOP 86, vol 213 of Lecture Notes in Computer Science","author":"Jifeng H","year":"1986"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/557365"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2002) UMLsec: Extending UML for secure systems development. In: J\u00e9z\u00e9quel J-M Hussmann H Cook S (eds) UML 2002\u2014The Unified Modeling Language 5th International Conference Dresden Germany Springer LNCS 2460","DOI":"10.1007\/3-540-45800-X_32"},{"key":"e_1_2_1_2_30_2","unstructured":"J\u00fcrjens J (2005) Secure systems development with UML. Springer Heidelberg ISBN: 3-540-00701-6"},{"key":"e_1_2_1_2_31_2","unstructured":"Web presentation of the mondex case study in KIV URL: http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/mondex.html"},{"key":"e_1_2_1_2_32_2","first-page":"393","volume-title":"Proceedings of the international conference on integrated formal methods (iFM) 2007, vol 4591 of LNCS","author":"Kong W","year":"2007"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/3-540-61042-1_43"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.21236\/ADA327281"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/ICSEA.2007.7"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur. 6","DOI":"10.3233\/JCS-1998-61-205"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_2_1_2_38_2","unstructured":"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"},{"key":"e_1_2_1_2_39_2","unstructured":"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"},{"key":"e_1_2_1_2_40_2","volume-title":"The modelling and analysis of security protocols: the CSP approach","author":"Ryan PYA","year":"2001"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Reif W Schellhorn G Stenzel K Balser M (1998) Structured specifications and interactive proofs with KIV. In: Bibel W Schmitt P (eds) Automated deduction\u2014a basis for applications vol II: Systems and implementation techniques Chap. 1: Interactive theorem proving. Kluwer Dordrecht pp 13\u201339","DOI":"10.1007\/978-94-017-0435-9_1"},{"issue":"4","key":"e_1_2_1_2_42_2","first-page":"377","article-title":"Reasoning about abstract state machines: The WAM case study","volume":"3","author":"Schellhorn G","year":"1997","journal-title":"J Univer Comput Sci (J.UCS)"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-94-017-0437-3_7","volume-title":"Automated deduction\u2014a basis for applications","author":"Schellhorn G","year":"1998"},{"issue":"1","key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","article-title":"Athena: a novel approach to efficient automatic security protocol analysis","volume":"9","author":"Song D","year":"2001","journal-title":"J Comput Secur (Special Issue CSFW"},{"key":"e_1_2_1_2_45_2","unstructured":"Schellhorn G (1999) Verification of abstract state machines. PhD thesis Universit\u00e4t Ulm Fakult\u00e4t f\u00fcr Informatik URL: http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications"},{"key":"e_1_2_1_2_46_2","unstructured":"Schellhorn G (2001) Verification of ASM refinements using generalized forward simulation. J Univ Comput Sci (J.UCS) 7(11):952\u2013979 URL: http:\/\/www.jucs.org"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"e_1_2_1_2_48_2","unstructured":"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"},{"key":"e_1_2_1_2_49_2","unstructured":"Schellhorn G Grandy H Haneberg D Moebius N Reif W (2007) A systematic verification approach for mondex electronic purses using ASMs. In: Gl\u00e4sser 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\u00a0at [KIV])"},{"key":"e_1_2_1_2_50_2","first-page":"16","volume-title":"Formal methods 2006, Proceedings, vol 4085 of LNCS","author":"Schellhorn G","year":"2006"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Grandy H Haneberg D Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. Technical Report 2006-2 Universit\u00e4t Augsburg","DOI":"10.1007\/11813040_2"},{"key":"e_1_2_1_2_52_2","volume-title":"The Z notation: a reference manual. International Series in Computer Science","author":"Michael Spivey J","year":"1992","edition":"2"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-540-27815-3_37"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"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\u2013373","DOI":"10.1007\/978-3-540-27863-4_20"},{"key":"e_1_2_1_2_55_2","volume-title":"Using Z: Specification, proof and refinement. International Series in Computer Science","author":"Woodcock JCP","year":"1996"},{"key":"e_1_2_1_2_56_2","first-page":"14","volume-title":"Theoretical aspects of computing\u2014ICTAC 2006, 3rd international colloquium, LNCS 4281 Tunis","author":"Woodcock J","year":"2006"},{"key":"e_1_2_1_2_57_2","unstructured":"Zarba CG (1998) Model checking the Needham\u2013Schroeder protocol URL: http:\/\/www-step.stanford.edu\/case-studies\/security"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0057-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0057-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0057-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:48:58Z","timestamp":1641484138000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0057-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["10.1007\/s00165-007-0057-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0057-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1]]}}}