The transition from centralized identity architecture to a decentralized one introduces profound shifts in the privacy protection of users’ data. Yet, as decentralized identity continues to mature, today’s online services still overwhelmingly depend on centralized and federated identity management solutions built on top of OpenID Connect (OIDC) as the most widespread solution. Ensuring privacy-preserving OIDC deployments is therefore critical for safeguarding users’ personal data and maintaining compliance with regulatory frameworks such as the General Data Protection Regulation (GDPR) and trust frameworks such as the Electronic Identification, Authentication and Trust Services (eIDAS). However, the current OIDC ecosystem lacks a coherent set of privacy Best Current Practices (BCPs) and a study of how widely these privacy-enhancing features are adopted in real-world deployments. To this end, this work addresses the aforementioned gaps on two fronts. First, we propose a structured set of privacy BCPs derived from official OIDC specifications and current implementation trends, identifying easy-to-deploy privacy-enhancing features that strengthen the OIDC deployments’ baseline privacy without altering the protocol or compromising interoperability. Furthermore, the BCPs also help achieve the GDPR privacy principles, such as data minimization, confidentiality, and unlinkability. Second, this work provides a comprehensive survey of OpenID Providers (OPs) in the wild to identify gaps in privacy-preserving configurations in both private and public (i.e., national) sectors OPs. The study employs a dual methodology: first, a manual review performed in 2022; subsequently, an automated compliance analysis performed in 2025 surveying a dataset of 10000 OPs worldwide. The results reveal a concerning lack of privacy-enhancing features among private OPs and a wide gap between private and national OPs, with the latter group providing, on average, much higher baseline privacy. We have also found a prevalence of OPs not complying with the OIDC specifications, resulting in misconfigured OPs hampering interoperability and, in some cases, security. The paper emphasizes the importance of adopting actionable BCPs to improve baseline privacy and demonstrates the need for an automated framework for ongoing privacy compliance assessments in OIDC ecosystems.

The proliferation of AI conversation platforms has introduced unprecedented privacy risks through user-shared conversations. This paper presents a comprehensive analysis of privacy vulnerabilities in shared conversations across three major LLM platforms: ChatGPT, Microsoft Copilot, and Google Gemini. We collected and analyzed 100 342 conversations using an automated LLM-based privacy detection pipeline enhanced with a defined risk scoring system and the LINDDUN threat modeling framework. Our analysis identifies 8 131 conversations (8%) to incur privacy risks deriving from the disclosure of private and sensitive data including user identifiers (49%) and user location data (40%), yet in some cases also financial (4%), health (3%) and authentication data such as access tokens (3%). Through systematic analysis of conversation length and temporal disclosure patterns, we demonstrate that extended conversations exhibit higher privacy risk rates compared to brief interactions. Notably, 60% of private data disclosures in longer con- versation occur in the final quartile of these conversations, which may indicate that users progressively lose privacy awareness as interactions deepen. Our findings have immediate implications for platform designers and policymakers, highlighting the need for proactive interventions including real-time privacy warnings, pre- share scanning, and clearer education about the permanence and discoverability of shared conversation links.

Cryptographic Access Control (CAC) allows organizations to control cloud-hosted data sharing among users while preventing external attackers, malicious insiders, and honest-but-curious cloud providers from accessing the data. However, CAC entails an overhead often impractical for real-world scenarios due to the many cryptographic computations involved. Hence, we put forth a hybrid Access Control (AC) scheme --- combining CAC and (traditional) centralized AC --- that considers trust assumptions (e.g., on users) and data protection requirements of the underlying scenario on a case-by-case basis to reduce the number of cryptographic computations to execute in CAC. Besides, we design a consistency check to ensure the correctness and safety properties of the enforcement of the hybrid AC scheme, provide a proof-of-concept implementation in Prolog, and conduct a preliminary experimental evaluation.

Abstract The European Digital Identity Wallet (EUDI Wallet) plays a pivotal role in shaping digital identity across the EU, necessitating a secure storage solution compliant with eIDAS2 regulation. In this study, we first analyze mobile secure storage solutions for the EUDI Wallet, identifying any gaps between current offerings and the EUDI Wallet’s requirements. Our analysis indicates a significant shortfall in the availability of mobile native solutions, with only approximately 10.5% of mobile phones in the Italian market currently adhering to the stringent requirements mandated by eIDAS2. Consequently, we explore and evaluate alternative design solutions in terms of their feasibility and integration potential.

