Proving Security Goals With Shape Analysis Sentences

2014/03/14 by John D. Ramsdell, Ramsdell, John D. · 1 citation
Computer Science · #Advanced Authentication Protocols Security #Cryptography and Security (cs.CR) #Digital Rights Management and Security #FOS: Computer and information sciences #User Authentication and Security Systems #cs.CR

paper · pdf · doi:10.48550/arxiv.1403.3563

MITRE Technical Report. arXiv admin note: substantial text overlap with arXiv:1204.0480

arxiv created 2014/03/14 · openalex publication_date 2014/03/14 · arxiv updated 2014/03/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Deducing Security Goals From Shape Analysis Sentences

Cited by

• A Hybrid Analysis for Security Protocols with State

Related

• Deducing Security Goals From Shape Analysis Sentences
• Shape and Content: Incorporating Domain Knowledge into Shape Analysis
• FSL – Fibred Security Language
• Relations, Constraints and Abstractions: Using the Tools of Logic Programming in the Security Industry
• ModelForge: Using GenAI to Improve the Development of Security Protocols