Title :
Extension and application of protocol composition logic
Author :
You, Ziyi ; Li, Juntao ; Xie, Xiaoyao
Author_Institution :
Sch. of Comput. Sci. & Technol., Guizhou Univ., Guiyang, China
Abstract :
Protocol Composition Logic (PCL) is a logic for proving security properties of network protocols that use public and symmetric key cryptography. Because the PCL composition theorems support compositional reasoning about security protocols, including parallel composition of different protocols, and sequential composition of protocol steps, it is particularly useful in carrying out larger-scale security protocol studies. In this paper, PCL is extened by strand space model(SSM) and temporal logic (TL) to better describe and verify complex protocols. Based on improved PCL, the TLS protocol is verified as an example and proved to satisfy authentication property.
Keywords :
cryptographic protocols; message authentication; public key cryptography; temporal logic; authentication property; compositional reasoning; network protocols; parallel composition; protocol composition logic composition theorems; public key cryptography; security property proving; sequential composition; strand space model; symmetric key cryptography; temporal logic; Application software; Authentication; Body sensor networks; Computer science; Cryptographic protocols; Cryptography; Information security; Laboratories; Logic; Protocol Composition Logic; TLS protocol; extension; strand space; temporal logic;
Conference_Titel :
Computer Engineering and Technology (ICCET), 2010 2nd International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4244-6347-3
DOI :
10.1109/ICCET.2010.5485720
