Heuristic Methods for Security Protocols

TL;DR

This paper introduces a heuristic approach that improves the efficiency of model checking cryptographic security protocols by prioritizing state exploration based on security properties, addressing the state-space explosion problem.

Contribution

It proposes a security property-dependent heuristic that weights states using security formulae to enhance attack search in model checking of cryptographic protocols.

Findings

Heuristic reduces state-space exploration time.

Improves detection of security violations.

Addresses state-space explosion in protocol verification.

Abstract

Model checking is an automatic verification technique to verify hardware and software systems. However it suffers from state-space explosion problem. In this paper we address this problem in the context of cryptographic protocols by proposing a security property-dependent heuristic. The heuristic weights the state space by exploiting the security formulae; the weights may then be used to explore the state space when searching for attacks.