-
On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials
Authors:
Andrea Flamini,
Giada Sciarretta,
Mario Scuro,
Amir Sharif,
Alessandro Tomasi,
Silvio Ranise
Abstract:
Verifiable credentials are a digital analogue of physical credentials. Their authenticity and integrity are protected by means of cryptographic techniques, and they can be presented to verifiers to reveal attributes or even predicates about the attributes included in the credential. One way to preserve privacy during presentation consists in selectively disclosing the attributes in a credential. I…
▽ More
Verifiable credentials are a digital analogue of physical credentials. Their authenticity and integrity are protected by means of cryptographic techniques, and they can be presented to verifiers to reveal attributes or even predicates about the attributes included in the credential. One way to preserve privacy during presentation consists in selectively disclosing the attributes in a credential. In this paper we present the most widespread cryptographic mechanisms used to enable selective disclosure of attributes identifying two categories: the ones based on hiding commitments - e.g., mdl ISO/IEC 18013-5 - and the ones based on non-interactive zero-knowledge proofs - e.g., BBS signatures. We also include a description of the cryptographic primitives used to design such cryptographic mechanisms. We describe the design of the cryptographic mechanisms and compare them by performing an analysis on their standard maturity in terms of standardization, cryptographic agility and quantum safety, then we compare the features that they support with main focus on the unlinkability of presentations, the ability to create predicate proofs and support for threshold credential issuance. Finally we perform an experimental evaluation based on the Rust open source implementations that we have considered most relevant. In particular we evaluate the size of credentials and presentations built using different cryptographic mechanisms and the time needed to generate and verify them. We also highlight some trade-offs that must be considered in the instantiation of the cryptographic mechanisms.
△ Less
Submitted 16 January, 2024;
originally announced January 2024.
-
Identifying and Quantifying Trade-offs in Multi-Stakeholder Risk Evaluation with Applications to the Data Protection Impact Assessment of the GDPR
Authors:
Majid Mollaeefar,
Silvio Ranise
Abstract:
Cybersecurity risk management consists of several steps including the selection of appropriate controls to minimize risks. This is a difficult task that requires to search through all possible subsets of a set of available controls and identify those that minimize the risks of all stakeholders. Since stakeholders may have different perceptions of the risks (especially when considering the impact o…
▽ More
Cybersecurity risk management consists of several steps including the selection of appropriate controls to minimize risks. This is a difficult task that requires to search through all possible subsets of a set of available controls and identify those that minimize the risks of all stakeholders. Since stakeholders may have different perceptions of the risks (especially when considering the impact of threats), conflicting goals may arise that require to find the best possible trade-offs among the various needs. In this work, we propose a quantitative and (semi)automated approach to solve this problem based on the well-known notion of Pareto optimality. For validation, we show how a prototype tool based on our approach can assist in the Data Protection Impact Assessment mandated by the General Data Protection Regulation on a simplified but realistic use case scenario. We also evaluate the scalability of the approach by conducting an experimental evaluation with the prototype with encouraging results.
△ Less
Submitted 15 July, 2022;
originally announced July 2022.
-
Blockchain Tree for eHealth
Authors:
Sergii Kushch,
Silvio Ranise,
Giada Sciarretta
Abstract:
The design of access control mechanisms for healthcare systems is challenging: it must strike the right balance between permissions and restrictions. In this work, we propose a novel approach that is based on the Blockchain technology for storage patient medical data and create an audit logging system able to protect health data from unauthorized modification and access. The proposed method consis…
▽ More
The design of access control mechanisms for healthcare systems is challenging: it must strike the right balance between permissions and restrictions. In this work, we propose a novel approach that is based on the Blockchain technology for storage patient medical data and create an audit logging system able to protect health data from unauthorized modification and access. The proposed method consists of a tree structure: a main chain linked with the patient's identity and one or several Subchains which are used for storing additional critical data (e.g., medical diagnoses or access logs).
△ Less
Submitted 13 August, 2019;
originally announced August 2019.
-
PADS: Practical Attestation for Highly Dynamic Swarm Topologies
Authors:
Moreno Ambrosin,
Mauro Conti,
Riccardo Lazzeretti,
Md Masoom Rabbani,
Silvio Ranise
Abstract:
Remote attestation protocols are widely used to detect device configuration (e.g., software and/or data) compromise in Internet of Things (IoT) scenarios. Unfortunately, the performances of such protocols are unsatisfactory when dealing with thousands of smart devices. Recently, researchers are focusing on addressing this limitation. The approach is to run attestation in a collective way, with the…
▽ More
Remote attestation protocols are widely used to detect device configuration (e.g., software and/or data) compromise in Internet of Things (IoT) scenarios. Unfortunately, the performances of such protocols are unsatisfactory when dealing with thousands of smart devices. Recently, researchers are focusing on addressing this limitation. The approach is to run attestation in a collective way, with the goal of reducing computation and communication. Despite these advances, current solutions for attestation are still unsatisfactory because of their complex management and strict assumptions concerning the topology (e.g., being time invariant or maintaining a fixed topology). In this paper, we propose PADS, a secure, efficient, and practical protocol for attesting potentially large networks of smart devices with unstructured or dynamic topologies. PADS builds upon the recent concept of non-interactive attestation, by reducing the collective attestation problem into a minimum consensus one. We compare PADS with a state-of-the art collective attestation protocol and validate it by using realistic simulations that show practicality and efficiency. The results confirm the suitability of PADS for low-end devices, and highly unstructured networks.
△ Less
Submitted 14 June, 2018;
originally announced June 2018.
-
A Survey on Workflow Satisfiability, Resiliency, and Related Problems
Authors:
Daniel Ricardo dos Santos,
Silvio Ranise
Abstract:
Workflows specify collections of tasks that must be executed under the responsibility or supervision of human users. Workflow management systems and workflow-driven applications need to enforce security policies in the form of access control, specifying which users can execute which tasks, and authorization constraints, such as Separation of Duty, further restricting the execution of tasks at run-…
▽ More
Workflows specify collections of tasks that must be executed under the responsibility or supervision of human users. Workflow management systems and workflow-driven applications need to enforce security policies in the form of access control, specifying which users can execute which tasks, and authorization constraints, such as Separation of Duty, further restricting the execution of tasks at run-time. Enforcing these policies is crucial to avoid frauds and malicious use, but it may lead to situations where a workflow instance cannot be completed without the violation of the policy. The Workflow Satisfiability Problem (WSP) asks whether there exists an assignment of users to tasks in a workflow such that every task is executed and the policy is not violated. The WSP is inherently hard, but solutions to this problem have a practical application in reconciling business compliance and business continuity. Solutions to related problems, such as workflow resiliency (i.e., whether a workflow instance is still satisfiable even in the absence of users), are important to help in policy design. Several variations of the WSP and similar problems have been defined in the literature and there are many solution methods available. In this paper, we survey the work done on these problems in the past 20 years.
△ Less
Submitted 22 June, 2017;
originally announced June 2017.
-
A Declarative Framework for Specifying and Enforcing Purpose-aware Policies
Authors:
Riccardo De Masellis,
Chiara Ghidini,
Silvio Ranise
Abstract:
Purpose is crucial for privacy protection as it makes users confident that their personal data are processed as intended. Available proposals for the specification and enforcement of purpose-aware policies are unsatisfactory for their ambiguous semantics of purposes and/or lack of support to the run-time enforcement of policies.
In this paper, we propose a declarative framework based on a first-…
▽ More
Purpose is crucial for privacy protection as it makes users confident that their personal data are processed as intended. Available proposals for the specification and enforcement of purpose-aware policies are unsatisfactory for their ambiguous semantics of purposes and/or lack of support to the run-time enforcement of policies.
In this paper, we propose a declarative framework based on a first-order temporal logic that allows us to give a precise semantics to purpose-aware policies and to reuse algorithms for the design of a run-time monitor enforcing purpose-aware policies. We also show the complexity of the generation and use of the monitor which, to the best of our knowledge, is the first such a result in literature on purpose-aware policies.
△ Less
Submitted 29 July, 2015;
originally announced July 2015.
-
Modularity for Security-Sensitive Workflows
Authors:
Daniel Ricardo dos Santos,
Silvio Ranise,
Serena Elisa Ponta
Abstract:
An established trend in software engineering insists on using components (sometimes also called services or packages) to encapsulate a set of related functionalities or data. By defining interfaces specifying what functionalities they provide or use, components can be combined with others to form more complex components. In this way, IT systems can be designed by mostly re-using existing component…
▽ More
An established trend in software engineering insists on using components (sometimes also called services or packages) to encapsulate a set of related functionalities or data. By defining interfaces specifying what functionalities they provide or use, components can be combined with others to form more complex components. In this way, IT systems can be designed by mostly re-using existing components and develo** new ones to provide new functionalities. In this paper, we introduce a notion of component and a combination mechanism for an important class of software artifacts, called security-sensitive workflows. These are business processes in which execution constraints on the tasks are complemented with authorization constraints (e.g., Separation of Duty) and authorization policies (constraining which users can execute which tasks). We show how well-known workflow execution patterns can be simulated by our combination mechanism and how authorization constraints can also be imposed across components. Then, we demonstrate the usefulness of our notion of component by showing (i) the scalability of a technique for the synthesis of run-time monitors for security-sensitive workflows and (ii) the design of a plug-in for the re-use of workflows and related run-time monitors inside an editor for security-sensitive workflows.
△ Less
Submitted 27 July, 2015;
originally announced July 2015.
-
Automated Analysis of Scenario-based Specifications of Distributed Access Control Policies with Non-Mechanizable Activities (Extended Version)
Authors:
Michele Barletta,
Silvio Ranise,
Luca Viganò
Abstract:
The advance of web services technologies promises to have far-reaching effects on the Internet and enterprise networks allowing for greater accessibility of data. The security challenges presented by the web services approach are formidable. In particular, access control solutions should be revised to address new challenges, such as the need of using certificates for the identification of users an…
▽ More
The advance of web services technologies promises to have far-reaching effects on the Internet and enterprise networks allowing for greater accessibility of data. The security challenges presented by the web services approach are formidable. In particular, access control solutions should be revised to address new challenges, such as the need of using certificates for the identification of users and their attributes, human intervention in the creation or selection of the certificates, and (chains of) certificates for trust management. With all these features, it is not surprising that analyzing policies to guarantee that a sensitive resource can be accessed only by authorized users becomes very difficult. In this paper, we present an automated technique to analyze scenario-based specifications of access control policies in open and distributed systems. We illustrate our ideas on a case study arising in the e-government area.
△ Less
Submitted 14 June, 2012;
originally announced June 2012.
-
Quantifier-Free Interpolation of a Theory of Arrays
Authors:
Roberto Bruttomesso,
Silvio Ghilardi,
Silvio Ranise
Abstract:
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier- free interpolants in general. In this paper, we show that it is possible to obtain quantifier-free interpolants for a Skolemized vers…
▽ More
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier- free interpolants in general. In this paper, we show that it is possible to obtain quantifier-free interpolants for a Skolemized version of the extensional theory of arrays. We prove this in two ways: (1) non-constructively, by using the model theoretic notion of amalgamation, which is known to be equivalent to admit quantifier-free interpolation for universal theories; and (2) constructively, by designing an interpolating procedure, based on solving equations between array updates. (Interestingly, rewriting techniques are used in the key steps of the solver and its proof of correctness.) To the best of our knowledge, this is the first successful attempt of computing quantifier- free interpolants for a variant of the theory of arrays with extensionality.
△ Less
Submitted 26 April, 2012; v1 submitted 11 April, 2012;
originally announced April 2012.
-
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
Authors:
Roberto Bruttomesso,
Silvio Ghilardi,
Silvio Ranise
Abstract:
The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories hav…
▽ More
The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the 'strong (sub-)amalgamation' property. Then, we provide an equivalent syntactic characterization, identify a sufficient condition, and design a combined quantifier-free interpolation algorithm capable of handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.
△ Less
Submitted 24 April, 2012; v1 submitted 16 March, 2012;
originally announced March 2012.
-
Automated Symbolic Analysis of ARBAC-Policies (Extended Version)
Authors:
A. Armando,
S. Ranise
Abstract:
One of the most widespread framework for the management of access-control policies is Administrative Role Based Access Control (ARBAC). Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One limitation of many available techniques is that the sets of users and roles are bounded. In this paper, we propose a symbolic framewor…
▽ More
One of the most widespread framework for the management of access-control policies is Administrative Role Based Access Control (ARBAC). Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One limitation of many available techniques is that the sets of users and roles are bounded. In this paper, we propose a symbolic framework to overcome this difficulty. We design an automated security analysis technique, parametric in the number of users and roles, by adapting recent methods for model checking infinite state systems that use first-order logic and state-of-the-art theorem proving techniques. Preliminary experiments with a prototype implementations seem to confirm the scalability of our technique.
△ Less
Submitted 27 December, 2010;
originally announced December 2010.
-
Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
Authors:
Silvio Ghilardi,
Silvio Ranise
Abstract:
The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verif…
▽ More
The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we present a fully declarative and symbolic approach to the mechanization of backward reachability of infinite state systems manipulating arrays by Satisfiability Modulo Theories solving. Theories are used to specify the topology and the data manipulated by the system. We identify sufficient conditions on the theories to ensure the termination of backward reachability and we show the completeness of a method for invariant synthesis (obtained as the dual of backward reachability), again, under suitable hypotheses on the theories. We also present a pragmatic approach to interleave invariant synthesis and backward reachability so that a fix-point for the set of backward reachable states is more easily obtained. Finally, we discuss heuristics that allow us to derive an implementation of the techniques in the model checker MCMT, showing remarkable speed-ups on a significant set of safety problems extracted from a variety of sources.
△ Less
Submitted 21 December, 2010; v1 submitted 9 October, 2010;
originally announced October 2010.
-
Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)
Authors:
Alberto Calvi,
Silvio Ranise,
Luca Viganò
Abstract:
We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reachability problems. To assess the practical viability of our approach, we have de…
▽ More
We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reachability problems. To assess the practical viability of our approach, we have developed a prototype tool implementing our techniques and applied it to a digital contract signing service inspired by an industrial case study.
△ Less
Submitted 7 September, 2010;
originally announced September 2010.
-
Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)
Authors:
Michele Barletta,
Silvio Ranise,
Luca Viganò
Abstract:
A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits on…
▽ More
A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide the right level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions.
In this paper, we present a two-level formal verification framework to overcome these problems and formally reason about the interplay of authorization policies and workflow in service-oriented architectures. This allows us to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability.
△ Less
Submitted 25 June, 2009;
originally announced June 2009.
-
New results on rewrite-based satisfiability procedures
Authors:
Alessandro Armando,
Maria Paola Bonacina,
Silvio Ranise,
Stephan Schulz
Abstract:
Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisfi…
▽ More
Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure. We prove termination of a rewrite-based first-order engine on the theories of records, integer offsets, integer offsets modulo and lists. We give a modularity theorem stating sufficient conditions for termination on a combinations of theories, given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability, and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.
△ Less
Submitted 31 May, 2008; v1 submitted 12 April, 2006;
originally announced April 2006.
