Formal Verification of a Keystore. - Jaap Boender; Goran Badevic (TASE, 2022)