Combining model learning and formal analysis: A framework for protocol implementation verification

doi:10.1016/j.jisa.2025.104079

Combining model learning and formal analysis: A framework for protocol implementation verification

2025-06-02

0

PRE

AI

DOI：10.1016/j.jisa.2025.104079

Original

Original request for help

Save

Abstract

En 中文

Ensuring the security of cryptographic protocols in practice is challenging due to the complexity of state transitions, cryptographic dependencies, and dynamic interactions. Real-world implementations often deviate from formal specifications, introducing subtle vulnerabilities that compromise key security properties such as confidentiality and authentication. To address this challenge, we propose a lightweight verification framework that integrates model learning with the Applied Pi calculus, enabling automated analysis of security protocol implementations. Our approach consists of two key components: (1) an Extended Mealy Machine (EMM) model that captures both control flow and data flow semantics to represent protocol behavior, and (2) a formal verification framework translating execution paths into symbolic models for automated analysis using ProVerif. We validated the framework on multiple TLS implementations, demonstrating its ability to uncover critical vulnerabilities such as authentication bypass and confidentiality violations. The results show that our method achieves a balance between precision and efficiency, providing a scalable and practical solution for real-world systems.

Combining model learning and formal analysis: A framework for protocol implementation verification

Abstract

Journal

Organization