Formal development of secure Email

Dan Zhou, Joncheng C. Kuo, Susan Older, Shiu Kai Chin

Research output: Chapter in Book/Entry/PoemConference contribution

5 Scopus citations


Developing systems that are assured to be secure requires precise and accurate descriptions of specifications, designs, implementations, and security properties. Formal specification and verification have long been recognized as giving the highest degree of assurance. In this paper, we describe a software development process that integrates formal verification and synthesis. We demonstrate this process by developing assured sender and receiver C++ code for a secure electronic mail system, Privacy Enhanced Mail. We use higher-order logic for system-requirements specification, design specifications and design verification. We use a combination of higher-order logic and category theory and tools supporting these formalisms to refine specifications and synthesize code. Much of our work is applicable to other secure email protocols, as our development is parameterized, component-based, and reusable.

Original languageEnglish (US)
Title of host publicationProceedings of the Hawaii International Conference on System Sciences
PublisherIEEE Computer Society
Number of pages1
StatePublished - 1999
EventProceedings of the 1999 32nd Annual Hawaii International Conference on System Sciences, HICSS-32 - Maui, HI, USA
Duration: Jan 5 1999Jan 8 1999


OtherProceedings of the 1999 32nd Annual Hawaii International Conference on System Sciences, HICSS-32
CityMaui, HI, USA

ASJC Scopus subject areas

  • Software
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Formal development of secure Email'. Together they form a unique fingerprint.

Cite this