This paper proposes a dynamic, decentralized social trust model to meet Know Your Customer (KYC) and Anti-Money Laundering (AML) compliance requirements, especially for individuals lacking formal documentation. Building on previous work, we present a conceptual model for dynamically computing trust and risk values to support financial transaction approvals through innovative recognition schemes. Agent-based simulations across four scenarios demonstrate that dynamic trust mechanisms enhance transaction approval rates and payment volumes, provided malicious agents are controlled. The model is flexible, adaptable to diverse populations, and promotes financial inclusion without compromising compliance requirements. It also offers a foundation for future research on mitigating risks from malicious actors. Furthermore, it is particularly suited for enabling compliant and inclusive decentralized finance (DeFi) applications.

The majority of Internet of Things (IoT) devices available on the market nowadays present heterogeneity problems and security problems. These devices adopt different protocols to communicate among each other, hence the definition of a series of standards has been necessary to make their interaction possible. Moreover, certification processes have been proposed to analyse manufacturer’s products in search of every vulnerability and security threat which might affect firmware and final devices. However, none of these methodologies fully considers the effects which might occur when executing an IoT firmware. Therefore, to fill in this gap, we propose the behaviours assessment as a technique which allows a certifier to evaluate whether the effects of firmware operations are in accordance with some established policies. Starting from this model, we have created a library which performs the behaviours assessment using a safe and secure programming language called Rust. We have named this library manifest-producer. This library provides APIs to analyse ELF binaries, extract their functions, disassemble machine code, and build call trees to support behaviour evaluation using reverse engineering techniques in an automated way. To demonstrate its potential as an additional tool for IoT certification, we present a proof of concept showing how it helps to assess behaviours in a mock IoT firmware.

The theory of noninterference supports the analysis of information leakage and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back-and-forth computations, it is necessary to switch to a more expressive semantics, which has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the taxonomy of Focardi and Gorrieri based on weak bisimilarity.

Abstract Logical investigations of the notion of secrecy are typically concentrated on tools for deducing whether private information is well hidden from unauthorized, direct, or indirect access attempts. This paper proposes a multi-agent, normal multi-modal logic to capture salient features of secrecy’s intentions. Specifically, we focus on the intentions, beliefs and knowledge of secret keepers and, more generally, of all the actors involved in secret-keeping scenarios. In particular, we investigate intentions underlying the keeping of a true secret, namely a secret concerning information known (and so true) by the secret keeper. The resulting characterization of intending to keep a true secret provides valuable insights into conditions ensuring or undermining secrecy depending on agents’ attitudes and links between secrets and their surrounding context. We present the proposed logical system’s soundness, completeness and decidability results. Furthermore, we outline some theorems with potential applications to several fields, e.g. computer science and the social sciences.

Convolutional Neural Networks (CNNs) are artificial deep learning networks widely used in computer vision and image recognition for their highly efficient capability of extracting input image features. In the literature, such a successful tool has been leveraged for detection/classification purposes in several application domains where input data are converted into images. In this work, we consider the application of CNN models, developed by employing standard Python libraries, to detect and then classify Android-based malware applications. Different models are tested, even in combination with machine learning-based classifiers, with respect to two datasets of 5000 applications each. To emphasize the adequacy of the various CNN implementations, several performance metrics are considered, as also stressed by a comprehensive comparison with related work.

Trust is an extremely helpful construct when reasoning under uncertainty. Thus, being able to logically formalize the concept in a suitable language is important. However, doing so is problematic for three reasons. First, in order to keep track of the contextual nature of trust, situation trackers are required inside the language. Second, in order to produce trust estimations, agents rely on evidence personally gathered or reported by other agents; this requires elements in the language that can track which agents are used as referrals and how much weight is placed on their opinions. Finally, trust is subjective in nature, thus, personal thresholds are needed to track the trust-propensity of different evaluators. In this paper we propose an interpretation of a probabilistic modal language à la Hennessy-Milner in order to capture a context-aware quantitative notion of trust based on evidence. We also provide an axiomatization for the language and prove soundness, completeness, and decidability results.