The Single Sign-On based account linking process (SSOLinking in short) allows users to link their accounts at Service Provider (SP) websites to their Identity Providers (IdP) accounts. We focus on a serious (and overlooked) attack, namely an Account Hijack targeting the SSOLinking and relying on two CSRF vulnerabilities, one affecting the IdP and the other the SP. The former is an Authentication CSRF (also known as Login CSRF) and the latter is a CSRF on the button triggering the SSOLinking. We propose a security testing approach to help testers automatically detect such attacks. We implemented our testing technique as an extension (namely SSOLinking Checker) to the open-source penetration testing tool Micro-Id-Gym. To demonstrate the effectiveness of our approach and the pervasiveness of the SSOLinking Account Hijack, we conducted an experimental analysis against a selection of popular SPs that offer the SSOLinking with major IdPs. The results of our experiments are alarming: out of the 648 web sites we considered, 48 qualified for conducting our experiments and 21 of these suffered from SSOLinking vulnerability (i.e. 43.7%). Our findings (we responsibly disclosed to the affected vendors) include severe vulnerabilities among the web sites of Goodreads, Naver, Workable, etc.

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.

Authentication protocols represent the entry point to online services, so they must be sturdily designed in order to allow only authorized users to access the underlying data. However, designing authentication protocols is a complex process: security designers should carefully select the technologies to involve and integrate them properly in order to prevent potential vulnerabilities. In addition, these choices are usually restricted by further factors, such as the requirements associated with the scenario, the regulatory framework, the dimensions to balance (e.g., security vs. usability), and the standards to rely on. We come to the rescue by presenting an automated multi-layered methodology we have developed to assist security designers in this phase: by repeatedly evaluating their protocols, they can select the security mitigations to consider until they reach the desired security level, thus enabling a security-by-design approach. For concreteness, we also show how we have applied our methodology to a real use case scenario in the context of a collaboration with the Italian Government Printing Office and Mint.

An Attribute Authority is an entity responsible for establishing, maintaining, and sharing a subject’s qualified attributes, such as titles and qualifications. In the OpenID Connect digital identity ecosystem, In the OpenID Connect digital identity ecosystem, for privacy reasons, this entity is distinct from Identity Providers that manage only the basic identity profile information. A relevant scenario is as follows: the User first logs in to an online service using his/her identity managed by an Identity Provider. Then, the online service asks the Attribute Authority for the additional User’s attributes (e.g., entitlements) before granting access to its resources. In some high-sensitive cases, an Attribute Authority needs proof of the User’s authentication before releasing the User’s attributes to the online service. The challenge of this scenario involving usability, security, and privacy requirements lies in finding the right mechanism to share (the minimum and necessary set of) claims of the User who is currently authenticated with the online service across multiple domains without requiring his or her re-authentication. In this paper, we present the design of two solutions based on OpenID Connect to share User claims across domains. We provide security and privacy analysis for the two solutions and a brief comparison between them.

Intelligent Transport Systems (ITS) are crucial to support Situation Awareness (SA), which aims to keep a safe and efficient driving experience. While promising, ITS use for SA brings several security challenges, including enforcing access control policies in distributed environments with stringent computational constraints in terms of availability, consistency, and latency. Consequently, traditional mechanisms used to enforce authorization policies cannot be reused off-the-shelf but need to be carefully adapted to the particular requirements and minimize the overhead of access control enforcement. In this paper, we propose a distributed architecture for access control enforcement for ITS capable of satisfying the requirements of SA scenarios based on the idea of dynamically compiling a high-level specification of access control policies (written in the Attribute-Based Access Control model) into a set of low-level Access Control Lists that are easier to enforce. We discuss how to realize it by reusing well-known techniques developed in the field of distributed systems. To evaluate the applicability of the proposed approach, we build a prototype that we use to conduct an experimental evaluation in the context of two practical use case scenarios.

The eIDAS Regulation aims to provide an interoperable European framework to enable EU citizens to authenticate and communicate with services of other Member States by using their national electronic identity. While a set of high-level requirements (e.g., related to privacy and security) are established to make interoperability among Member States possible, the eIDAS Regulation does not explicitly specify the technologies that can be adopted during the development phase to meet the requirements as mentioned earlier. This paper considers the technological trends of (pre)notified eIDAS electronic identity schemes used by Member States, and they satisfy the eIDAS regulation requirements. We do this by defining a set of research questions that allow us to investigate the correlations between different design dimensions such as security, privacy, and usability. Based on these findings, we provide a set of lessons learned that can be used by the security community to protect interoperable national digital identities more efficiently.

