Using Formal Methods to Cultivate Trust in Smart Card Operating Systems

Marjan I. Alberda, Pieter H. Hartel, Eduard K. de Jong

    Research output: Contribution to journalArticleAcademicpeer-review

    1 Citation (Scopus)
    94 Downloads (Pure)


    To be widely accepted, smart cards must contain completely trustworthy software. Because smart cards contain relatively simple computers, and are used only for a specific class of applications, it is feasible to make the language used to program the software components focused and tiny. Formal methods can be used to precisely specify this language and to reason about properties of the language, which results in more trustworthy software. We explore this process by specifying the core of a proprietary systems programming language for smart card operating systems. We show how the specification obtained is used in proofs, and in the development of tool support.
    Original languageUndefined
    Pages (from-to)39-54
    Number of pages16
    JournalFuture generation computer systems
    Issue number1
    Publication statusPublished - Jul 1997


    • EWI-1069
    • SCS-Cybersecurity
    • IR-55697

    Cite this