A Semi-Decidable Procedure for Secrecy in Cryptographic Protocols
Abstract
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.
Cite
@article{arxiv.1408.2774,
title = {A Semi-Decidable Procedure for Secrecy in Cryptographic Protocols},
author = {Jaouhar Fattahi and Mohamed Mejri and Hanane Houmani},
journal= {arXiv preprint arXiv:1408.2774},
year = {2015}
}
Comments
Presentation enhanced