Hotel Key Card System

Tobias Nipkow 🌐

September 9, 2006

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Two models of an electronic hotel key card system are contrasted: a state based and a trace based one. Both are defined, verified, and proved equivalent in the theorem prover Isabelle/HOL. It is shown that if a guest follows a certain safety policy regarding her key cards, she can be sure that nobody but her can enter her room.

License

BSD License

Topics

Related publications

Session HotelKeyCards

Cite

× 
@article{HotelKeyCards-AFP,
  author  = {Tobias Nipkow},
  title   = {Hotel Key Card System},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2006},
  note    = {\url{https://isa-afp.org/entries/HotelKeyCards.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: