Verifying a hotel key card system

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

12 Scopus 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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2006 Third International Colloquium, Proceedings
PublisherSpringer Verlag
Pages1-14
Number of pages14
ISBN (Print)3540488154, 9783540488156
DOIs
StatePublished - 2006
EventThird International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings - Tunis, Tunisia
Duration: 20 Nov 200624 Nov 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4281 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThird International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings
Country/TerritoryTunisia
CityTunis
Period20/11/0624/11/06

Fingerprint

Dive into the research topics of 'Verifying a hotel key card system'. Together they form a unique fingerprint.

Cite this