Verifying a Hotel Key Card System

DOI10.1007/11921240_1MaRDI QIDQ3525136zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow

Publication date 11 September 2008

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

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

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1950634
• Keyless Authentication and Authenticated Capacity
• Session key distribution using smart cards
• Integrating smart cards into authentication systems
• An automatically verified prototype of the Tokeneer ID station specification

Cited in

(8)

• Formally verified algorithms for upper-bounding state space diameters
• Verified over-approximation of the diameter of propositionally factored transition systems
• Hotel Key Card
• Monotonicity inference for higher-order formulas
• Monotonicity inference for higher-order formulas
• AI Planning Languages Semantics
• Verified SAT-Based AI Planning
• Upper Bounding Diameters of State Spaces of Factored Transition Systems

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle/Isar

This page was built for publication: Verifying a Hotel Key Card System

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