Refinement and Verification of CBC Casper. - Ryuya Nakamura; Takayuki Jimba; Dominik Harz (IACR Cryptol. ePrint Arch., 2019)