A Novel Security Protocol Attack Detection Logic with Unique Fault Discovery Capability for Freshness Attacks and Interleaving Session Attacks

This paper introduces a new logic-based technique for detecting security protocol weaknesses that are exploitable by freshness and interleaving session attacks. This technique is realised as a special purpose logic to be used throughout the protocol design stage, where a draft of the protocol is subjected to formal analysis prior to its publication or deployment. For any detected failures the analysis also reveals their cause, facilitating design corrections. The proposed Attack Detection Logic is introduced and its details, including the language, predicates, axioms, rules, semantics as well as soundness and completeness are presented. The effectiveness of the logic is evaluated in a case study, where it is demonstrated how to use the Attack Detection Logic as part of the design process of security protocols. Further, the logic is applied to a range of security protocols, including protocols with known weaknesses and protocols that are known to be secure. The logic's ability to detect various attacks is established by demonstrating that for protocols with known weaknesses, at least one detection rule is activated and no detection rule is activated for protocols without weaknesses. This case study confirms the logic's ability to detect design weaknesses exploitable by freshness and interleaving session attacks.