Towards Automated Verification of Rational Cryptographic Protocols
Michael Backes, Oana Ciobotaru, and Matteo Maffei
Rational cryptography is a new field which combines models and methods from both cryptography and game theory. More precisely, while in the traditional cryptographic setting one considers protocol participants to be either honest or arbitrarily malicious, in rational cryptography the participants are self-interested (also called rational) and only perform attacks which they can benefit from. Rational cryptography relies on game-theoretic notions, such as equilibria, in order to ensure protocol security when the attacker is rational. In this work, we give a general technique for modeling rational cryptographic protocols and their associated security properties in the applied pi calculus. These properties come from game theory equilibrium concepts, which we also redefine within the applied pi calculus setting. We further illustrate our approach by modeling a simplified version of the RatFish rational file sharing protocol [Backes-Ciobotaru-Krohmer-ESORICS-2010] within the new framework and by providing its corresponding automatic proof of Nash equilibrium using ProVerif. To the best of our knowledge, this is the first time such an approach has been taken for general modeling of rationality and utilities and also for automated verification of rational cryptographic protocols and their associated game-theoretic properties.