Front.Comput.Sci. DOI RESEARCH ARTICLE Design and Formal Verification of a CEM Protocol with Transparent TTP

Abstract In certified email (CEM) protocols, TTP trans-parency is an important security requirement which helps to avoid bad publicity as well as protecting individual users ’ pri-vacy. Cederquist et al. proposed an optimistic certified email protocol, which employs key chains to reduce the storage re-quirement of the trusted third party (TTP). We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An imple-mentation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satis-fying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended pro-tocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP trans-parency is formalised and analysed using the toolsets µCRL and CADP