Formal development of secure Email

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Abstract

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
Pages132
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

Other

OtherProceedings of the 1999 32nd Annual Hawaii International Conference on System Sciences, HICSS-32
CityMaui, HI, USA
Period1/5/991/8/99

ASJC Scopus subject areas

  • Software
  • Industrial and Manufacturing Engineering

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

  • Cite this

    Zhou, D., Kuo, J. C., Older, S. B., & Chin, S. K. (1999). Formal development of secure Email. In Proceedings of the Hawaii International Conference on System Sciences (pp. 132). IEEE Computer Society.