Authors
Jaouhar Fattahi1 and Mohamed Mejri1 and Hanane Houmani2, 1Laval University, Canada and
2University Hassan II, Morocco
Abstract
In this paper, we present new functions for secrecy in cryptographic protocols:the witness-functions. A witness-function is a protocol-dependent function that is able to prove the correctness of a protocol through its growth. It bases its calculation on the static part of a message only in a role-based specification by using derivation techniques. We show here how to build them. Then, we run an analysis on two real protocols. First, we run an analysis on NSL protocol and we prove that it is correct with respect to the property of secrecy. Then, we run an analysis on a variation of Needham-Schroeder protocol in which we show that a witness-function could even help to discover flaws.
Keywords
Cryptographic Protocols, Role-based specification, Secrecy