Two-Level Liveness of Cryptographic Protocols

W. Jiao (Canada)


Cryptographic Protocol, Liveness, SPi-Calculus


Safety and liveness are two important aspects of properties of cryptographic protocols, but few deep studies have been developed on the aspect of liveness of cryptographic protocols at the current stage. In this paper, we studied the liveness properties of cryptographic protocols and defined two-level liveness for protocols, principal-level liveness and protocol-level liveness. We proved that an authentication protocol is correct if and only if it is alive at both the principal level and the protocol level. By analyzing the two-level liveness, we can easily judge whether an authentication protocol is correct or not.

Important Links:

Go Back