Sciweavers

Share
CSFW
2007
IEEE

LTL Model Checking for Security Protocols

9 years 2 months ago
LTL Model Checking for Security Protocols
Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. By using our approach we have been able to formalise all the a...
Alessandro Armando, Roberto Carbone, Luca Compagna
Added 02 Jun 2010
Updated 02 Jun 2010
Type Conference
Year 2007
Where CSFW
Authors Alessandro Armando, Roberto Carbone, Luca Compagna
Comments (0)
books