Conference

Authors: Kalyvas C., Konstantinou E., Kambourakis G.
Title: Modeling Multiple Modes of Operation with Alloy
Conference: International Conference on Security Technology (SecTech 2012)
Editors: T.H. Kim et al.
Ed: No
Eds: Yes
Pages: 78-85
To appear: No
Month: November
Year: 2012
Place: Jeju, Korea
Pubisher: CCIS 339, Springer
Link: http://link.springer.com/chapter/10.1007%2F978-3-642-35264-5_11
File name:
Abstract: Speci fication (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 veri fication 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 [9] 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.