We propose and explore a framework for the symbolic static analysis of side-channel attacks. Our approach is built on top of a probabilistic model for studying off-line guessing attacks to security protocols, which already took into account algebraic and probabilistic mathematical properties of cryptography. In our extension, we further consider side-channel information concerning observable physical properties of the implementations of cryptographic primitives. Overall, the framework encompasses a probabilistic symbolic attacker, more powerful than conventional Dolev-Yao attackers, and able to capture and quantify attacks that also explore side-channel weaknesses.
We illustrate the power of our framework with several meaningful examples, semi-automated by our (in development) prototype analyzer.