科研之友
微信
新浪微博
Facebook
分享链接
摘要
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.
