Name
Abstract | ||
|---|---|---|
This paper discusses a case study in formal verification and development of secure smart card applications. An elementary Java Card electronic purse applet is presented whose specification can be simply formulated as “in normal operation, the applet’s balance field can only be decreased, never increased”. The applet features a challenge-response mechanism which allows legitimate terminals to increase the balance by putting the applet into a special operation mode. A systematic approach is used to guarantee a secure flow of control within the applet: appropriate transition properties are first formalized as a finite state machine, then incorporated in the specification, and finally formally verified using the Loop translation tool and the PVS theorem prover. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.jlap.2003.07.007 | The Journal of Logic and Algebraic Programming |
Keywords | Field | DocType |
Smart card,Java,Applet verification,Security | Programming language,Computer science,Source code,Control flow,Automated theorem proving,Smart card,Finite-state machine,Java Card,Java applet,Operating system,Formal verification | Journal |
Volume | Issue | ISSN |
58 | 1 | 1567-8326 |
Citations | PageRank | References |
6 | 0.89 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| B. Jacobs | 1 | 1046 | 100.09 |
| Martijn Oostdijk | 2 | 132 | 13.89 |
| Martijn Warnier | 3 | 236 | 27.43 |