Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran

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.

Bounded ACh unification

We consider the problem of the unification modulo an equational theory associativity and commutativity (ACh), which consists of a function symbol h that is homomorphic over an associative–commutative operator +. Since the unification modulo ACh theory is undecidable, we define a variant of the problem called bounded ACh unification. In this bounded version of ACh unification, we essentially bound the number of times h can be applied to a term recursively and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving the bounded version of the problem and prove that the rules are sound, complete, and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.