Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran
Abstract
The Cryptographic Protocol Shapes Analyzer (CPSA) determines if a cryptographic protocol achieves authentication and secrecy goals. It can be difficult to ensure that an implementation of a protocol matches up with what CPSA analyzed, and therefore be sure the implementation achieves the security goals determined by CPSA. Roletran is a program distributed with CPSA that translates a role in a protocol into a language independent description of a procedure that is easily translated into an existing computer language. This paper shows how we ensure the procedure produced by Roletran is faithful to strand space semantics and therefore achieves the security goals determined by CPSA. Real implementations of cryptographic functions make use of probabilistic encryption, but CPSA will conclude that two encryptions are the same if they are constructed with the same plaintext and key. The paper concludes by showing how we ensure that executions of generated code that make use of probabilistic encryption achieve the goals determined by CPSA.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 19, 2021
- Accession Number
- AD1156874
Entities
People
- John D. Ramsdell
Organizations
- MITRE Corporation