While being both extremely powerful and popular, TLS is a protocol that is hard to securely deploy. On the one hand, system administrators are required to grasp several security concepts to fully understand the impact of each option and avoid misconfigurations. On the other hand, app developers should use cryptographic libraries in a secure way avoiding dangerous default settings or other subtleties (e.g., padding or modes of operations). To help secure TLS, we propose a modular framework, extensible with new features and capable of streamlining the mitigation process of known and newly discovered TLS attacks even for non-expert users.

To grasp the security implications of the various TLS configuration options, system administrators and app developers must be familiar with a wide range of concepts, including cryptography. To assist users in this task, we propose TLSAssistant- a modular and extensible framework designed to streamline the discovery and mitigation of potential vulnerabilities in TLS deployments. This demo will focus on two of the four available analysis types.

To facilitate the adoption of cloud by organizations, Cryptographic Access Control (CAC) is the obvious solution to control data sharing among users while preventing partially trusted Cloud Service Providers (CSP) from accessing sensitive data. Indeed, several CAC schemes have been proposed in the literature. Despite their differences, available solutions are based on a common set of entities—e.g., a data storage service or a proxy mediating the access of users to encrypted data—that operate in different (security) domains—e.g., on-premise or the CSP. However, the majority of these CAC schemes assumes a fixed assignment of entities to domains; this has security and usability implications that are not made explicit and can make inappropriate the use of a CAC scheme in certain scenarios with specific trust assumptions and requirements. For instance, assuming that the proxy runs at the premises of the organization avoids the vendor lock-in effect but may give rise to other security concerns (e.g., malicious insiders attackers). To the best of our knowledge, no previous work considers how to select the best possible architecture (i.e., the assignment of entities to domains) to deploy a CAC scheme for the trust assumptions and requirements of a given scenario. In this article, we propose a methodology to assist administrators in exploring different architectures for the enforcement of CAC schemes in a given scenario. We do this by identifying the possible architectures underlying the CAC schemes available in the literature and formalizing them in simple set theory. This allows us to reduce the problem of selecting the most suitable architectures satisfying a heterogeneous set of trust assumptions and requirements arising from the considered scenario to a decidable Multi-objective Combinatorial Optimization Problem (MOCOP) for which state-of-the-art solvers can be invoked. Finally, we show how we use the capability of solving the MOCOP to build a prototype tool assisting administrators to preliminarily perform a “What-if” analysis to explore the trade-offs among the various architectures and then use available standards and tools (such as TOSCA and Cloudify) for automated deployment in multiple CSPs.

Besides developing new Cooperative, Connected and Automated Mobility (CCAM) services for the improvement of road safety and travel experience, researchers are considering protection mechanisms to ensure the security of these services and the safety of involved users (drivers but also, e.g., cyclists and pedestrians). In particular, several Identity Management (IDM) protocols have been designed as the first line of defence against external attackers. Among these protocols, a promising trend in research consists in the use of a Smart Card (SC) as a technical enabler for strong authentication. Indeed, many SC-based IDM protocols for Vehicle-to-Vehicle (V2V) and Vehicle-to-Infrastructure (V2I) communications in real-time CCAM services have been proposed in the literature which present interesting features and promising usability experimental results. However, this research line is far from being exhausted, especially considering the recent spread of SC technologies and use cases. For this reason, in this paper we propose a systematic literature review on SC-based IDM protocols for real-time CCAM services. In particular, we identify characterising assumptions of CCAM scenarios and extrapolate a unified high-level view of the steps composing a SC-based IDM protocol. Then, we present a detailed survey of several SC-based IDM protocols. Finally, we identify trends in research and formulate guidelines and useful recommendations to provide a solid base which researchers can use as a starting point for the design of new and improved SC-based IDM protocols for CCAM scenarios.

Several automated tools have been proposed to detect vulnerabilities. These tools are mainly evaluated in terms of their accuracy in detecting vulnerabilities, but the evaluation of their usability is a commonly neglected topic. Usability of automated security tools is particularly crucial when dealing with problems of cryptographic protocols for which even small—apparently insignificant—changes in their configuration can result in vulnerabilities that, if exploited, pave the way to attacks with dramatic consequences for the confidentiality and integrity of exchanged messages. This becomes even more acute when considering such ubiquitous protocols as the one for Transport Layer Security (TLS for short). In this paper, we present the design and the lessons learned of a user study, meant to compare two different approaches when reporting misconfigurations. Results reveal that including contextualized actionable mitigations in security reports significantly impact the accuracy and the time needed to patch TLS vulnerabilities. Along with the lessons learned, we share the experimental material that can be used during cybersecurity labs to let students configure and patch TLS first-hand.

