Probabilistic Applied Pi Calculus and Zero Knowledge

As zero-knowledge proof plays a more and more important role in modern cryptography, the need for formal analysis becomes more urgent. In this paper, we make use of formal methods to establish a zero-knowledge result. The formal model is probabilistic applied pi and the zero-knowledge proof is Hamiltonian cycle. By this example, our preliminary work shows how zero-knowledge can be modeled in formal models such as process calculi and how to establish a zero-knowledge proof by checking equivalence in the model.