Knowledge flow analysis offers a simple and flexible way to find flaws in security protocols. A protocol is described by a collection of rules constraining the propagation of knowledge amongst principals. Because this characterization corresponds closely to informal descriptions of protocols, it allows a succinct and natural formalization; because it abstracts away message ordering, and handles communications between principals and applications of cryptographic primitives uniformly, it is readily represented in a standard logic. A generic framework in the Alloy modelling language is presented, and instantiated for two standard protocols, and a new key management scheme.
@cite_16: Abstract: We investigate the complexity of the protocol insecurity problem for a finite number of sessions (fixed number of interleaved runs). We show that this problem is NP-complete in a Dolev-Yao model of intruders. The result does not assume a limit on the size of messages and supports nonatomic symmetric encryption keys. We also prove that in order to build an attack with a fixed number of sessions the intruder needs only to forge messages of polynomial size, provided that they are represented as dags.
@cite_23: We formalize the Dolev-Yao model of security protocols, using a notation based on multiset rewriting with existentials. The goals are to provide a simple formal notation for describing security protocols, to formalize the assumptions of the Dolev-Yao model using this notation, and to analyze the complexity of the secrecy problem under various restrictions. We prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP-complete class when the number of nonces is restricted, and an NP-complete class when both the number of nonces and the number of roles is restricted. We point out a remaining open complexity problem, and discuss the implications these results have on the general topic of protocol analysis.
Our formalism derives its simplicity from being just sufficiently expressive to enable modelling of practical cryptographic protocols. In particular, existentials @cite_23 cannot be encoded as knowledge flows; existentials are implicitly modeled in Oscar's initial knowledge. As mentioned in Section ), NP-hardness proofs which use (existential) Horn clause reduction @cite_23 or SAT3 reduction @cite_16 are not applicable to Knowledge Flow Analysis.