Foundations of Security Protocol Analysis

Abstract

One of the central problems in the automatic verification of security protocols is that of verifying whether a given protocol leaks secrets or not. It identifies syntactic subclasses of protocols for which the secrecy problem is decidable. It also concerns reasoning about protocols. The author introduces a logic using which interesting properties of protocols can be specified and reasoned about. A formal model of security protocols is set up, and several important properties about the model are proved. In particular the properties relating to synth and anlz proofs which formalise the way the agents running a protocol derive new information from the old. The secrecy problem is considered and shown that it is undecidable both when the set of nonces is infinite and when the length of messages is unbounded. Relatively simple and uniform proofs for both these results are proved. Then the secrecy problem is considered in the setting of infintely many nonces, but bounded message length. It is proved that for a syntactic subclass of protocols called 'tagged protocols' the secrecy problem in this setting is decidable. It is also proved that the tagged protocol has a leaky run iff it has a leaky run containing only bounded length messages; And further the secrecy problem for tagged protocols is decidable even in the setting where both message length and number of nonces is unbounded. About reasoning, a logic is defined in which one can easily specify several interesting security properties like secrecy, authenticity, etc., Some examples are given to illustrate how to reason about protocols. Some of the undecidability and decidability results are extended to the verification problem of logic.