Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini: Automated Proofs of Block Cipher Modes of Operation. J. Autom. Reason. 56(1): 49-94 (2016)