Fair certified E-mail Protocols with delivery deadline agreement

A certified e-mail system guarantees that a mail originator gets a receipt if and only if a recipient receives mail content. Unlike the previous schemes, the optimistic protocols that were recently proposed have some drawbacks: mail receiving can be delayed indefinitely or the originator can place the blame on the. recipient for not having received the mail. In this paper, we point out some shortcomings in the optimistic protocols and improve them by introducing deadline agreement of mail delivery. We modelled the original protocols and the improved schemes by using ATS (Alternating Transition System) and verified them by using MOCHA, a model checker. MOCHA showed that the improved protocols do not have the shortcomings of the original schemes.