Model checking of robustness properties in trust and reputation systems

Abstract

Trust and reputation systems (TRSs) are used in cooperative environments where an agent needs to make a decision for requesting or performing a service. However, TRSs can be abused by malicious agents who do sequences of dishonest actions (attacks). Although there are proposals on verification of TRSs against attacks, they are not comprehensive enough to evaluate various Trust Computation Models (TCMs) and/or do not provide sufficient expressive power to specify different required robustness properties. In this paper, we introduce a comprehensive framework for specifying and verifying various robustness properties in TRSs through model checking approach. The proposed framework includes three main parts: (1) a logic for specification of robustness properties of TRSs named Probabilistic Action and Reward based Computation Tree Logic (PARCTL), (2) an enhanced version of our previously proposed model for specifying TRSs in hostile environments named Trust and Reputation Interaction Model (TRIM), and (3) the required algorithms for quantitative and probabilistic model checking of PARCTL properties over the specified model. The proposed framework has been implemented as a tool named TRIM-Checker. Our experimental results on robustness analysis of famous eBay, Beta, and CORE TCMs using TRIM-Checker are presented and their robustness against attacks is evaluated and compared together. © 2020 Elsevier B.V.