所有权认证传输协议安全属性的形式化验证

在普适计算设备中，用户倾向于在设备中存储一些有价值的信息。即使设备可以被其他用户临时借用，但借用或出借设备对任何用户来说都不安全，因为这可能导致用户的私人数据公开。为了保护用户数据并维护用户隐私，我们提出并建模了所有权认证传输技术。愿意出售设备的用户必须转移待售设备的所有权。一旦设备售出且所有权已转移，原所有者将无法以任何代价使用该设备。如果所有权转移过程未正确执行，任何一方用户都无法使用该设备。这也涵盖了设备被盗或丢失的情形，从而避免了伪装攻击。本文旨在对提出的所有权认证传输协议的基本过程进行建模，并通过使用 CSP 和模型检查方法表示该过程来检查其安全属性。对于模型检查，我们使用了一种名为 NuSMV 的符号模型检查工具。所有权传输协议的安全属性已用 CTL 规范进行建模，观察结果表明该系统满足所有协议约束且部署安全。