@inproceedings{3a54bdf943444da3819af6ae5872be5a,
title = "Verifying a hotel key card system",
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.",
author = "Tobias Nipkow",
year = "2006",
doi = "10.1007/11921240_1",
language = "English",
isbn = "3540488154",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "1--14",
booktitle = "Theoretical Aspects of Computing - ICTAC 2006 Third International Colloquium, Proceedings",
note = "Third International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings ; Conference date: 20-11-2006 Through 24-11-2006",
}