1990

Gray, James W. "Information Sharing in Secure Systems," Proc. IEEE Computer Security Foundations Workshop III, IEEE Press, 1990.

Gray, James W. "Probabilistic Interference," Proc. 1990 IEEE Symposium on Security and Privacy, IEEE Press, 1990.

McLean, John D. "The Specification and Modeling of Computer Security," Computer, Vol. 23, No. 1, Jan. 1990. PostScript, PDF

McLean, John D. "Security Models and Information Flow," Proceedings of 1990 IEEE Symposium on Research in Security and Privacy, IEEE Press, 1990. (IEEE Computer Society Outstanding Paper Award) PostScript, PDF

Moore, Andrew P. "The Specification and Verified Decomposition of System Requirements Using CSP," IEEE Transactions on Software, Vol. 16, No. 9, September, 1990. PostScript, PDF

An important principle of building trustworthy systems is to rigorously analyze the critical requirements early in the development process, even before starting system design. Existing proof methods for systems of communicating processes focus on the bottom-up composition of component-level specifications into system-level specifications. Trustworthy system development requires, instead, the top-down derivation of component requirements from the critical system requirements. This paper describes a formal method for decomposing the requirements of a system into requirements of its component processes and a minimal, possibly empty, set of synchronization requirements. The Trace Model of Hoare's Communicating Sequential Processes (CSP) is the basis for the formal method. We apply the method to an abstract voice transmitter and describe the role that the EHDM verification system plays in the transmitter's decomposition. In combination with other verification techniques, we expect that the method defined here will promote the development of more trustworthy systems.

Moskowitz, Ira S. "Quotient States and Probabilistic Channels," Proc. IEEE Computer Security Foundations Workshop III, IEEE Press, 1990.

Syverson Paul F. "A Logic for the Analysis of Cryptographic Protocols," NRL Formal Report 9305, December 1990.

A corrected version of the logic and semantics from "Formal Semantics for Logics of Cryptographic Protocols" is presented. Also presented are soundness and completeness proofs for the logic.

A first order, epistemic logic for representing and analyzing cryptographic protocols is presented along with an associated model-theoretic semantics. The formal language presented has distinct means to represent knowledge of an individual word, e.g., the ability to recognize or produce a decryption key, and propositional knowledge. A sample analysis of a protocol is given.

Back to the CHACS Publications Page.

Back to the Publications Page.