The Internet of Things is a widely adopted and pervasive technology, but also one of the most conveniently attacked given the volume of shared data and the availability of affordable but insecure products. This paper investigates two classes of denial of service (DoS) attacks that target the handling of message queues in MQTT, one of the most broadly used IoT protocols. The first attack attempts to saturate the MQTT broker resources, while the second exploits the broker to perform an amplification attack against the connected clients. We demonstrate the effectiveness of the attacks and indicate the parameters that would hinder the capabilities of a DoS attacker in three open-source MQTT implementations: Mosquitto, VerneMQ and EMQ X. To improve the security awareness in MQTT-based deployments, we integrate the attacks and mitigations in MQTTSA, a tool that detects MQTT misconfigurations and provides security-oriented recommendations and configuration snippets.

With more systems becoming digitised, enterprises are adopting cloud technologies and outsourcing non-critical services to reduce the pressure on IT departments. In this process, it is crucial to achieving the right balance between costs, usability and security; prioritising security over the rest when handling sensitive data. Considering the print management, often off-premise, many enterprises report at least one print-related security incident that led to data loss in the past year. This problem can damage the enterprise business, especially considering the fines prescribed by current regulations or its reputation. Focusing on securing enterprise printing, pull printing is the set of technologies and processes that allow the release of print jobs according to specific conditions; typically user authentication and proximity to a printer. We design a software-oriented pull printing infrastructure that supports a print release mechanism using QR codes and electronic IDentity cards as a second-factor authenticator. Our solution addresses the costs, as any medium-size organisation can adopt our open-source solution without additional devices or access badges; and the user experience, as we offer a driverless print environment and a user-friendly mobile application.

While organisations move their infrastructure to the cloud, honest but curious Cloud Service Providers (CSPs) threaten the confidentiality of cloud-hosted data. In this context, many researchers proposed Cryptographic Access Control (CAC) schemes to support data sharing among users while preventing CSPs from accessing sensitive data. However, the majority of these schemes focuses on high-level features only and cannot adapt to the multiple requirements arising in different scenarios. Moreover, (almost) no CAC scheme implementation is available for enforcement of authorisation policies in the cloud, and performance evaluation is often overlooked. To fill this gap, we propose the toolchain COERCIVE, short for CryptOgraphy killEd (the honest but) cuRious Cloud servIce proVidEr, which is composed of two tools: TradeOffBoard and CryptoAC. TradeOffBoard assists organisations in identifying the optimal CAC architecture for their scenario. CryptoAC enforces authorisation policies in the cloud by deploying the architecture selected with TradeOffBoard. In this paper, we describe the implementation of CryptoAC and conduct a thorough performance evaluation to demonstrate its scalability and efficiency with synthetic benchmarks.

The General Data Protection Regulation requires, where possible, to seek data subjects perception. Studies showed that people do not have a correct privacy risk perception. In this paper, we study how lay people perceive privacy risks once they are made aware and if experts can differentiate between security and privacy risks.

More and more online services are characterised by the need for strongly verifying the real-world identity of end users, especially when sensitive operations have to be carried out: just imagine a fully-remote signature of a contract, and what could happen whether someone managed to perform it by using another person’s name. For this reason, the identity management lifecycle contains specific procedures – called enrollment or onboarding – providing a certain level of assurance on digital users’ real identities. These procedures must be as secure as possible to prevent frauds and identity thefts. In this paper, we present a framework composed of a specification language, a security analysis methodology and a risk analysis methodology for enrollment solutions. For concreteness, we apply our framework to a real use case (i.e., fully-remote solutions relying on electronic documents as identity evidence) in the context of a collaboration with an Italian FinTech startup. Beyond validating the framework, we analyse and highlight the essential role of mitigations on the overall security of enrollment procedures.

To facilitate the adoption of cloud by organizations, Cryptographic Access Control (CAC) is the obvious solution to control data sharing among users while preventing partially trusted Cloud Service Providers (CSP) from accessing sensitive data. Indeed, several CAC schemes have been proposed in the literature. Despite their differences, available solutions are based on a common set of entities---e.g., a data storage service or a proxy mediating the access of users to encrypted data---that operate in different (security) domains---e.g., on-premise or the CSP. However, the majority of the CAC schemes assume a fixed assignment of entities to domains; this has security and usability implications that are not made explicit and can make inappropriate the use of a CAC scheme in certain scenarios with specific requirements. For instance, assuming that the proxy runs at the premises of the organization avoids the vendor lock-in effect but may substantially undermine scalability.

