Secrecy by Witness Functions.
Jaouhar Fattahi, Mohamed Mejri, Hanane Houmani · 2014
Abstract. In this paper, we introduce a new type of functions to analyze crypto-graphic protocols statically for the property of secrecy: the Witness-Functions. A Witness-Function is a reliable protocol-dependent function intended to prove the cor-rectness of a protocol through its growth. It bases its calculation on the static part of a message in a role-based specification and ignores the dynamic one by introducing the notion of derivative messages. It offers two interesting bounds that enable an analysis of protocols on an unbounded number of sessions. We give here the way to build these functions and we state the theorem of protocol analysis with the Witness-Functions.