Formal analysis of a secure communication channel: Secure core-email protocol

Dan Zhou, Shiu Kai Chin

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

3 Scopus citations

Abstract

To construct a highly-assured implementation of secure communication channels we must have clear definitions of the security services, the channels, and under what assumptions these channels provide the desired services. We formally define secure channel services and develop a detailed example. The example is a core protocol common to a family of secure email systems. We identify the necessary properties of cryptographic algorithms to ensure that the email protocol is secure, and we verify that the email protocol provides secure services under these assumptions. We carry out the definitions and verifications in higher order logic using the HOL theorem-prover. All our definitions and theorems are conservative extensions to the logic of HOL.

Original languageEnglish (US)
Title of host publicationFM 1999 – Formal Methods - World Congress on Formal Methods in the Development of Computing Systems, Proceedings
EditorsJeannette M. Wing, Jim Woodcock, Jim Davies
PublisherSpringer Verlag
Pages758-775
Number of pages18
ISBN (Print)3540665870, 9783540665878
DOIs
StatePublished - 1999
Event1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999 - Toulouse, France
Duration: Sep 20 1999Sep 24 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1708
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999
CountryFrance
CityToulouse
Period9/20/999/24/99

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formal analysis of a secure communication channel: Secure core-email protocol'. Together they form a unique fingerprint.

  • Cite this

    Zhou, D., & Chin, S. K. (1999). Formal analysis of a secure communication channel: Secure core-email protocol. In J. M. Wing, J. Woodcock, & J. Davies (Eds.), FM 1999 – Formal Methods - World Congress on Formal Methods in the Development of Computing Systems, Proceedings (pp. 758-775). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1708). Springer Verlag. https://doi.org/10.1007/3-540-48119-2_42