A framework for cryptographic protocol analysis using linear temporal logic

In this paper, a framework for cryptographic protocol analysis using linear temporal logic is proposed. This framework can be used to specify and analyse security protocols. It aims to prove the correctness of the security properties of protocols. The framework extends the linear temporal logic by including the knowledge of participants in each status which may change over the time. The ability of the framework is demonstrated by analysing the Needham-Schroeder public key protocol as an example.