Despite many efforts to increase access to financial services, 1,4 billion people still are unbanked. One significant barrier to decreasing this number is the lack of official personal documents (e.g., government-issued identification or utility bills) to comply with the necessary KYC/AML regulation. Innovative schemes can recognize one by using inputs like the personal trail generated when one uses the phone or engages in some digital activity. This paper proposes a formal language-based approach for modeling financial inclusion services and for representing in a structured way the existing KYC/AML compliance rules from different countries. Currently, those rules are written in an unstructured format using natural language and spread in regulatory documents from these jurisdictions. Our proposed language is a core building block of a computational trust and risk engine model, also discussed in this paper. Our approach supports the use of traditional and innovative recognition schemes, helping to overcome the barrier for those who cannot comply with conventional KYC/AML requirements. Moreover, it can also be used to power the risk calculation of computational trust and risk engines. Finally, the proposal is generic enough to be applied to both traditional and decentralized finance.

Abstract In recent years, one of the major issues concerning the study of online social network phenomena is related to the diffusion of misinformation, commonly known as fake news. In the literature, several mathematical tools are used to investigate both the identifying attributes of fake news and their spreading model. This work concentrates on the latter aspect and follows the lines of research inspired by the analysis of epidemic models. Its main contribution is the definition of a modeling framework based on process algebra for the explicit, formal representation of typical behavioral patterns of agents in social networks, and the use of a probabilistic verification framework based on modal logics and model checking for the quantitative analysis of the fake news spread.

Abstract In this work, we provide a logical characterization of trust, which is based on a modal logic expressing a computational notion of trust quantitatively dependent on the beliefs possessed by the agent. The proposed framework encompasses decidability results and equivalence laws emphasizing the properties of trust. The overall aim is to obtain a formal notion of trust that could be employed for further developments of formal languages related to decision-making procedures and soft-security mechanisms in online, digital environments. Such formal counterpart of trust should support agents, either human or artificial, in devising secure decision strategies based on partial and/or indirect information.

Computational trust is the digital counterpart of the human notion of trust as applied in social systems. Its main purpose is to improve the reliability of interactions in online communities and of knowledge transfer in information management systems. Trust models are formal frameworks in which the notion of computational trust is described rigorously and where its dynamics are explained precisely. In this paper we will consider and extend a computational trust model, i.e., JØsang's Subjective Logic: we will show how this model is well-suited to describe the dynamics of computational trust, but lacks effective tools to compute initial trust values to feed in the model. To overcome some of the issues with subjective logic, we will introduce a logical language which can be employed to describe and reason about trust. The core ideas behind the logical language will turn out to be useful in computing initial trust values to feed into subjective logic. The aim of the paper is, therefore, that of providing an improvement on subjective logic.

Purpose The Bring-Your-Own-Device (BYOD) paradigm favors the use of personal and public devices and communication means in corporate environments, thus representing a challenge for the traditional security and risk management systems. In this dynamic and heterogeneous setting, the purpose of this paper is to present a methodology called opportunity-enabled risk management (OPPRIM), which supports the decision-making process in access control to remote corporate assets. Design/methodology/approach OPPRIM relies on a logic-based risk policy model combining estimations of trust, threats and opportunities. Moreover, it is based on a mobile client – server architecture, where the OPPRIM application running on the user device interacts with the company IT security server to manage every access request to corporate assets. Findings As a mandatory requirement in the highly flexible BYOD setting, in the OPPRIM approach, mobile device security risks are identified automatically and dynamically depending on the specific environment in which the access request is issued and on the previous history of events. Originality/value The main novelty of the OPPRIM approach is the combined treatment of threats (resp., opportunities) and costs (resp., benefits) in a trust-based setting. The OPPRIM system is validated with respect to an economic perspective: cost-benefit sensitivity analysis is conducted through formal methods using the PRISM model checker and through agent-based simulations using the Anylogic framework.

