Workshop on
Foundations of Computer Security - FCS'03
Ottawa, Canada, 26-27 June 2003
Symbolic Approach to the Analysis of Security Protocols
Stéphane Lafrance and John Mullins (École Politechnique
Montreal - Canada)
Abstract
The specification and validation of security protocols often requires viewing
function calls - like encryption/decryption and the generation of fake
messages - explicitly as actions within the process semantics. Following this
approach, this paper introduces a symbolic framework based on value-passing
processes able to handle symbolic values like fresh nonces, fresh keys, fake
address and fake messages. The main idea in our approach is to assign to each
value-passing process a formula describing the symbolic values conveyed by its
semantics. In such symbolic processes, called processes, the formulas are
drawn from a logic based on a message algebra equipped with encryption,
signature and hashing primitives. The symbolic operational semantics of a
process is then established through semantic rules updating formulas by adding
restrictions over the symbolic values, as required for the process to evolve.
We then prove that the logic required from the semantic rules is decidable.
We also define a bisimulation equivalence between processes; this amounts to a
generalisation of the standard bisimulation equivalence between (non-symbolic)
value-passing processes. Finally, we provide a complete symbolic bisimulation
method for constructing the bisimulation between processes.