Lazy infinite-State analysis of security protocols

Abstract

Security protocols are used to exchange information in a distributed system with the aim of providing security guarantees. We present an approach to modeling security protocols using lazy data types in a higher-order functional programming language. Our approach supports the formalization of protocol models in a natural and high-level way, and the automated analysis of safety properties using infinite-state model checking, where the model is explicitly constructed in a demand- driven manner. We illustrate these ideas with an extended example: modeling and checking the Needham-Schroeder public-key authentication protocol.