Modeling and Reasoning about an Attacker with Cryptanalytical Capabilities

We propose a probabilistic framework for the analysis of security protocols. The proposed framework allows one to model and reason about attackers that extend the usual Dolev-Yao adversary with explicit probabilistic statements representing properties of cryptographic primitives and the attacker's (partial) information about secret messages. The expressive power of these probabilistic statements is illustrated, namely by representing a standard security notion like indistinguishability under chosen plaintext attacks. We present an entropy-based approach to estimate the probability of a successful attack on a protocol given the prescribed knowledge of the attacker. We prove that, for an attacker whose knowledge increases with the security parameter, computing this quantity is NP-hard in the security parameter. However, we are still able to analyze a few meaningful and illustrative examples. Finally, we obtain a result which may be used to prove that a certain amount of probabilistic knowledge (about the properties of the cryptography being used) is not enough for allowing an attacker to correctly uncover a secret with non-negligible probability.