Journal of Computer Security

Protection and secure exchange of Web documents is becoming a crucial need for many Internet-based applications. Securing Web documents entail addressing two main issues: confidentiality and integrity. Ensuring document confidentiality means that document contents can only be disclosed to subjects authorized according to specified security policies, whereas by document integrity we mean that the document contents are correct with respect to a given application domain and that the document contents are modified only by authorized subjects. While the problem of document confidentiality has been widely investigated in the literature, the problem of how to ensure that a document, when moving among different parties, is modified only according to the stated policies still lacks comprehensive solutions. In this paper we present a solution to this problem by proposing a model for specifying update policies, and an infrastructure supporting the specification and enforcement of these policies in a distributed and cooperative environment, in which subjects in different organizational roles can modify possibly different portions of the same document. The key aspect of our proposal is that, by using a combination of hash functions and digital signature techniques, we create a distributed environment that enables subjects, in most cases, to verify, upon receiving a document, whether the update operations performed on the document up to that point are correct with respect to the update policies, without interacting with the document server. Our approach is particularly suited for environments, such as mobile systems, pervasive systems, decentralized workflows, and peer-to-peer systems.

This document presents an efficient, high quality random number generator for multi-programmed environments, in particular for UNIX/Linux and Windows systems. The algorithm uses a system's notion of the time, given by a high-precision real-time counter, to obtain random bits, and a combination of system calls to reduce the correlation between consecutive random bits. The combination of system calls introduces variable and unpredictable real-time gaps in the execution of the generator. We present a rationale for such variation and unpredictability, and we show that in fact they exist even when the generator runs in an adverse scenario, i.e., a lightly loaded system. We also show how the generator resists several attacks attempting to guess or control the values it produces. The quality of the generator is evaluated both in terms of its performance and the randomness of the byte sequences it produces. Comparing against other similar generators, CryptoLib and librand, our generator produces equally good random byte sequences, but its performance increases with the speed of the processor, while the performance of CryptoLib and librand is rather constant for each operating system, independently of the processor were it runs.

Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev–Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Strand spaces provide a simple and economical approach to analysis of completed protocol runs by emphasizing causal interactions among protocol participants. The multiset rewriting formalism provides a very precise way of specifying finite-length protocols with unboundedly many instances of each protocol role, such as client, server, initiator, or responder. A number of modifications to each system are required to produce a meaningful comparison. In particular, we extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands. The relationship we illustrate here between multiset rewriting specifications and strand spaces thus suggests refinements to both frameworks, and deepens our understanding of the Dolev–Yao model.

Schneider's work on rank functions [IEEE TSE 24(9) (1998)] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a protocol running on a small network; and no help is given with the somewhat hit-and-miss process of finding the rank function that underpins the central theorem.

In this paper, we develop the theory to allow for an arbitrarily large network, and give a clearly defined decision procedure by which one may either construct a rank function, proving correctness of the protocol, or show that no rank function exists.

We briefly discuss the implications of the absence of a rank function, and the open question of completeness of the rank function theorem.