Modeling Multiple Modes of Operation with Alloy

Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted or mass reproduced without the explicit permission of the copyright holder.

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.