This paper takes a step toward addressing this gap by introducing a system model, adversary model and end-to-end security property that enable reasoning about the security of authenticated load protocols. We then present a decomposition of the security hyperproperty into two simpler 2-safety properties that enables more scalable verification. Experiments on a protocol model demonstrate viability of the methodology.
Category / Keywords: foundations / formal methods, formal verification, model checking, secureboot, authenticated load, security property specification Original Publication (with minor differences): Formal Methods in Computer-Aided Design (FMCAD) 2019 Date: received 25 May 2019, last revised 19 Aug 2019 Contact author: spramod at cse iitk ac in Available format(s): PDF | BibTeX Citation Note: v2.2.1 of the paper with revisions based on referee comments. Version: 20190820:034417 (All versions of this report) Short URL: ia.cr/2019/564