A Semi-Decidable Procedure for Secrecy in Cryptographic Protocols
This work addresses the challenge of ensuring security in cryptographic protocols for researchers and practitioners, though it appears incremental as it builds on existing verification methods with new functions.
The paper tackles the problem of verifying secrecy in cryptographic protocols by introducing a semi-decidable procedure based on Witness-Functions, which guarantee secrecy if a protocol is proven increasing, and demonstrates its application by analyzing variations of the Needham-Schroeder and NSL protocols, proving the latter correct for secrecy.
In this paper, we present a new semi-decidable procedure to analyze cryptographic protocols for secrecy based on a new class of functions that we call: the Witness-Functions. A Witness-Function is a reliable function that guarantees the secrecy in any protocol proved increasing once analyzed by it. Hence, the problem of correctness becomes a problem of protocol growth. A Witness-Function operates on derivative messages in a role-based specification and introduces new derivation techniques. We give here the technical aspects of the Witness-Functions and we show how to use them in a semi-decidable procedure. Then, we analyze a variation of the Needham-Schroeder protocol and we show that a Witness-Function can also help to teach about flaws. Finally, we analyze the NSL protocol and we prove that it is correct with respect to secrecy.