X-Men: A Mutation-Based Approach for the Formal Analysis of Security Ceremonies
X-Men: A Mutation-Based Approach for the Formal Analysis of Security Ceremonies
复制标题
X 战警：基于突变的安全仪式正式分析方法
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
L. Viganò
中科院分区：
文献类型：
--
作者：
Diego Sempreboni;L. Viganò
越来越多的网络系统（例如，支付、运输、投票、关键基础设施系统），其安全性本质上依赖于人类用户。安全仪式扩展了一个安全协议，其中包含所有被认为是带外的内容，特别是包括人类用户在积极参与安全仪式时可能犯的错误。在本文中，我们介绍了一种新的方法，安全仪式的形式化分析。我们的方法定义了突变规则，模拟人类用户的可能行为，并自动生成突变的行为的其他代理人的仪式，以匹配人类引起的突变。这允许分析原始仪式规范及其可能的变化，其中可能包括仪式实际实施的方式。为了使我们的方法自动化，我们开发了工具X-Men，这是一个扩展Tamarin的原型，Tamarin是安全协议自动无界验证的最常见工具之一。作为概念验证，我们将我们的方法应用于两个现实案例研究，揭示了一些具体的漏洞。
There is an increasing number of cyber-systems (e.g., payment, transportation, voting, critical-infrastructure systems) whose security depends intrinsically on human users. A security ceremony expands a security protocol with everything that is considered out-of-band to it, including, in particular, the mistakes that human users might make when participating actively in the security ceremony. In this paper, we introduce a novel approach for the formal analysis of security ceremonies. Our approach defines mutation rules that model possible behaviors of a human user, and automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that extends Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to two real-life case studies, uncovering a number of concrete vulnerabilities.