Tracking Security Flaws in Cryptographic Protocols Using Witness-Functions

In this paper, we use witness-function to capture attack scenarios in cryptographic protocols. A witness-function is a protocol-dependent metric that attributes a reliable security level to every atomic message. We use these functions to prove the protocol correctness with respect to secrecy by proving that the security level of every atomic message never decreases throughout all consecutive receiving and sending steps of the protocol. In this paper, we analyze the defective variant of the Otway-Rees protocol and we demonstrate that the use of witness-functions can be a key element in tracing a well-known type flaw that this protocol involves.