Modeling multiple modes of operation with alloy

Abstract

Specification (or modeling) languages can be very handy in describing certain aspects of a system and check properties of interest about it. Also, once a model is constructed, one is able to use the associated analyzer to create examples and/or counterexamples to explore hypotheses posed about the system. In the context of cryptography this verification process is of great importance as it can contribute towards finding weaknesses and assessing system's robustness. This paper capitalizes on the well-known Alloy language to model and analyze attacks on DES triple modes namely ECB|ECB|CBC-1 and ECB|OFB|OFB. We model attacks described in [5] and show that they can be fruitful in the general case. This work can serve as a framework in modeling similar cryptosystems and assessing certain attacks on them. © 2012 Springer-Verlag.