用形状分析语句证明安全目标
Proving Security Goals With Shape Analysis Sentences
摘要：
介绍形状分析语句的论文提出了一种在一阶逻辑中提取完全表征CPSA运行的语句的方法。然后可以使用逻辑推理来确定是否满足安全目标。本文在详细的串空间理论的基础上，提出了一种将形状分析语句导入证明助手的方法。其结果是一个语义丰富的环境中，安全目标的有效性可以确定使用形状分析句子和它们所基于的基础。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
