@inproceedings{05a15434f93d4d8abdcf88e96c235441,
title = "Formal analysis of a secure communication channel: Secure core-email protocol",
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.",
author = "Dan Zhou and Chin, {Shiu Kai}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999 ; Conference date: 20-09-1999 Through 24-09-1999",
year = "1999",
doi = "10.1007/3-540-48119-2_42",
language = "English (US)",
isbn = "3540665870",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "758--775",
editor = "{ Wing}, {Jeannette M.} and Jim Woodcock and Jim Davies",
booktitle = "FM 1999 – Formal Methods - World Congress on Formal Methods in the Development of Computing Systems, Proceedings",
}