A Calculus for Cryptographic Communication Protocols——The CCP Calculus

摘要：

We introduce the CCP calculus, a revision of valuepassing 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.

作者: Luming Fang Hangjun Wang

作者单位: School of Information Science and Technology Zhejiang Forestry University, Linan 311300, China

会议类型: 国际会议

会议名称: 2006 International Conference on Communications,Circuits and Systems(第四届国际通信、电路与系统学术会议)

会议地点: 广西桂林

会议语种:英文

页码: 1651-1654

在线出版日期: 2006-06-25（万方平台首次上网日期，不代表论文的发表时间）