Journal of Computer Security

In this paper we develop methods for analyzing key management and authentication protocols using techniques developed for the solutions of equations in a term rewriting system. In particular, we describe a model of a class of protocols and possible attacks on those protocols as term rewriting systems, and we also describe a software tool based on a narrowing algorithm that can be used in the analysis of such protocols. We formally model a protocol and describe the results of using these techniques to analyze security properties. We show how a security flaw was found, and we also describe the verification of a corrected scheme using these techniques.

The trace method of software specification is extended to provide a natural semantics for a procedural programming language. This extension provides a method for proving program correctness that permits a direct proof of program Noninterference without having to produce an intermediate finite state machine and unwinding conditions. This approach provides a uniform framework for reasoning about abstract software system specifications and their implementations. It also allows us to prove security at an abstract level so that changes to programs that do not affect functional behavior will not affect the security proof.

In this paper we show that the Schematic Protection Model (SPM) subsumes several well-known protection models as particular instances. We show this for a diverse collection of models including the Bell-LaPadula multilevel security model, take-grant models, and grammatical protection systems. Remarkably SPM subsumes these models within its known efficiently decidable cases for safety analysis (i.e., the determination or whether or not a given privilege can possibly be acquired by a particular subject). Therefore SPM subsumes these models not only in terms of its expressive power but also in terms of safety analysis. This is in sharp contrast to the Harrison-Ruzzo-Ullman (HRU) access-matrix model. HRU does subsume all the models discussed in this paper in terms of expressive power. However, all known constructions of these models in HRU require multi-conditional commands (i.e., commands whose conditions have two or more terms), whereas safety is undecidable in HRU even for bi-conditional commands (i.e., commands whose conditions have exactly two terms).

In the context of the modal logic of security, confidentiality is defined by the formula K B φ → R B φ that could be read “If B knows φ then B should have the permission to know φ”. We propose a new semantics for the R B modal operator, such that the definition of security would allow a certain number of dependencies (called secure dependencies) between objects of the system. We formally compare this new definition of security with non-interference, non-deducibility and generalized non-interference, especially with respect to assumptions of non-determinism and input-totalness.