Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Verification of Mondex Electronic Purses with KIV: From Transactions to Java Code

  • Speaker:   Dr  Gerhard Schellhorn  (Universitat Augsberg)
  • Host:   Richard Banach
  • 21st March 2007 at 14:15 in 1.5
Mondex electronic purses implement cashless money transfer on smartcards. To prove security, Woodcock, Stepney and Cooper developed a formal specification together with paper-and-pencil proofs for security. This allowed Mondex to become one of the first applications that were certified with the highest level E6 of ITSEC.

Recently proving security has been proposed as a challenge for theorem provers in the context of 'Grand Challenge 6'. Our group was the first to deliver a full formal verification among several other groups that took up the challenge last year using various different approaches.

Since our work was done in the context of a project with the goal to develop a framework for formal development of verified E-commerce applications (I will give some other examples) we extended the case study to the development of a proper security model and to verified JavaCard code.

My talk will give an overview over the results.
▲ Up to the top