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.
Cite
@article{arxiv.1207.0418,
title = {An Analysis of the CAVES Attestation Protocol using CPSA},
author = {John D. Ramsdell and Joshua D. Guttman and Jonathan K. Millen and Brian O'Hanlon},
journal= {arXiv preprint arXiv:1207.0418},
year = {2012}
}