Title :
AKA Protocol and Its Formal Analysis and Verification Using Ambient Calculus and Logics
Author :
Zhang, Xiaopei ; Li, Xiang ; Luo, Wenjun
Author_Institution :
Inst. of Comput. Sci., Guizhou Univ., Guiyang, China
Abstract :
In this paper, ambient calculus and ambient logics are introduced. Then we describe 3GPP authentication and key agreement protocol (AKA). This protocolpsilas goals are formally analyzed using ambient calculus. And we verified this protocolpsilas goals using ambient logics. It shows that AKA protocol can achieve successfully the goals of authentication and key agreement.
Keywords :
3G mobile communication; calculus; cryptographic protocols; formal verification; mobile computing; 3GPP authentication; AKA protocol; ambient calculus; ambient logics; formal analysis; formal verification; key agreement protocol; Authentication; Calculus; Computer science; Cryptography; Distributed computing; Helium; Logic; Mobile computing; Protocols; Tin; ambient calculus; authentication; formal analysis; key agreement; verification;
Conference_Titel :
Networking and Digital Society, 2009. ICNDS '09. International Conference on
Conference_Location :
Guiyang, Guizhou
Print_ISBN :
978-0-7695-3635-4
DOI :
10.1109/ICNDS.2009.54
