5Greasoner: A property-directed security and privacy analysis framework for 5G cellular network protocol

Syed Rafiul Hussain, Mitziu Echeverria, Imtiaz Karim, Omar Chowdhury, Elisa Bertino

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    9 Scopus citations

    Abstract

    The paper proposes 5GReasoner, a framework for property-guided formal verification of control-plane protocols spanning across multiple layers of the 5G protocol stack. The underlying analysis carried out by 5GReasoner can be viewed as an instance of the model checking problem with respect to an adversarial environment. Due to an effective use of behavior-specific abstraction in our manually extracted 5G protocol, 5GReasoner's analysis generalizes prior analyses of cellular protocols by reasoning about properties not only regarding packet payload but also multi-layer protocol interactions. We instantiated 5GReasoner with two model checkers and a cryptographic protocol verifier, lazily combining them through the use of abstraction-refinement principle. Our analysis of the extracted 5G protocol model covering 6 key control-layer protocols spanning across two layers of the 5G protocol stack with 5GReasoner has identified 11 design weaknesses resulting in attacks having both security and privacy implications. Our analysis also discovered 5 previous design weaknesses that 5G inherits from 4G, and can be exploited to violate its security and privacy guarantees.

    Original languageEnglish (US)
    Title of host publicationCCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
    PublisherAssociation for Computing Machinery
    Pages669-684
    Number of pages16
    ISBN (Electronic)9781450367479
    DOIs
    StatePublished - Nov 6 2019
    Event26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019 - London, United Kingdom
    Duration: Nov 11 2019Nov 15 2019

    Publication series

    NameProceedings of the ACM Conference on Computer and Communications Security
    ISSN (Print)1543-7221

    Conference

    Conference26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019
    CountryUnited Kingdom
    CityLondon
    Period11/11/1911/15/19

    All Science Journal Classification (ASJC) codes

    • Software
    • Computer Networks and Communications

    Fingerprint Dive into the research topics of '5Greasoner: A property-directed security and privacy analysis framework for 5G cellular network protocol'. Together they form a unique fingerprint.

    Cite this