Modeling Multiple Modes of Operation with Alloy

  • Christos Kalyvas
  • Elisavet Konstantinou
  • Georgios Kambourakis
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 339)


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.


Alloy Alloy Analyzer Modes of Operation Cryptography 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Implementation of Cryptographic Modes In Alloy (Online Material),
  2. 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
  3. 3.
    Biham, E.: Cryptanalysis of multiple modes of operation. Journal of Cryptology 11, 45–58 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Biham, E.: Cryptanalysis of triple modes of operation. Journal of Cryptology 12, 161–184 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Hong, D., Sung, J., Hong, S., Lee, W., Lee, S., Lim, J., Yi, O.: Known-IV Attacks on Triple Modes of Operation of Block Ciphers. In: Boyd, C. (ed.) ASIACRYPT 2001. LNCS, vol. 2248, pp. 208–221. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRefGoogle Scholar
  7. 7.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)Google Scholar
  8. 8.
    Lin, A., Bond, M., Clulow, J.: Modeling Partial Attacks with Alloy. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2007. LNCS, vol. 5964, pp. 20–33. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    National Institute of Standards and Technology: FIPS PUB 81: DES Modes of Operation (1980)Google Scholar
  10. 10.
    National Institute of Standards and Technology: FIPS PUB 46-3: Data Encryption Standard (DES) (1999)Google Scholar
  11. 11.
    Wagner, D.: Cryptanalysis of Some Recently-Proposed Multiple Modes of Operation. In: Vaudenay, S. (ed.) FSE 1998. LNCS, vol. 1372, pp. 254–269. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Christos Kalyvas
    • 1
  • Elisavet Konstantinou
    • 1
  • Georgios Kambourakis
    • 1
  1. 1.Department of Information and Communication Systems EngineeringUniversity of the AegeanSamosGreece

Personalised recommendations