Loading...
Thumbnail Image
Publication

A novel security protocol attack detection logic with unique fault discovery capability for freshness attacks and interleaving session attacks

Date
2017
Abstract
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.
Supervisor
Description
peer-reviewed
Publisher
IEEE Computer Society
Citation
IEEE Transactions on Dependable and Secure Computing; 16 (6), pp. 969-983
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
Type
Article
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/
License