Proving Security Goals With Shape Analysis Sentences
Cryptography and Security
2014-03-17 v1
Abstract
The paper that introduced shape analysis sentences presented a method for extracting a sentence in first-order logic that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a security goal is satisfied. This paper presents a method for importing shape analysis sentences into a proof assistant on top of a detailed theory of strand spaces. The result is a semantically rich environment in which the validity of a security goal can be determined using shape analysis sentences and the foundation on which they are based.
Keywords
Cite
@article{arxiv.1403.3563,
title = {Proving Security Goals With Shape Analysis Sentences},
author = {John D. Ramsdell},
journal= {arXiv preprint arXiv:1403.3563},
year = {2014}
}
Comments
MITRE Technical Report. arXiv admin note: substantial text overlap with arXiv:1204.0480