Extending A Certified Email Protocol With Key Chains And Its Formal Verification

With the development of electronic business, certified email (CEM) protocol is getting more and more attention. CEM protocol is kind of fair-exchange protocol, which allows two mutually mistrusting parties to exchange an electronic message with the help of evidences. It is supposed to guarantee fairness with respect to non-repudiable evidence, i.e., it is undesirable that at the end of the protocol, only one of the two parties gets all that he expects.Our starting point is an optimistic certified email protocol, which is proposed by Cederquist et al. The crucial point of the protocol is that it employs key chains to reduce the storage requirement of the trusted third party. We extend their protocol to satisfy one more property of TTP (trusted third party) transparency, using an existing verifiably encrypted signature scheme based on bilinear pairings. We are able to show, by a detailed comparison, that our extended protocol is one of the most efficient certified email protocols satisfying strong fairness, timeliness, effectiveness and TTP transparency.After that, we analyze the extended protocol using the technique of automatic formal verification. Formal verification is a technique to check automatically whether a give specification of system satisfies the specification of properties. The finite-state model checker Mocha is adopted to verify the properties of fairness, timeliness and effectiveness which can be naturally interpreted in alternating-time temporal logic (ATL) formulas with game semantics. The model for the extended CEM protocol is built using the guarded command language with concurrent game structures. The verification of properties expressed in ATL formulas corresponds to the computation of winning strategies.Besides, as to how to analyze the property of TTP transparency, another toolsetμCRL is used, since we have to compare traces of getting evidences from different situations. TheμCRL toolset has the ability of generating state spaces which can be visualized and manipulated by the toolbox CADP (Construction and Analysis of Distributed Processes) that acts as a back-end ofμCRL.Our results show that the extended certified email protocol is an efficient protocol that satisfies fairness, effectiveness, timeliness and TTP transparency at the same time.