Summary Repackaged applications are based on genuine applications, but they subtlety include some modifications. In particular, trojanized applications are one of the most dangerous threats for smartphones. Malware code may be hidden inside applications to access private data or to leak user credit. In this paper, we propose a contract‐based approach to detect such repackaged applications, where a contract specifies the set of legal actions that can be performed by an application. Current methods to generate contracts lack information from real usage scenarios, thus being inaccurate and too coarse‐grained. This may result either in generating too many false positives or in missing misbehaviors when verifying the compliance between the application and the contract. In the proposed framework, application contracts are generated dynamically by a central server merging execution traces collected and shared continuously by collaborative users executing the application. More precisely, quantitative information extracted from execution traces is used to define a contract describing the expected application behavior, which is deployed to the cooperating users. Then, every user can use the received contract to check whether the related application is either genuine or repackaged. Such a verification is based on an enforcement mechanism that monitors the application execution at run‐time and compares it against the contract through statistical tests. Copyright © 2014 John Wiley & Sons, Ltd.

Abstract Trust is a basic soft‐security condition influencing interactive and cooperative behaviors in online communities. Several systems and models have been proposed to enforce and investigate the role of trust in the process of favoring successful cooperations while minimizing selfishness and failure. However, the analysis of their effectiveness and efficiency is a challenging issue. This paper provides a formal approach to the design and verification of trust infrastructures used in the setting of software architectures and computer networks supporting online communities. The proposed framework encompasses a process calculus of concurrent systems, a temporal logic for trust, and model checking techniques. Both functional and quantitative aspects can be modeled and analyzed, while several types of trust models can be integrated. Copyright © 2015 John Wiley & Sons, Ltd.

Cooperation incentives are essential in user-centric networks to motivate users to share services and resources (including bandwidth, computational power, and storage space) and to avoid selfish nodes to hinder the functioning of the entire system. Virtual currency and reputation mechanisms are commonly adopted in online communities to boost participation, but their joint application has not been deeply explored, especially in the context of wireless communities, where not only the services, but even the enabling infrastructure is opportunistically built by community members. This paper investigates the combined use of virtual currency and reputation-based incentives in the specific context of a community of users with Wi-Fi enabled devices capable of establishing ad-hoc connections.

In this paper we provide an incremental methodology to assess the effect of the introduction of a dynamic power manager in a mobile embedded computing device. The methodology consists of two phases. In the first phase, we verify whether the introduction of the dynamic power manager alters the functionality of the system. We show that this can be accomplished by employing standard techniques based on equivalence checking for noninterference analysis. In the second phase, we quantify the effectiveness of the introduction of the dynamic power manager in terms of power consumption and overall system efficiency. This is carried out by enriching the functional model of the system with information about the performance aspects of the system, and by comparing the values of the power consumption and the overall system efficiency obtained from the solution of the performance model with and without dynamic power manager. To this purpose, first we employ a more abstract performance model based on the Markovian assumption, then we use a more realistic performance model - to be validated against the Markovian one - where general probability distributions are considered. The methodology is illustrated by means of its application to the study of a remote procedure call mechanism - through which a battery-powered device is used by some application requesting information - and of a streaming video service - which is accessed by a mobile client equipped with a power-manageable network interface card.

We define several security properties for the analysis of probabilistic noninterference as a conservative extension of a classical, nondeterministic, process-algebraic approach to information flow theory. We show that probabilistic covert channels (that are not observable in the nondeterministic setting) may be revealed through our approach and that probabilistic information can be exploited to give an estimate of the amount of confidential information flowing to unauthorized users. Finally, we present a case study showing that the expressiveness of the calculus we adopt makes it possible to model and analyze real concurrent systems.