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. 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.

翻译：工业与安全关键系统中通信协议的安全验证面临挑战，因为其实现通常具有专有性、仅能以黑盒形式访问，且过于复杂而难以手动建模。因此，现有安全测试方法通常依赖于不完整的测试套件和/或需要大量人工建模，限制了覆盖范围、可扩展性与可信度。本文致力于解决在无法访问内部系统模型的情况下系统化验证协议安全属性的问题。我们提出一种灵活且可扩展的通信协议形式化验证方法，该方法将主动自动机学习与模型检验相结合，从而实现对黑盒协议实现的严格安全分析。主要贡献包括：（i）一种为学习得到的协议模型增强安全相关命题的方法；（ii）从学习模型到模型检验制品的全自动化转换流程；（iii）可复用、通用的安全属性模板，可在特定协议模型中实例化；（iv）通过案例研究进行实证验证，展示了该方法在不同协议与领域中的适用性。结果表明，与传统验证流程相比，本方法能够以可扩展且系统化的方式发现黑盒系统中的安全漏洞，同时减少建模工作量并提升自动化程度。