出版社：Academy & Industry Research Collaboration Center (AIRCC)
摘要：In this paper, we present new functions for secrecy in cryptographic protocols:the witnessfunctions.A witness-function is a protocol-dependent function that is able to prove thecorrectness of a protocol through its growth. It bases its calculation on the static part of amessage only in a role-based specification by using derivation techniques. We show here how tobuild them. Then, we run an analysis on two real protocols. First, we run an analysis on NSLprotocol and we prove that it is correct with respect to the property of secrecy. Then, we run ananalysis on a variation of Needham-Schroeder protocol in which we show that a witnessfunctioncould even help to discover flaws.
