Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/s00165-007-0060-5 | Formal Asp. Comput. |
Keywords | Field | DocType |
international grand challenge,refinement,verified software repository,smart cards,security,grand challenge in verified software,formal model,grand challenges,paper record,theorem proving,itsec level e6,electronic finance,certification,verified software,verification,mondex,z notation,original project,pilot project,mondex electronic purse,correctness,highest level,smart card | Z notation,Computer science,Computer security,Automated theorem proving,Correctness,Smart card,Grand Challenges,Mathematical proof,Certification,ITSEC | Journal |
Volume | Issue | ISSN |
20 | 1 | 1433-299X |
Citations | PageRank | References |
13 | 0.81 | 14 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jim Woodcock | 1 | 357 | 25.74 |
| Susan Stepney | 2 | 813 | 113.21 |
| David Cooper | 3 | 13 | 0.81 |
| John A. Clark | 4 | 110 | 7.93 |
| Jeremy Jacob | 5 | 147 | 13.65 |