DocumentCode
2573677
Title
Analysis of cryptographic protocols using LTL of knowledge
Author
Shigong, Long ; Lijun, Wang
Author_Institution
Dept. of Comput. Sci., Guizhou Univ., Guiyang, China
Volume
1
fYear
2010
fDate
30-31 May 2010
Firstpage
463
Lastpage
466
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Networking and Digital Society (ICNDS), 2010 2nd International Conference on
Conference_Location
Wenzhou
Print_ISBN
978-1-4244-5162-3
Type
conf
DOI
10.1109/ICNDS.2010.5479238
Filename
5479238
Link To Document