DocumentCode
561264
Title
Formal modeling and verification of DLK protocol
Author
Al-Hamadi, H.M.N. ; Yeun, C.Y. ; Zemerly, M.J. ; Al-Qutayri, M.A. ; Gawanmeh, A.
Author_Institution
Coll. of Eng., Khalifa Univ., Sharjah, United Arab Emirates
fYear
2011
fDate
11-14 Dec. 2011
Firstpage
578
Lastpage
583
Abstract
This paper presents a formal model for the analysis and verification of a multi-agent system based on the Distributed Lightweight Kerberos (DLK) protocol. Verifying the security protocol exposes security defects and aids in fixing them. The verification process of the DLK protocol uses the ProVerif tool. Based on this tool, the security mechanism of the protocol is clearly exposed. The results of using ProVerif indicate that DLK is secure as initially claimed.
Keywords
distributed processing; formal verification; multi-agent systems; protocols; security of data; DLK protocol; ProVerif tool; distributed lightweight Kerberos protocol; formal modeling; formal verification; multiagent system; security defects; security protocol; Authentication; Encryption; Protocols; Servers; Syntactics; Agent technology; DLK protocol; Formal Method; ProVerif;
fLanguage
English
Publisher
ieee
Conference_Titel
Internet Technology and Secured Transactions (ICITST), 2011 International Conference for
Conference_Location
Abu Dhabi
Print_ISBN
978-1-4577-0884-8
Type
conf
Filename
6148402
Link To Document