CRJul 2, 2012
An Analysis of the CAVES Attestation Protocol using CPSAJohn D. Ramsdell, Joshua D. Guttman, Jonathan K. Millen et al.
This paper describes the CAVES attestation protocol and presents a tool-supported analysis showing that the runs of the protocol achieve stated goals. The goals are stated formally by annotating the protocol with logical formulas using the rely-guarantee method. The protocol analysis tool used is the Cryptographic Protocol Shape Analyzer.