用形状分析语句证明安全目标
密码学与安全
2014-03-17 v1
摘要
引入形状分析语句的论文提出了一种方法，用于提取一阶逻辑中的语句，该语句完全刻画了CPSA的一次运行。然后可以利用逻辑演绎来确定安全目标是否满足。本文提出了一种方法，将形状分析语句导入到基于详细串空间理论的证明助手中。结果是一个语义丰富的环境，在该环境中，可以使用形状分析语句及其所基于的基础来确定安全目标的有效性。
引用
@article{arxiv.1403.3563,
title = {Proving Security Goals With Shape Analysis Sentences},
author = {John D. Ramsdell},
journal= {arXiv preprint arXiv:1403.3563},
year = {2014}
}
备注
MITRE Technical Report. arXiv admin note: substantial text overlap with arXiv:1204.0480