Formalisation and verification of Java Card security properties in dynamic logic

DOI10.1007/978-3-540-31984-9_27MaRDI QIDQ5316441zbMATH OpenOpenAlexFDO

Authors Wojciech Mostowski

Publication date 13 September 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107062

Mathematics Subject Classification ID

Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A formally verified calculus for full Java card
• Formal verification of a commercial smart card applet with multiple tools
• A formal executable semantics of the JavaCard platform
• A dynamic logic for the formal verification of Java card programs
• Source code verification of a secure payment applet

Cited in

(20)

• Verifying OpenJDK's sort method for generic collections
• Formal methods for smart cards: an experience report
• Proof pearl: The KeY to correct and stable sorting
• A program logic for resources
• A formal executable semantics of the JavaCard platform
• Specification of a smart card operating system
• CardKt: Automated multi-modal deduction on Java cards for multi-application security
• Formal methods in context: security and Java card
• A dynamic logic for the formal verification of Java card programs
• Formal specification and verification of JavaCard's application identifier class
• Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
• A formal correspondence between offensive and defensive JavaCard virtual machines
• CardS4: Modal theorem proving on Java smardcards
• Specification and runtime verification of Java card programs
• Formal verification of a commercial smart card applet with multiple tools
• A formally verified calculus for full Java card
• Verification by Parallelization of Parametric Code
• KeY: A Formal Method for Object-Oriented Systems
• Formal verification of security properties of smart card embedded source code
• Integration of a security type system into a program logic

Describes a project that uses

Uses Software

• KRAKATOA
• ESC/Java
• KeY

This page was built for publication: Formalisation and verification of Java Card security properties in dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5316441)