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.
BSD License

Topics

Theories of HotelKeyCards