Center for High Assurance Computing Systems (CHACS) Publications

1991

Gray, James ``On Information Flow Security Models,'' Proc. IEEE Computer Security Foundations Workshop IV, IEEE Press, 1991.

Gray, James ``Toward a Mathematical Foundation for Information Flow Security,'' Proc. 1991 IEEE Symposium on Security and Privacy, IEEE Press, 1991.

McDermott, J., S. Jajodia, and R. Sandhu, "A Single-Level Scheduler for the Replicated Architecture for Multilevel-Secure Databases", Proc. 7th Annual Computer Security Applications Conference, San Antonio, December 1991, pp. 2-11. PostScript

The replicated architecture for multilevel secure database systems provides security by replicating data into separate untrusted single-level database systems. To be successful, a system using the replicated architecture must have a concurrency and replica control algorithm that does not introduce any covert channels. Jajodia and Kogan have developed one such algorithm that uses update projections and a write-all replica control algorithm. The new algorithm uses replicated transactions, and a set of queues organized according to security class. A new definition of correctness is require for this approach, so we present one and use it to show that our algorithm is correct. The existence of this new algorithm increases the viability of the replicated architecture as an alternative to kernelized approaches.
Moskowitz, Ira ``Analysis of a Storage Channel in the Two-Phase Commit Protocol,'' (with O. Costich) Proc. IEEE Computer Security Foundations Workshop IV, IEEE Press, 1991.

Moskowitz, Ira ``Variable Noise Effects upon a Simple Timing Channel,'' Proc. 1991 IEEE Symposium on Research in Security and Privacy, IEEE Press, 1991.

Paul Syverson, ``The Use of Logic in the Analysis of Cryptographic Protocols,'' Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, Oakland CA May 1991 IEEE CS Press (Los Alamitos CA, 1991)

Logics for cryptographic protocol analysis are discussed and a study is made of the protocol features that they are appropirate for analyzing: some are appropriate for analyzing trust, others security. The goals of Burrows, Abadi, and Needham's BAN logic are examined, and it is found that there is confusion about these. Formal semantics is explored as a reasoning tool and the importance of soundness and completeness for protocol security is discussed. The logic KPL is used to resolve a debate over an alleged flaw in BAN logic.