Modeling Multiple Modes of Operation with Alloy
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  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.
KeywordsAlloy Alloy Analyzer Modes of Operation Cryptography
Unable to display preview. Download preview PDF.
- 1.Implementation of Cryptographic Modes In Alloy (Online Material), http://www.icsd.aegean.gr/postgraduates/icsdm10002/
- 2.Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the ”small scope hypothesis”. Tech. Rep., POPL 2002: Proceedings of the 29th ACM Symposium on the Principles of Programming Languages (2002)Google Scholar
- 7.Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)Google Scholar
- 9.National Institute of Standards and Technology: FIPS PUB 81: DES Modes of Operation (1980)Google Scholar
- 10.National Institute of Standards and Technology: FIPS PUB 46-3: Data Encryption Standard (DES) (1999)Google Scholar