An Open Approach for the Applied Pi Calculus

A notion of open bisimulation is proposed for the Applied Pi Calculus, which extends -calculus in order to facilitate analyzing security protocols. Our notion is based on the labeled transition system, and takes a knowledge aware open approach to model knowledge in security protocols. It is shown to be sound to labeled bisimilarity and is a congruent relation. As a running example, we analyze two e-commerce protocol, namely iKP and Ferguson's electronic cash protocol, by Applied Pi and open bisimilarity.

• Type: Journal
• Year: 2008
• Where: JSW
• Authors: Han Zhu, Yonggen Gu, Xiaohong Wu
• Keywords: Applied Pi, Applied Pi Calculus, JSW 2008, Security Protocols