Heuristic Methods for Security Protocols

Security protocols present many interesting challenges from both pragmatic and theoretical points of view as they are ubiquitous and pose many theoretical challenges despite their apparent simplicity. One of the most interesting aspects of security protocols is the complexity of the verification algorithms to check their correctness; in fact, under many models of the intruder, correctness is undecidable and/or computationally hard [15, 12, 11, 26].Many authors have formalised security protocols in terms of process calculi suitable to define many verification frameworks (besides model checking, path analysis, static analysis, etc.) [21, 1, 7, 8]. Model checking (MC) techniques have been exploited in the design and implementation of automated tools [13, 23] and symbolic techniques have been proposed to tackle the state explosion problem [3, 9, 10, 18].This paper promotes the use of directed MC in security protocols. We define a heuristic based on the logic formulae formalising the security properties of interest and we show how such heuristic may drive the search of an attack path. Specifically, we represent the behaviour of a security protocol in the context of the (symbolic) MC framework based on the cIP and PL, respectively a cryptographic process calculus and a logic for specifying security properties introduced in [18]. An original aspect of this framework is that it allows to explicitly represent instances1 of participants and predicate over them.Intuitively, the heuristic ranks the nodes and the edges of the state space by inspecting (the syntactical structure of the) formula expressing the security property of interest. More precisely, the state space consists of the transition system representing possible runs of a protocol; our heuristic weights states and transitions considering the instances of principals that joined the context and how they are quantified in the security formula. Weights are designed so that most promising paths are tried before other less promising directions. Rather interestingly, the heuristic can rule out a portion of the state space by exploring only a part of it. In fact, we also show that the heuristic may possibly cut some directions as they cannot lead to attacks; in fact, the heuristic is proved to be correct, namely no attacks can be found in the portion of the state space cut by our heuristic.