A New Knowledge Representation Strategy for Cryptographic Protocol Analysis

The formal verifiation of security properties of a cryptographic protocol is a diffcult, albeit very important task as more and more sensible resources are added to public networks. This paper is focused on model checking; when adopting this approach to the problem, one challenge is to represent the intruder's knowledge in an effective way. We present an intruder's knowledge representation strategy that supports the full term language of spi calculus and does not pose artificial restrictions, such as atomicity or limited maximum size, to language elements. In addition, our approach leads to practical implementation because the knowledge representation is incrementally computable and is easily amenable to work with various term representation languages.