Static evidences for attack reconstruction

Control Flow Analysis (CFA) has been proven successful for the analysis of cryptographic protocols. Due to its over-approximative nature, the absence of detected flaws implies their absence also at run time, while their presence only says that there is the possibility for flaws to occur. Nevertheless, the static detection of a flaw can be considered as a warning bell that alerts against a possible attack, of which the flaw is the result. Reconstructing the possible attack leading to the detected flaw is not trivial, though. We propose a CFA enriched with causal information that accounts for attacker activity. In case a flaw is predicted, the causal information provides a sort of climbing holds that can be escalated to reconstruct the attack sequence leading to the flaw.