Everyday life is permeated by new technologies allowing people to perform almost any kind of operation from their smart devices. Although this is amazing from a convenience perspective, it may result in several security issues concerning the need for authenticating users in a proper and secure way. Electronic identity cards (also called eID cards) play a very important role in this regard, due to the high level of assurance they provide in identification and authentication processes. However, authentication solutions relying on them are still uncommon and suffer from many usability limitations. In this paper, we thus present the design and implementation of a novel passwordless, multi-factor authentication protocol based on eID cards. To reduce known usability issues while keeping a high level of security, our protocol leverages push notifications and mobile devices equipped with NFC, which can be used to interact with eID cards. In addition, we evaluate the security of the protocol through a formal security analysis and a risk analysis, whose results emphasize the acceptable level of security.

The CAP Theorem is used by distributed system practitioners to investigate the necessary trade-offs in the design and development of distributed systems, mainly databases and web applications. In this paper, we use it to reason about access control systems designed for the Internet of Things (IoT). We validate our approach by experimentally investigating alternative architectural designs to enforce access control in a smart lock system using the cloud-edge IoT platform offered by Amazon Web Services. We discuss the trade-off between security and performance that may help IoT designers choose the most suitable architecture supporting their requirements.

Remote attestation has emerged as a valuable security mechanism which aims to verify remotely whether or not a potentially untrusted device has been compromised. The protocols of Remote attestation are particularly important for securing Internet of Things (IoT) systems which, due to the large number of interconnected devices and limited security protections, are susceptible to a wide variety of cyber attacks. To guarantee the integrity of a software running on a single device, remote attestation is usually executed as an uninterrupted procedure: at the attestation time, a device stops the normal operation and executes the attestation of the entire device without interruption. The remote attestation protocols that aim to attest a large number of devices also follow the assumption on uninterrupted execution: when a device attests its network neighbours, each device verified in the neighborhood suspends its normal operation until the attestation protocol is completed. To avoid unnecessary suspension of the normal operation of the devices, this paper proposes a novel Secure Asynchronous Remote Attestation (SARA) protocol that releases the constraint of synchronous interaction among devices. In particular, SARA is an attestation protocol that exploits asynchronous communication capabilities among IoT devices in order to attest a distributed IoT service executed by them. SARA verifies both that each IoT device is not compromised (device trustworthiness), and that the exchanged communication data have not maliciously influence the communicating devices (legitimate operations). By tracing the execution order of each service invocation of an asynchronous distributed service, SARA allows each service to collect accurately historical data of its interactions, and transmits asynchronously such historical data to other interacting services. We have implemented and validated SARA through a realistic simulation on the Contiki emulator that demonstrates the functionality and efficiency of our protocol. The results confirm the suitability of SARA for low-end devices.

Over the last few years, there has been an almost exponential increase in the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication factors of different categories are required instead. Even if several solutions are currently used, their security analyses have been performed informally or semiformally at best, and without a reference model and a precise definition of the multi-factor authentication property. This makes a comparison among the different solutions both complex and potentially misleading. In this article, we first present the design of two reference models for native applications based on the requirements of two real-world use-case scenarios. Common features between them are the use of one-time password approaches and the support of a single sign-on experience. Then, we provide a formal specification of our threat model and the security goals, and discuss the automated security analysis that we performed. Our formal analysis validates the security goals of the two reference models we propose and provides an important building block for the formal analysis of different multi-factor authentication solutions.

Cyber security incidents can have dramatic economic, social and institutional impact. The task of providing an adequate cyber-security posture to companies and organisations is far far from trivial and need the collection of information about threats from a wide range of sources. One such a source is history in the form of datasets containing information about past cyber-security incidents including date, size, type of attacks, and industry sector. Unfortunately, there are few publicly available datasets of this kind that are of good quality. The paper reports our initial efforts in building a large datasets of cyber-security incidents that contains around 14,000 entries by merging a collection of four publicly available datasets of different size and provenance. We also perform an analysis of the combined dataset, discuss our findings, and discuss the limitations of the proposed approach.

The Internet of Things (IoT) is radically changing the way people live and interact with society: ranging from wearables to smart cities, the number of IoT devices has grown exponentially. The Message Queuing Telemetry Transport (MQTT) protocol is one of the most widely used IoT communication protocols. However, our investigation over publicly available MQTT endpoints confirms an alarming trend, i.e. many do not provide adequate security measures and often rely on the insecure default configuration. To improve the security awareness on the use of MQTT the paper presents MQTT Security Assistant (MQTTSA), a tool that automatically detects misconfigurations in MQTT-based IoT deployments. To assist IoT system developers, MQTTSA produces a report outlining detected vulnerabilities, together with (high level) hints and code snippets to implement adequate mitigations. The effectiveness of the tool is assessed by a thorough experimental evaluation.

