Abstract

In the 1990s platform seven (then part of National Westminster Bank) started developing a smartcard electronic cash system, Mondex, to the highest ITSEC security certification level, E6. Logica developed the required Z specifications of the security policy and architectural design, and the proof of correspondence between them.

Once it became clear that E6 would be achievable for Mondex, the decision was taken to develop Multos, a smartcard operating system that allows several applications to be securely co-hosted on a single card, also too E6. Logica again handled the formal methods development.

In 1999 both Mondex and Multos achieved ITSEC level E6 certification.

@journal(SS-BCS,
  author = "Susan Stepney",
  title = "New Horizons in Formal Methods",
  journal = "The Computer Bulletin",
  pages = "24-26",
  month = jan,
  publisher = "BCS",
  year = 2001
)