Heuristic for Directed Model Checking of Security Protocols

Abstract

This paper introduces a heuristic to mitigate the state space explosion problem inherent in model checking of security protocols. The heuristic is property-dependent as it derives the hints from the security property to be verified. The heuristic has been implemented in a tool and the preliminary results show the effectiveness of the heuristic. The heuristic extends our previous work in which we suggested that directed model checking can be effectively used for security protocol verification.