The Internet of Things (IoT) is receiving considerable attention from both industry and academia because of the new business models that it enables and the new security and privacy challenges that it generates. Major Cloud Service Providers (CSPs) have proposed platforms to support IoT by combining cloud and edge computing. However, the security mechanisms available in the cloud have been extended to IoT with some shortcomings with respect to the management and enforcement of access control policies. Access Control as a Service (ACaaS) is emerging as a solution to overcome these difficulties. The paper proposes a lazy approach to ACaaS that allows the specification and management of policies independently of the CSP while leveraging its enforcement mechanisms. We demonstrate the approach by investigating (also experimentally) alternative deployments in the IoT platform offered by Amazon Web Services on a realistic smart lock solution.

Security-sensitive workflows impose constraints on the controlflow and authorization policies that may lead to unsatisfiable instances. In these cases, it is still possible to find "least bad" executions where costs associated to authorization violations are minimized, solving the so-called Multi-Objective Workflow Satisfiability Problem (MO-WSP). The MO-WSP is inspired by the Valued WSP and its generalization, the Bi-Objective WSP, but our work considers quantitative solutions to the WSP without abstracting control-flow constraints. In this paper, we define variations of the MO-WSP and solve them using bounded model checking and optimization modulo theories solving. We validate our solutions on real-world workflows and show their scalability on synthetic instances.

Due to recent notorious security threats, like Mirai-botnet, it is challenging to perform efficient data communication and routing in low power and lossy networks (LLNs) such as Internet of Things (IoT), in which huge data collection and processing are predictable. The Routing Protocol for low power and Lossy networks (RPL) is recently standardized as a routing protocol for LLNs. However, the lack of scalability and the vulnerabilities towards various security threats still pose a significant challenge in the broader adoption of RPL in LLNs.To address these challenges, we propose SPLIT, a secure and scalable RPL routing protocol for IoT networks. SPLIT effectively uses a lightweight remote attestation technique to ensure software integrity of network nodes. To avoid additional overhead caused by attestation messages, SPLIT piggybacks attestation process on the RPL's control messages. Thus, SPLIT enjoys the low energy consumption and scalability features of RPL protocol, which are essential in resource-constrained large scale networks such as IoT. The simulation results for different IoT scenarios show the effectiveness of SPLIT compared to the state-of-the-art in presence of different types of attacks, concerning metrics such as packet delivery ratio and energy consumption.

Temporal role-based access control models support the specification and enforcement of several temporal constraints on role enabling, role activation, and temporal role hierarchies among others. In this paper, we define three mappings that preserve the solutions to a class of policy problems: they map security analysis problems in presence of static temporal role hierarchies to problems without them. We show how our mappings can be used to extend the capabilities of a tool for the analysis of administrative temporal role-based access control policies to reason in presence of temporal role hierarchies. We carried out an experimental evaluation with a prototype implementation, which highlighted that one of the proposed mappings behaves better than the other two. To the best of our knowledge, ours is the first tool capable of reasoning with (static) temporal role hierarchies.

Organizations often expose business processes and services as web applications. Improper enforcement of security policies in these applications leads to business logic vulnerabilities that are hard to find and may have dramatic security implications. Aegis is a tool to automatically synthesize run-time monitors to enforce control-flow and data-flow integrity, as well as authorization policies and constraints in web applications. The enforcement of these properties can mitigate attacks, e.g., authorization bypass and workflow violations, while allowing regulatory compliance in the form of, e.g., Separation of Duty. Aegis is capable of guaranteeing business continuity while enforcing the security policies. We evaluate Aegis on a set of real-world applications, assessing the enforcement of policies, mitigation of vulnerabilities, and performance overhead.

Nowadays, most of business practices involve personal data-processing of customers and employees. This is strictly regulated by legislation to protect the rights of the data subject. Enforcing regulation into enterprise information system is a non-trivial task that requires an interdisciplinary approach. This paper presents a declarative framework to support the specification of information system designs, purpose-aware access control policies, and the legal requirements derived from the European Data Protection Directive. This allows for compliance checking via a reduction to policy refinement that is supported by available automated tools. We briefly discuss the results of the compliance analysis with a prototype tool on a simple but realistic scenario about the processing of personal data to produce salary slips of employees in an Italian organization.

Remote Attestation (RA) has been proven to be a powerful security service to check the legitimacy of the software configuration (e.g., running software and data) of devices. In recent years, advances in trusted computing, made possible to extend the use of RA also to embedded and Internet of Things (IoT) devices. The massive scale of IoT deployments poses scalability challenges to RA. Recently, researchers proposed efficient protocols for collective network attestation, i.e., efficient attestation of a whole network of interconnected embedded devices; however, most of these solutions are either costly, or simply unsuitable for highly dynamic networks.

