Name
Abstract | ||
|---|---|---|
This paper reports on the use of the Coq proof assistant for the formal verication of applet isolation properties in Java Card technology. We focus on the conden tiality property. We show how this property is veried by the card manager and the APIs, extending our former proof addressing the Java Card virtual machine. We also show how our verication method allows to complete specications and to enhance the secure design of the platform. For instance, we describe how the proof of the integrity puts the light on a known bug. Finally, we present the benets of the use of high order modelling to handle the complexity of the system, to prove security properties and eventually to construct generic re-usable proof architectures. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/10930755_22 | TPHOLs |
Keywords | Field | DocType |
theorem proving,security.,smart card,virtual machine,java card | Programming language,Virtual machine,Confidentiality,Computer science,Automated theorem proving,Algorithm,Smart card,Java Card,Java applet,Operating system,Formal verification,Proof assistant | Conference |
Citations | PageRank | References |
13 | 0.75 | 11 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| June Andronick | 1 | 903 | 42.66 |
| Boutheina Chetali | 2 | 59 | 5.68 |
| Olivier Ly | 3 | 13 | 0.75 |