Formal analysis of non-repudiation protocol by spi

Abstract

spi calculus, which was based on the theorems of process algebra, was fit for the proof of concurrent protocol execution. Message origination test was put up and the semantics of message sign operation was successfully expressed base on the test, at last, the non-repudiation protocol ZG was proved so as to prove the validity of the method.

Keywords

• spi calculus;non-repudiation;fairness;message origination test