• DocumentCode
    2233316
  • 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
  • Volume
    1
  • fYear
    2009
  • fDate
    30-31 May 2009
  • Firstpage
    194
  • Lastpage
    197
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Networking and Digital Society, 2009. ICNDS '09. International Conference on
  • Conference_Location
    Guiyang, Guizhou
  • Print_ISBN
    978-0-7695-3635-4
  • Type

    conf

  • DOI
    10.1109/ICNDS.2009.54
  • Filename
    5116244