Deducing Security Goals From Shape Analysis Sentences

2012/04/02 by John D. Ramsdell, Ramsdell, John D. · 4 citations
Computer Science · #Advanced Authentication Protocols Security #Cryptographic Implementations and Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #User Authentication and Security Systems #cs.CR #cs.LO

paper · pdf · doi:10.48550/arxiv.1204.0480

19 pages

openalex publication_date 2012/04/02 · arxiv created 2018/02/05 · arxiv updated 2018/02/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Guttman presented a model-theoretic approach to establishing security goals in the context of Strand Space theory. In his approach, a run of the Cryptographic Protocol Shapes Analyzer (CPSA) produces models that determine if a goal is satisfied. This paper presents a method for extracting a sentence that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a goal is satisfied. This method has been implemented and is available to all.

Cited by

• Homomorphisms and Minimality for Enrich-by-Need Security Analysis
• Proving Security Goals With Shape Analysis Sentences
• Enrich-by-need Protocol Analysis for Diffie-Hellman (Extended Version)
• A Hybrid Analysis for Security Protocols with State

Related

• Proving Security Goals With Shape Analysis Sentences
• ModelForge: Using GenAI to Improve the Development of Security Protocols
• Adding branching to the strand space model
• State Space Reduction with Message Inspection in Security Protocol Model Checking
• FSL – Fibred Security Language