Deducing Security Goals From Shape Analysis Sentences
This work addresses security verification for cryptographic protocol designers, but it appears incremental as it builds on existing model-theoretic approaches.
The paper tackles the problem of establishing security goals in cryptographic protocols by presenting a method to extract a complete characterization sentence from a run of the Cryptographic Protocol Shapes Analyzer (CPSA), enabling logical deduction to determine goal satisfaction, with the method implemented and made available.
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.