StEVe: A Rational Verification Tool for Stackelberg Security Games
摘要
We present StEVe, a prototype tool modelling Stackelberg Security Games (SSGs) and employing rational verification based on bespoke Stackelberg equilibrium computation. StEVe automatically extracts technical details from public vulnerability databases, transforming these into Attack Defence Trees and then into SSG models. By using the temporal logic rPATL, the tool enables the synthesis of optimal defence strategies through Stackelberg equilibrium analysis, which is implemented as a PRISM-games extension. Preliminary results demonstrate StEVe’s ability to model and counteract cyber threats, reducing potential damages and financial losses.