A calculus of challenges and responses

er presents a novel approach for concisely abstracting authentication s and for subsequently analyzing those abstractions in a sound manner, i.e., deriving authentication guarantees for protocol abstractions suffices for prove guarantees for the actual protocols. The abstractions are formalized in a lculus which constitutes a higher-level abstraction of the ρ-spi calculus and is specifically tailored towards reasoning about challenge-response mechanisms within authentication protocols. Furthermore, it allows for expressing protocols without having to include details on the specific structure of exchanged messages. This in particular entails that many authentication protocols share a common abn so that a single validation of this abstraction already gives rise to security es for all these protocols. Such an abstract validation can be automatically performed using static analysis techniques based on an effect system proposed in er. Finally, extensions to abstractions of additional p...

• Type: Conference
• Year: 2007
• Where: CCS
• Authors: Michael Backes, Agostino Cortesi, Riccardo Focardi, Matteo Maffei
• Keywords: Abstractions, Authentication Protocols, CCS 2007, Protocol Abstractions Suffices, Security Privacy