Verifying a Hotel Key Card System
Verifying a Hotel Key Card System
复制标题
验证酒店钥匙卡系统
DOI：
10.1007/11921240_1
复制
发表时间：
2006
影响因子：
2
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
T. Nipkow
对比了两种电子酒店门卡系统模型：基于状态的和基于轨迹的。在定理证明器Isabelle/HOL中对两者进行了定义、验证和证明是等价的。结果表明，如果客人对她的钥匙卡遵守一定的安全政策，她可以确保除了她自己之外没有人可以进入她的房间。
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.