ESSM: Formal Analysis Framework for Protocol to Support Algebraic Operations and More Attack Capabilities. (7th December 2021)

• Record Type: Journal Article
• Authors: Miao, Xuyang; Gu, Chunxiang; Lu, Siqi; Shi, Yanan
• Other Names: Zhu Youwen Academic Editor.
• Is Part Of: Security and communication networks. Volume 2021(2021)
• Publication Date: 2021-12-07
• Subjects: Computer networks -- Security measures -- Periodicals; Computer security -- Periodicals; Cryptography -- Periodicals; 005.805
• DOI: 10.1155/2021/8273172
• Languages: English
• ISSNs: 1939-0114

Abstract

Abstract : The strand space model has been proposed as a formal method for verifying the security goals of cryptographic protocols. However, only encryption and decryption operations and hash functions are currently supported for the semantics of cryptographic primitives. Therefore, we establish the extended strand space model (ESSM) framework to describe algebraic operations and advanced threat models. Based on the ESSM, we add algebraic semantics, including the Abelian group and the XOR operation, and a threat model based on algebraic attacks, key-compromise impersonation attacks, and guess attacks. We implement our model using the automatic analysis tool, Scyther. We demonstrate the effectiveness of our framework by analysing several protocols, in particular a three-factor agreement protocol, with which we can identify new attacks while providing trace proofs.