WSEmail: Secure internet messaging based on Web services

Web services offer an opportunity to redesign a variety of older systems to exploit the advantages of a flexible, extensible, secure set of standards. In this paper we explore the objective of improving Internet messaging (email) by redesigning it as a family of web services, an approach we call WSEmail. We illustrate an architecture and describe some applications. Since increased flexibility often mitigates against security and performance, we focus on steps for proving security properties and measuring the performance of our system with its security operations. In particular, we demonstrate an automated proof using TulaFale and Pro Verif of a correspondence theorem for an application called on-demand attachments. We also provide performance measures for the basic WSEmail functions in a prototype we have implemented using .NET. Our experiments show a latency of about a quarter of a second per transaction under load.