Fabio Massacci

AILAW Journal 2008 Journal Article

How to integrate legal requirements into a requirements engineering methodology for the development of security and privacy patterns

• Luca Compagna
• Paul El Khoury
• Alžběta Krausová
• Fabio Massacci
• Nicola Zannone

Abstract Laws set requirements that force organizations to assess the security and privacy of their IT systems and impose them to implement minimal precautionary security measures. Several IT solutions (e. g. , Privacy Enhancing Technologies, Access Control Infrastructure, etc.) have been proposed to address security and privacy issues. However, understanding why, and when such solutions have to be adopted is often unanswered because the answer comes only from a broader perspective, accounting for legal and organizational issues. Security engineers and legal experts should analyze the business goals of a company and its organizational structure and derive from there the points where security and privacy problems may arise and which solutions best fit such (legal) problems. The paper investigates the methodological support for capturing security and privacy requirements of a concrete health care provider.

TAAS Journal 2008 Journal Article

Interactive access control for autonomic systems

• Hristo Koshutanski
• Fabio Massacci

Autonomic communication and computing is a new paradigm for dynamic service integration over a network. An autonomic network crosses organizational and management boundaries and is provided by entities that see each other just as partners. For many services no autonomic partner may guess a priori what will be sent by clients nor clients know a priori what credentials are required to access a service. To address this problem we propose a new interactive access control: servers should interact with clients, asking for missing credentials necessary to grant access, whereas clients may supply or decline the requested credentials. Servers evaluate their policies and interact with clients until a decision of grant or deny is taken. This proposal is grounded in a formal model on policy-based access control. It identifies the formal reasoning services of deduction, abduction and consistency. Based on them, the work proposes a comprehensive access control framework for autonomic systems. An implementation of the interactive model is given followed by system performance evaluation.

TAAS Journal 2006 Journal Article

A survey of autonomic communications

• Simon Dobson
• Spyros Denazis
• Antonio Fernández
• Dominique Gaïti
• Erol Gelenbe
• Fabio Massacci
• Paddy Nixon
• Fabrice Saffre

Autonomic communications seek to improve the ability of network and services to cope with unpredicted change, including changes in topology, load, task, the physical and logical characteristics of the networks that can be accessed, and so forth. Broad-ranging autonomic solutions require designers to account for a range of end-to-end issues affecting programming models, network and contextual modeling and reasoning, decentralised algorithms, trust acquisition and maintenance---issues whose solutions may draw on approaches and results from a surprisingly broad range of disciplines. We survey the current state of autonomic communications research and identify significant emerging trends and techniques.

AIJ Journal 2000 Journal Article

EXPtime tableaux for ALC

• Francesco M. Donini
• Fabio Massacci

The last years have seen two major advances in Knowledge Representation and Reasoning. First, many interesting problems (ranging from Semi-structured Data to Linguistics) were shown to be expressible in logics whose main deductive problems are EXPtime-complete. Second, experiments in automated reasoning have substantially broadened the meaning of “practical tractability”. Instances of realistic size for Pspace-complete problems are now within reach for implemented systems. Still, there is a gap between the reasoning services needed by the expressive logics mentioned above and those provided by the current systems. Indeed, the algorithms based on tree-automata, which are used to prove EXPtime-completeness, require exponential time and space even in simple cases. On the other hand, current algorithms based on tableau methods can take advantage of such cases, but require double exponential time in the worst case. We propose a tableau calculus for the description logic ALC for checking the satisfiability of a concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based decision procedure working in single exponential time. To guarantee the ease of implementation, we also discuss the effects that optimizations (propositional backjumping, simplification, semantic branching, etc.) might have on our complexity result, and introduce a few optimizations ourselves.

TCS Journal 2000 Journal Article

The proof complexity of analytic and clausal tableaux

• Fabio Massacci

It is widely believed that a family Σn of unsatisfiable formulae proposed by Cook and Reckhow in their landmark paper (Proc. ACM Symp. on Theory of Computing, 1974) can be used to give a lower bound of 2 Ω(2n) on the proof size with analytic tableaux. This claim plays a key role in the proof that tableaux cannot polynomially simulate tree resolution. We exhibit an analytic tableau proof for Σn for whose size we prove an upper bound of O(2n2 ), which, although not polynomial in the size O(2n) of the input formula, is exponentially shorter than the claimed lower bound. An analysis of the proofs published in the literature reveals that the pitfall is the blurring of n-ary (clausal) and binary versions of tableaux. A consequence of this analysis is that a second widely held belief falls too: clausal tableaux are not just a more efficient notational variant of analytic tableaux for formulae in clausal normal form. Indeed clausal tableaux (and thus model elimination without lemmaizing) cannot polynomially simulate analytic tableaux.

AAAI Conference 1998 Conference Paper

Anytime Approximate Modal Reasoning

• Fabio Massacci

Propositional modal logics have two independent sources of complexity: unbounded logical omniscience and unbounded logical introspection. This paper discusses an approximation method to tame both of them, by merging propositional approximations with a new technique tailored for multi-modal logics. It provides both skeptical and credulous approximations (or approximation that are neither of the two). On this semantics we build an anytime proof procedure with a simple modification to classical modal tableaux. The procedure yields approximate proofs whose precision increases as we have more resources (time, space etc.) and we analyze its semantical and computational “quality guarantees”.

ECAI Conference 1998 Conference Paper

Cook and Reckhow are Wrong: Subexponential Tableaux Proofs for Their Family of Formulae

• Fabio Massacci

AAAI Conference 1996 Conference Paper

Contextual Reasoning Is NP-Complete

• Fabio Massacci

The logic of context with the ist (c, p) modality has been proposed by McCarthy as a foundation for contextual reasoning. This paper shows that propositional logic of context is NP-complete and therefore more tractable than multimodal logics or Multi Language hierarchical logics which are PSPACE-complete, This result is given in a proof-theoretical way by providing a tableau calculus, which can be used as a decision procedure for automated reasoning. The computational gap between logic of context and modal logics is analyzed and some indications for the use of either formalisms are drawn on the basis of the tradeoff between compactness of representation and tractability of reasoning.