Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking

Stefan Marksteiner, Mikael Sjödin, Marjan Sirjani

TL;DR

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

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

Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking

TL;DR

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

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

Paper Structure

This paper contains 11 sections, 2 figures.

Table of Contents

  1. Introduction
  2. Contribution
  3. Approach
  4. Background
  5. Automata and Kripke Structures
  6. Automata Learning
  7. Interface and Abstraction Layer
  8. Linear Temporal Logic and Model Checking
  9. Rebeca
  10. Near Field Communication and Integrated Circuit Access
  11. Electronically Machine-Readable Travel Documents

Figures (2)

  • Figure 1: Overview of the proposed approach; boxes denote artifacts and ellipses denote processes or tools. The items in amber are artifacts and processes defined in this paper, while boxes in blue are artifacts automatically generated by algorithms defined in this paper. Cyan are other items, namely: Mealy machines of SuTs, which are obtained via automata learning and the model checking result which is obtained by running RMC with the respective inputs. RMC is shown as an ellipse in Cyan. Generic security properties and Rebeca templates are one-time work. For each specific problem, only CPMs have to be defined individually.
  • Figure 2: Logical Data Structure of Machine Readable Travel Documents from marksteinerAutomatedPassportControl2024. This shows the applications and files on an eMRTD chip. Amber is the master file (MF), Cyan are dedicated files (DF), Blue are Elementary Files (EF), and Green are key files. Solid frames means mandatory files, dashed ones optional files. Solid boxes donate the LDS contexts, dashed black boxes requirements, and dashed red boxes necessary authentication.