From Automata Learning to Model Checking: Formal Security Verification of Black-Box Protocols

Abstract

Security verification of communication protocols in industrial and safety-critical systems is challenging because implementations are often proprietary, accessible only as black boxes, and too complex for manual modeling. As a result, existing security testing approaches usually depend on incomplete test suites and/or require labor-intensive modeling, limiting coverage, scalability, and trust. This paper addresses the problem of systematically verifying protocol security properties without access to internal system models. We propose a flexible and scalable method for formal verification of communication protocols that combines active automata learning with model checking to enable rigorous security analysis of black-box protocol implementations. Behavioral models are first inferred from system interactions using automata learning. We then propose context-based proposition maps (CPMs) to enrich the learned models with semantic information, yielding annotated Mealy machines that bridge the gap between learned behavior and property verification. These machines are automatically transformed into verifiable models in the Rebeca modeling language, enabling model checking of generic security properties such as authentication, confidentiality, privilege levels, and key validity, while allowing protocol-specific properties to be manually added. The CPMs are also used to populate these generic properties with protocol-specific propositions. Furthermore, the resulting model can be easily altered to introduce non-deterministic behavior (like timeouts or faults) and examined if the properties still hold under these different conditions. As a result, we gain an automated tool chain that spans from model learning to security property checking of specific protocols.

27 pages, 9 figures, 4 tables, preprint accepted for publication in Elsevier Computers & Security - Original abstract shortened to comply to the arXiv requirements