Catálogo de publicaciones - libros

Fern is an updatable cryptographically authenticated dictionary developed to propagate identification and authorization information within distributed systems. Fern incrementally distributes components of its dictionary as required to satisfy client requests and thus is suitable for deployments where clients are likely to require only a small fraction of a dictionary’s contents and connectivity may be limited. When dictionary components must be obtained remotely, the latency of lookup and validation operations is dominated by communication time. This latency can be reduced with locality-sensitive caching of dictionary components. Fern dictionary’s components are suitable for caching and distribution via autonomic scalable locality-aware Content Distribution Networks (CDNs) and therefore can provide these properties without requiring the provisioning of a dedicated distribution infrastructure. Competitive approaches require either the sequential transfer of two-to-three times more vertices or the replacement of a greater number of already distributed vertices when updates occur.

Electronic messages authentication issue is of significant importance for computer systems. A number of public key cryptosystems based on the composite modulus ( n=pq , where p and q are large primes) has been proposed to provide information authentication and only for one of them (that has been proposed by M. Rabin) security has been proved formally. In this paper we generalize the M. Rabin’s public key encryption and digital signature schemes and present formal proof of the security of the class of public key cryptosystems based on difficulty of the factorization problem.

The emergence of powerful, full-featured and small form-factor mobile devices enables rich services to be offered to it’s users. As the mobile user interacts with multiple administrative domains, he acquires various attributes. In such dynamic usage scenarios, attributes from one domain are interpreted and used in another domain. This motivates the need for dynamic authorization at the time of interaction. In this paper, we investigate the requirements of multi-domain interactions and explore a new paradigm for modeling these requirements using the UCON model for Usage Control [5]. We propose extensions to UCON in order to accommodate dynamic authorizations requirements.

In this paper, we focus on distributed systems subject to security issues. Such systems are usually composed of two entities: a high level user and a low level user that can both do some actions. The security properties we consider are non-interference properties. A system is non-interferent if the low level user cannot deduce any information by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we focus on two of them: one trace-based property (SNNI) and another bisimulation-based property (BSNNI). For these properties we study the problems of synthesis of a high level user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.

Trust management systems provide a flexible way for performing decentralized security management. However, most trust management systems only support monotonic policies. Compared with nonmonotonic policies, monotonic ones are less flexible and cannot express policies such as “Chinese wall policies” and “separation of duties”. To support non-monotonic policies, trust management systems must be able to correctly identify the credentials which a subject has that are required by the policies. Previous efforts address the problem by letting the system query the issuers directly to verify the possession status of the credentials. But this approach can violate the subject’s privacy. The main contribution of this paper is a cryptographic credential verification scheme for non-monotonic, trust management systems that can correctly identify the credentials that a subject has while also protecting the subject’s privacy. We also analyze the security of the scheme and prove that with correct construction and certain cryptographic assumptions, the scheme is secure.

We consider a sequence of finite products of a finite set. A statistical test problem is defined on every product. Consistent sequences of probability measures on these products of the set generate probability measures on the set of infinite sequences. Sufficient conditions of nonexistence for consistent test sequences are proved. These results may be interpreted from the point of view of covert channel secrecy.

One of topical tasks of policy-based security management is checking that the security policy stated in organization corresponds to its implementation in the computer network. The paper considers the suggested approach to proactive monitoring of security policy performance and security mechanisms functioning. This approach is based on the different strategies of automatic imitation of possible users’ actions in the computer network, including exhaustive search, express-analysis and generating the optimized test sequences. It is applicable to different security policies (authentication, authorization, filtering, communication channel protection, etc.). The paper describes stages, generalized algorithms and main peculiarities of the suggested approach and formal methods used to fulfill the test sequence optimization. We consider the generalized architecture of the proactive monitoring system “Proactive security scanner” (PSC) developed, its implementation and an example of policy testing.

The ability to efficiently compare differing, security solutions for effectiveness is often considered lacking from a management perspective. To address this we propose a methodology for estimating the mean time-to-compromise (MTTC) of a target device or network as a comparative metric. A topological map of the target system is divided into attack zones, allowing each zone to be described with its own state-space model (SSM). We then employ a SSM based on models used in the biological sciences to predict animal behavior in the context of predator prey relationships. Markov chains identify predominant attacker strategies which are used to build the MTTC intervals which can be compared for a broad range of mitigating actions. This allows security architects and managers to intelligently select the most effective solution, based on the lowest cost/MTTC ratio that still exceeds a benchmark level.

Safety critical and business critical systems are usually controlled by policies with the objective to guarantee a variety of safety, liveness and security properties. Traditional model checking techniques allow a verification of the required behaviour only for systems with very few components. To be able to verify entire families of systems, independent of the exact number of replicated components, we developed an abstraction based approach to extend our current tool supported verification techniques to such families of systems that are usually parameterised by a number of replicated identical components. We demonstrate our technique by an exemplary verification of security and liveness properties of a simple parameterised collaboration scenario. Verification results for configurations with fixed numbers of components are used to choose an appropriate property preserving abstraction that provides the basis for an inductive proof that generalises the results for a family of systems with arbitrary settings of parameters.

The management of security for large and complex environments still represents an open problem and the policy-based systems are certainly one of the most innovative and effective solution to this problem. The policy, that at low level is expressed by sets of rules, becomes crucial for the consistency of the systems to be protected and it is necessary to check it for correctness. This paper presents a set-based model of rules that permits the static conflict detection and an axiomatic model of conflict resolution leading to semi-lattices theory to solve inconsistencies. We proved the effectiveness of the theory implementing an extensible tool supporting security officers in creating rules by providing an easy environment to identify the conflicts and to use manual as well as automatic resolution strategies.