A Calculus for Cryptographic Communication Protocols-The CCP Calculus

We introduce the CCP calculus, a revision of value-passing process calculus designed for describing and reasoning about cryptographic protocols with full encryption systems. Traditional bisimulations are suitable for defining security properties, but very few can be automatized because of infinite branches. To deal with this problem, we adopt the symbolic techniques and propose a symbolic bisimulation for the calculus. Equipped with a symbolic LTS semantics, the previous uncontrollable input transitions are confined to finite branches. We also prove that our symbolic bisimulation is sound to the traditional ones, and therefore is much promising to automatically check the security properties of cryptographic protocols