A Simpler Framework Based on the Applied Pi Calculus and Its Application to Electronic Cash Protocol

We present a framework for describing and analyzing security protocols. It simplifies the applied pi calculus of Abadi and Fournet by moving away the infinite processes and the capability of transmitting channels in order to make the framework fit for describing practical protocols. An alternative operational semantics is given to make the framework more efficient when analyzing protocols. The semantics turns out to be well defined, since in this semantics labeled bisimilarity coincides with observational equivalence. We benefit from this result in analyzing the anonymity of an electronic cash protocol by the bisimulation method.