On the Security of Cryptographic Protocols Using the Little Theorem of Witness Functions
This work addresses security issues in cryptographic protocols for practitioners and researchers, but it appears incremental as it applies an existing theorem to a known protocol.
The paper tackles the problem of detecting security flaws in cryptographic protocols by applying the little theorem of witness functions, specifically analyzing the Needham-Schroeder symmetric-key protocol to identify a vulnerability that could lead to replay attacks.
In this paper, we show how practical the little theorem of witness functions is in detecting security flaws in some category of cryptographic protocols. We convey a formal analysis of the Needham-Schroeder symmetric-key protocol in the theory of witness functions. We show how it helps to teach about a security vulnerability in a given step of this protocol where the value of security of a particular sensitive ticket in a sent message unexpectedly plummets compared with its value when received. This vulnerability may be exploited by an intruder to mount a replay attack as described by Denning and Sacco.