From automata learning to model checking: Formal security verification of black-box protocols

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. The key contributions include: (i) a method for augmenting learned protocol models with security-relevant propositions, (ii) a fully automated transformation pipeline from learned models to model-checking artifacts, (iii) reusable, generic security property templates that are instantiated in protocol-specific models, and (iv) empirical validation through case studies demonstrating applicability in different protocols and domains. The results show that the approach enables scalable and systematic discovery of security vulnerabilities in black-box systems while reducing modeling effort and improving automation compared with traditional verification workflows.