Composition of password-based protocols
Composition of password-based protocols
复制标题
基于密码的协议的组成
DOI：
10.1007/s10703-013-0184-6
复制
发表时间：
2013
影响因子：
0.8
通讯作者：
Chevalier C
中科院分区：
文献类型：
--
作者：
Chevalier C
形式化和符号化技术对于安全协议的建模和分析非常有用。它们有助于提高我们对此类协议的理解，使我们能够发现缺陷，并且还为协议设计提供支持。然而，这种分析通常认为协议是隔离执行的，或者假设协议会话的数量有限。因此，当协议在更复杂的环境中执行时，不提供安全保证。在本文中，我们研究了在重复使用相同密码的情况下，密码协议是否可以安全地组合。更准确地说，我们提出了一种转换，将对单个协议会话安全的密码协议（一个可确定的问题）映射为对无限数量的会话安全的协议。我们的研究结果提供了一个有效的策略来设计安全的密码协议：(i)设计一个协议旨在确保一个协议会话的安全；（ii）应用我们的变换，得到一个对无限会话数安全的协议。我们的技术也适用于组合不同的密码协议，使我们能够获得协议间和会话间的组合。
Formal and symbolic techniques are extremely useful for modelling and analysing security protocols. They have helped to improve our understanding of such protocols, allowed us to discover flaws, and they also provide support for protocol design. However, such analyses usually consider that the protocol is executed in isolation or assume a bounded number of protocol sessions. Hence, no security guarantee is provided when the protocol is executed in a more complex environment.In this paper, we study whether password protocols can be safely composed, even when a same password is reused. More precisely, we present a transformation which maps a password protocol that is secure for a single protocol session (a decidable problem) to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure password protocols: (i) design a protocol intended to be secure for one protocol session; (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. Our technique also applies to compose different password protocols allowing us to obtain both inter-protocol and inter-session composition.