We introduce a new class of analysis problems, called Scenario Finding Problems (SFPs), for security-sensitive business processes that – besides execution constraints on tasks – define access control policies (constraining which users can execute which tasks) and authorization constraints (such as Separation of Duty). The solutions to SFPs are concrete execution scenarios that assist customers in the reuse and deployment of security-sensitive workflows. We study the relationship of SFPs to well-known properties of security-sensitive processes such as Workflow Satisfiability and Resiliency together with their complexity. Finally, we present a symbolic approach to solving SFPs and describe our experience with a prototype implementation on real-world business process models taken from an on-line library.

Modularity is an important concept in the design and enactment of workflows. However, supporting the specification and enforcement of authorization in this setting is not straightforward. In this paper, we introduce a notion of component and a combination mechanism for 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 (specifying which users can execute which tasks). We show how authorization constraints can also be imposed across components and 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 reuse of workflows and related run-time monitors inside an editor for security-sensitive workflows.

While there exist many secure authentication and authorization solutions for web applications, their adaptation in the mobile context is a new and open challenge. In this paper, we argue that the lack of a proper reference model for Single Sign-On (SSO) for mobile native applications drives many social network vendors (acting as Identity Providers) to develop their own mobile solution. However, as the implementation details are not well documented, it is difficult to establish the proper security level of these solutions. We thus provide a rational reconstruction of the Facebook SSO flow, including a comparison with the OAuth 2.0 standard and a security analysis obtained testing the Facebook SSO reconstruction against a set of identified SSO attacks. Based on this analysis, we have modified and generalized the Facebook solution proposing a native SSO solution capable of solving the identified vulnerabilities and accommodating any Identity Provider.

Run-time monitors are crucial to the development of security-aware workflow management systems, which need to mediate access to their resources by enforcing authorization policies and constraints, such as Separation of Duty. In this paper, we introduce a precise technique to synthesize run-time monitors capable of ensuring the successful termination of workflows while enforcing authorization policies and constraints. An extensive experimental evaluation shows the scalability of our technique on the important class of hierarchically specified security-sensitive workflows with several hundreds of tasks.

NATO is developing a new IT infrastructure for automated information sharing between different information security domains and supporting dynamic and flexible enforcement of the need-to-know principle. In this context, the Content-based Protection and Release (CPR) model has been introduced to support the specification and enforcement of NATO access control policies. While the ability to define fine-grained security policies for a large variety of users, resources, and devices is desirable, their definition, maintenance, and enforcement can be difficult, time-consuming, and error prone. In this paper, we give an overview of a tool capable of assisting NATO security personnel in these tasks by automatically solving several policy analysis problems of practical interest. The tool levarages state-of-the-art SMT solvers.

Access control is a crucial issue for the security of Web Services. Since these are independently designed, implemented, and managed, each with its own access control policy, it is challenging to mediate the access to the information they share. In this context, a particularly difficult case occurs when a service invokes another service to satisfy an initial request, leading to indirect authorization errors. To overcome this problem, we propose a new approach based on a version of ORganization Based Access Control (OrBAC) extended by a delegation graph to keep track of transitive authorization dependencies. We show that Datalog can be used as the specification language of our model. As a byproduct of this, an automated analysis technique for simulating execution scenarios before deployment is proposed. Finally, we show how to implement an enforcement mechanism for our model on top of the XACML architecture. To validate our approach, we present a case study adapted from the literature.

The widespread adoption of Application Programming Interfaces (APIs) by enterprises is changing the way business is done by permitting the implementation of a multitude of apps, customized to user needs. While supporting a more flexible exploitation of available data, services and applications developed on top of APIs are vulnerable to a variety of attacks, ranging from SQL injection to unauthorized access of sensitive data. Available security solutions must be re-used and/or adapted to work with APIs. In this paper, we focus on the development of a flexible access control mechanism for APIs. This is an important security mechanism to guarantee the enforcement of authorization constraints on resources while invoking their API functions. We have developed an extension of the Spring Security framework, the standard for securing services and apps built in the popular (open source) Spring framework, for the specification and enforcement of Attribute-Based Access Control (ABAC) policies. We demonstrate our work with scenarios arising in a smart energy eco-system.

