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.
%0 Book Section
%1 nipkow_06_verifying
%A Nipkow, Tobias
%D 2006
%J Theoretical Aspects of Computing - ICTAC 2006
%K hol 2006 b vdm
%P 1--14
%R 10.1007/11921240_1
%T Verifying a Hotel Key Card System
%U http://dx.doi.org/10.1007/11921240_1
%X 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.
@incollection{nipkow_06_verifying,
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.},
added-at = {2009-02-11T20:58:21.000+0100},
author = {Nipkow, Tobias},
biburl = {https://www.bibsonomy.org/bibtex/2a177c7759b96d0f13fccf49bb6ccd852/leonardo},
citeulike-article-id = {1822792},
doi = {10.1007/11921240_1},
interhash = {8e83c4e1fbb64a1d8b9fde71a8fd573f},
intrahash = {a177c7759b96d0f13fccf49bb6ccd852},
journal = {Theoretical Aspects of Computing - ICTAC 2006},
keywords = {hol 2006 b vdm},
pages = {1--14},
posted-at = {2007-10-26 01:13:22},
priority = {3},
timestamp = {2009-02-11T20:58:21.000+0100},
title = {Verifying a Hotel Key Card System},
url = {http://dx.doi.org/10.1007/11921240_1},
year = 2006
}