Verifying Privacy-Type Properties in a Modular Way
Verifying Privacy-Type Properties in a Modular Way
复制标题
DOI：
10.1109/csf.2012.16
复制
发表时间：
2012-06
期刊：
影响因子：
--
通讯作者：
Myrto Arapinis;Vincent Cheval;S. Delaune
中科院分区：
文献类型：
--
作者：
Myrto Arapinis;Vincent Cheval;S. Delaune
形式化方法已经证明了它们在分析协议安全性方面的有效性。在这种情况下，在许多现代应用中扮演重要角色的隐私类型安全属性(例如投票隐私、匿名性、解链能力)是使用等价概念来形式化的。在这篇文章中，我们研究了迹等价的概念，并展示了如何以模数的方式建立这种等价关系。众所周知，当进程不共享机密时，组合工作得很好。然而，没有结果允许我们编写依赖于一些共享秘密的过程，例如长期密钥。我们证明了，即使当进程共享秘密时，只要它们满足一些合理的条件，合成也是有效的。我们的合成结果允许我们以模块化的方式证明各种基于等价的性质，并且在相当一般的环境下工作。特别是，我们考虑使用非平凡Else分支的任意密码原语和进程。作为一个例子，我们考虑了国际民航组织的电子护照标准，并展示了如何从子协议的隐私保证中获得整个应用程序的隐私保证。
Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlink ability) that play an important role in many modern applications are formalised using a notion of equivalence. In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches. As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.