Extensions of Role-Based Access Control (RBAC) policies taking into account contextual information (such as time and space) are increasingly being adopted in real-world applications. Their administration is complex since they must satisfy rapidly evolving needs. For this reason, automated techniques to identify unsafe sequences of administrative actions (i.e. actions generating policies by which a user can acquire permissions that may compromise some security goals) are fundamental tools in the administrator's tool-kit. In this paper, we propose a precise and scalable automated analysis technique for the safety of administrative temporal RBAC policies. Our approach is to translate safety problems for this kind of policy to (decidable) reachability problems of a certain class of symbolic transition systems. The correctness of the translation allows us to design a precise analysis technique for the safety of administrative RBAC policies with a finite but unknown number of users. For scalability, we present a heuristics that allows us to reduce the set of administrative actions without losing the precision of the analysis. An extensive experimental analysis confirms the scalability and precision of the approach also in comparison with a recent analysis technique developed for the same class of temporal RBAC policies.

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 reuse 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 and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation.

The successful operation of NATO missions requires effective and secure sharing of information among coalition partners and external organizations, while avoiding the disclosure of sensitive information to untrusted users. To resolve the conflict between confidentiality and availability, NATO is developing a new information sharing infrastructure, called Content-based Protection and Release. We describe the architecture of access control in NATO operations, which is designed to be easily built on top of available (service-oriented) infrastructures for identity and access control management. We then present a use case scenario drawn from the NATO Passive Missile Defence system for simulating the consequences of intercepting missile attacks. In the system demonstration, we show how maps annotated with the findings of the system are filtered by the access control module to produce appropriate views for users with different clearances and terminals under given release and protection policies.

The User Authorization Query (UAQ) Problem for Role- Based Access Control (RBAC) amounts to determining a set of roles to be activated in a given session in order to achieve some permissions while satisfying a collection of authorization constraints governing the activation of roles. Techniques ranging from greedy algorithms to reduction to (variants of) the propositional satisfiability (SAT) problem have been used to tackle the UAQ problem. Unfortunately, available techniques su er two major limitations that seem to question their practical usability. On the one hand, authorization constraints over multiple sessions or histories are not considered. On the other hand, the experimental evaluations of the various techniques are not satisfactory since they do not seem to scale to larger RBAC policies.

Administrative Role Based Access Control (ARBAC) is one of the most widespread framework for the management of access-control policies. Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One of the main limitation of availab le analysis techniques is that the set of users is bounded. In this paper, we propose a symbolic framework to overcome this limitation. We design an automated analysis technique that can handle both a bounded and an unbounded number of users by adapting recent methods for the symbolic model checking of infinite state systems that use first-order logic and SMT solving techniques. An extensive experimental evaluation confirms the scalability of the proposed technique.

Automated techniques for the security analysis of Role-Based Access Control (RBAC) access control policies are crucial for their design and maintenance. The definition of administrative domains by means of attributes attached to users makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains. In this paper, we describe an automated symbolic security analysis technique for administrative attribute-based RBAC policies. A class of formulae of first-order logic is used as an adequate symbolic representation for the policies and their administrative actions. State-of-the-art automated theorem proving techniques are used (off-the-shelf) to mechanize the security analysis procedure. Besides discussing the assumptions for the effectiveness and termination of the procedure, we demonstrate its efficiency through an extensive empirical evaluation.

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, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. 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 theory of arrays.

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 combination 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.

The key to many approaches to reason about pointerbased data structures is the availability of a decision procedure to automatically discharge proof obligations in a theory encompassing data, pointers, and the reachability relation induced by pointers. So far, only approximate solutions have been proposed which abstract either the data or the reachability component. Indeed, such approximations cause a lack of precision in the verification techniques where the decision procedures are exploited. In this paper, we consider the pointer-based data structure of singly-linked lists and define a Theory of Linked Lists (TLL). The theory is expressive since it is capable of precisely expressing both data and reachability constraints, while ensuring decidability. Furthermore, its decidability problem is NP-complete. We also design a practical decision procedure for TLL which can be combined with a wide range of available decision procedures for theories in firstorder logic.

Software bugs are very difficult to detect even in small units of code. Several techniques to debug or prove correct such units are based on the generation of a set of formulae whose unsatisfiability reveals the presence of an error. These techniques assume the availability of a theorem prover capable of automatically discharging the resulting proof obligations. Building such a tool is a difficult, long, and error-prone activity. In this paper, we describe techniques to build provers which are highly automatic and flexible by combining state-of-the-art superposition theorem provers and BDDs. We report experimental results on formulae extracted from the debugging of C functions manipulating pointers showing that an implementation of our techniques can discharge proof obligations which cannot be handled by Simplify (the theorem prover used in the ESC/Java tool) and perform much better on others.