交互系统注册协议的形式化安全分析：一种方法论与案例研究
密码学与安全
2012-09-07 v2
摘要
在这项工作中，我们提出并形式化分析了CHAT-SRP（基于混沌的票据-安全注册协议），该协议为交互式和协作平台提供了一种针对经典安全问题的密码学鲁棒解决方案。具体而言，我们在保持高可用性的同时，重点关注保密性和真实性属性。在此意义上，用户被迫盲目信任系统管理员和开发者。此外，据我们所知，使用形式化方法来验证通信协议的安全属性尚未成为普遍做法。我们提出了一种方法论来填补这一空白，即分析所提出协议的安全性以及基础前提的恰当性。为此，我们提出了一种数字身份分发协议的定义和形式化评估。一旦分发，这些身份可用于验证信息的完整性和来源。我们的安全分析基于科学界广泛接受的自动安全协议验证工具及其所依据的原理。此外，假设使用完美的密码学原语，以便将分析重点放在协议消息的交换上。我们协议的主要特性是引入了票据，这些票据使用基于混沌的随机数（仅使用一次的数字）摘要和用户的个人数据创建。结合具有某些先验知识的多渠道认证方案，这些票据通过将每个注册用户与单个请求唯一关联，在整个协议过程中提供安全性。[……]
引用
@article{arxiv.1201.1134,
title = {Formal security analysis of registration protocols for interactive systems: a methodology and a case of study},
author = {Jesus Diaz and David Arroyo and Francisco B. Rodriguez},
journal= {arXiv preprint arXiv:1201.1134},
year = {2012}
}
备注
32 pages, 7 figures, 8 listings, 1 table