Witness-Functions versus Interpretation-Functions for Secrecy in Cryptographic Protocols: What to Choose?
This work addresses the challenge of verifying secrecy in cryptographic protocols for security researchers, but it appears incremental as it compares existing function families rather than introducing a new paradigm.
The paper tackles the problem of proving secrecy in cryptographic protocols by comparing two families of functions—interpretation-functions and witness-functions—and shows that witness-functions are more efficient, successfully proving correctness for secrecy in an ad-hoc protocol where interpretation-functions fail.
Proving that a cryptographic protocol is correct for secrecy is a hard task. One of the strongest strategies to reach this goal is to show that it is increasing, which means that the security level of every single atomic message exchanged in the protocol, safely evaluated, never deceases. Recently, two families of functions have been proposed to measure the security level of atomic messages. The first one is the family of interpretation-functions. The second is the family of witness-functions. In this paper, we show that the witness-functions are more efficient than interpretation-functions. We give a detailed analysis of an ad-hoc protocol on which the witness-functions succeed in proving its correctness for secrecy while the interpretation-functions fail to do so.