Jim Woodcock
Skip Abstract Section
Abstract
Abstract.
Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly implement the required security properties. The work has been revived recently as a pilot project for the international Grand Challenge in Verified Software. This paper records the history of the original project and gives an overview of the formal models and proofs used.
- BJP+06a Banach R, Jeske C, Poppleton M, Stepney S (2006) Retrenching the purse: finite exception logs, and validating the small. 30th Annual IEEE/NASA Software engineering workshop. Columbia, April 2006Google Scholar
- BJP+06b Banach R, Jeske C, Poppleton M, Stepney S (2006) Retrenching the purse: hashing injective CLEAR codes, and security properties. In: 2nd International symposium on leveraging applications of formal methods, verification and validation (ISoLA 2006). Cyprus, November 2006. IEEE, 2006Google Scholar
- BJP+07 Retrenching the purse: the balance enquiry quandary, and generalised and (1,1) forward refinementsFundam Inform2007771412329273Google Scholar
- BP98 Retrenchment: an engineering variation on refinement B-98. Lecture notes in computer science, vol 1393.1998HeidelbergSpringerGoogle Scholar
- BPJ+05a Banach R, Poppleton M, Jeske C, Stepney S (2005) Retrenchment and the Mondex electronic purse (extended abstract). In: Proceedings 12th international workshop on abstract state machines (ASM’05). Paris, March 2005Google Scholar
- BPJ+05b Banach R, Poppleton M, Jeske C, Stepney S (2005) Retrenching the purse: finite sequence numbers and the tower pattern. In: Proceedings FM05. Lecture notes in computer science, vol 3582. Springer, Heidelberg, pp 382–398Google Scholar
- BSC94 Z in Practice BCS Practitioners Series1994Englewood CliffsPrentice HallGoogle Scholar
- BoD05 Formal program development with approximations ZB 2005 Lecture notes in computer science vol 34552005HeidelbergSpringer374392Google Scholar
- Bur02 Burton S (2002) Automated testing of high integrity test suites from graphical specifications. Ph.D. thesis. Department of Computer science, University of YorkGoogle Scholar
- CSC05 Breaking the model: finalisation and a taxonomy of security attacks. REFINE 2005, SurreyElectron Notes Theor Comput Sci2005137222524210.1016/j.entcs.2005.04.033Google ScholarDigital Library
- CSW02 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, December, University of YorkGoogle Scholar
- CoCURL http://www.niap-ccevs.org/cc-scheme/cc_docs/Google Scholar
- DeB01 Refinement in Z and Object-Z2001HeidelbergSpringer0982.68086Google ScholarCross Ref
- Dun03 Dunne S (2003) Introducing backwards refinement into B. In: ZB2003: third international conference of B and Z Users, Turku, June 2003. Lecture notes in computer science, vol 2651, Springer, Heidlberg, pp 178–196Google Scholar
- FHD90 Flynn M, Hoverd T, Brazier D (1990) Formaliser—an interactive support tool for Z. Z UserWorkshop. In: Proceedings of the 4th annual Z user meeting, workshops in computing, Springer, Hiedelberg, pp 128–141Google Scholar
- GCH97 E6: Use of formality discussion. G3A Tape No 68. Unclassified. Government Communications Headquarters (GCHQ). 22 October 1997Google Scholar
- HHH+87 Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW et al (1987) The laws of programming. Commun ACM. 30Google Scholar
- HHS86 Data refinement refined: resume. ESOP 86. Lecture notes in computer science, vol 2131986HeidelbergSpringer187196Google Scholar
- ITS91 Information Technology Security Evaluation Criteria (ITSEC): Preliminary Harmonised Criteria. Document COM(90) 314, Version 1.2. Commission of the European Communities. June 1991Google Scholar
- Jac92 Basic theorems about securityJ Comput Secur199214385411Google ScholarDigital Library
- SCP+03 Srivratanakul J, Clark J, Polack F, Stepney S (2003) Challenging formal specifications with mutation: a CSP security example. 12th IEEE Asia Pacific Software Engineering Conference (APSEC)Google Scholar
- SCW00 Stepney S, Cooper D, Woodcock J (2000) An electronic purse: specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory, July 2000Google Scholar
- SCW98 Stepney S, Cooper D, Woodcock J (1998) More powerful Z data refinement: pushing the state of the art in industrial refinement. In: ZUM ’98: 11th international conference of Z users, Berlin, September 1998. Lecture notes in computer science, vol 1493. Springer, Heidelberg, pp 284–307Google Scholar
- SFT03 Stepney S, Polack F, Toyn I (2003) Patterns to guide practical refactoring: examples targetting promotion in Z. In: ZB2003: third international conference of B and Z Users, Turku, June 2003. Lecture notes in computer science, vol 2651. Springer, Heidelberg, pp 20–39Google Scholar
- Spi92a Spivey JM (1992) The Z Notation: a reference manual, 2nd edn. http://spivey.oriel.ox.ac.uk/~mike/fuzzGoogle Scholar
- Spi92b The fUZZ Manual. Computer Science Consultancy19922Englewood CliffPrentice HallGoogle Scholar
- Ste01 Stepney S (2001) New horizons in formal methods. The Computer Bulletin, pp 24–26. BCS, January 2001Google Scholar
- Ste98 Stepney S (1998) A tale of two proofs. BCS-FACS third Northern formal methods workshop, Ilkley, September 1998. Electronic Workshops in ComputingGoogle Scholar
- WoD96 Using Z: specification, refinement, and proof1996Englewood CliffPrentice Hall0855.68060Google ScholarDigital Library
Index Terms
- The certification of the Mondex electronic purse to ITSEC Level E6
Index terms have been assigned to the content through auto-classification.
Recommendations
Mechanising Mondex with Z/Eves
AbstractWe describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original LaTEX sources without changing their ...
Z/Eves and the mondex electronic purse
ICTAC'06: Proceedings of the Third international conference on Theoretical Aspects of ComputingWe describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original ${\sc L^{A}T_{E}X}$ sources, without changing ...
Specification, proof, and model checking of the Mondex electronic purse using RAISE
AbstractThis paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, ...
Comments