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.

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.

Collective adaptive systems (CAS) often adopt cooperative operating strategies to run distributed decision-making mechanisms. Sometimes, their effectiveness massively relies on the collaborative nature of individuals’ behavior. Stimulating cooperation while preventing selfish and malicious behaviors is the main objective of trust and reputation models. These models are largely used in distributed, peer-to-peer environments and, therefore, represent an ideal framework for improving the robustness, as well as security, of CAS. In this article, we propose a formal framework for modeling and verifying trusted CAS. From the modeling perspective, mobility, adaptiveness, and trust-based interaction represent the main ingredients used to define a flexible and easy-to-use paradigm. Concerning analysis, formal automated techniques based on equivalence and model checking support the prediction of the CAS behavior and the verification of the underlying trust and reputation models, with the specific aim of estimating robustness with respect to the typical attacks conducted against webs of trust.