This paper extends previous efforts carried out by Abadi and Blanchet toward the use of type systems to analyze security protocols. Some classic work on information flow security relies on assigning security classes to objects. A crucial point is to guarantee that no information may flow from higher to lower classes, thus preventing security leakages. The underlying idea here is somewhat similar, though the notion of a security class is formalized as a “type,” much in the same way that type is formalized in a programming language. From a security point of view, useful types are “public,” “secret,” and “any.” Each object--a key, a communication channel, or any other piece of information--is assigned a type, and rules of composability are provided for typing a complex object composed of simpler units of data. At the core of this approach, there is a general type system for a process algebra that extends the classic pi calculus. It is supported by a main theorem that states that well-typed processes preserve the secrecy of any value of level “any,” namely, they do not reveal secrets.
This work is, in my opinion, a sound contribution to the field. Nevertheless, I find the second part of the paper even more revealing, where the authors establish a connection between typed process calculus and a completely different approach: logic programs. Traditionally, logic schemes rely on a symbolic analysis that has been fully disconnected from the process calculus approach. The authors prove the equivalence of both approaches, a result of great interest.
To the best of my knowledge, this is one of the few works that tries to explore the relationships among the different frameworks for specifying and reasoning about security properties in protocols. I think understanding these relationships may be highly useful, for example, in interpreting the implications of the important results of one system on another.