Modeling partial attacks with ALLOY

The automated and formal analysis of cryptographic primitives, security protocols and Application Programming Interfaces (APIs) up to date has been focused on discovering attacks that completely break the security of a system. However, there are attacks that do not immediately break a system but weaken the security sufficiently for the adversary. We term these attacks partial attacks and present the first methodology for the modeling and automated analysis of this genre of attacks by describing two approaches. The first approach reasons about entropy and was used to simulate and verify an attack on the ECB|ECB|OFB triple-mode DES block-cipher. The second approach reasons about possibility sets and was used to simulate and verify an attack on the personal identification number (PIN) derivation algorithm used in the IBM 4758 Common Cryptographic Architecture.