Title :
Analysis of cryptographic protocols using LTL of knowledge
Author :
Shigong, Long ; Lijun, Wang
Author_Institution :
Dept. of Comput. Sci., Guizhou Univ., Guiyang, China
Abstract :
In this paper, we present how the LTL (Linear Temporal Logic) language can be used to specify security protocols and discuss the analysis process using LTL. To illustrate the feasibility of our approach, we analyse the Needham-Schroeder public-key protocol and reproduce the error found by Gavin Lowe. We also extend LTL and we use LTL of knowledge to reason about situations where the knowledge of an agent is important, and where change may occur in this knowledge over time. In the end, we discuss some possible directions for future work.
Keywords :
cryptographic protocols; public key cryptography; temporal logic; Needham-Schroeder public-key protocol; cryptographic protocols; linear temporal logic language; security protocols; Computer errors; Computer science; Computer security; Cryptographic protocols; Data security; Logic; Natural languages; Public key; Public key cryptography; Specification languages; Cryptopgraphic Protocol; Knowledge; Linear Temporal Logic; Security; Verification;
Conference_Titel :
Networking and Digital Society (ICNDS), 2010 2nd International Conference on
Conference_Location :
Wenzhou
Print_ISBN :
978-1-4244-5162-3
DOI :
10.1109/ICNDS.2010.5479238
