Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Formal Development Of Secure Email, Dan Zhou, Joncheng C. Kuo, Susan Older, Shiu-Kai Chin
Formal Development Of Secure Email, Dan Zhou, Joncheng C. Kuo, Susan Older, Shiu-Kai Chin
Electrical Engineering and Computer Science - All Scholarship
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 …
Formal Analysis Of A Secure Communication Channel: Secure Core-Email Protocol, Dan Zhou, Shiu-Kai Chin
Formal Analysis Of A Secure Communication Channel: Secure Core-Email Protocol, Dan Zhou, Shiu-Kai Chin
Electrical Engineering and Computer Science - All Scholarship
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 …