Policies for Fair Exchanges of Resources
Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta, Luca Viganò
TL;DR
The paper addresses the problem of fair exchanges of digital resources on platforms where each participant specifies exchange policies. It introduces MuAC, a declarative policy language, and MuACL, a decidable logic that combines linear and non-linear reasoning with a linear contractual implication to capture circular promises. A correctness bridge is built by compiling MuAC policies into MuACL formulas, proving that exchange fairness reduces to MuACL provability and witness generation, amenable to a blockchain based NFT exchange with a TTP role implemented by a smart contract. The work demonstrates a rigorous, verifiable foundation for fair exchanges, enabling off chain proof generation with on chain verification, and points to practical deployment and future enhancements including richer policy features and time/value considerations.
Abstract
People increasingly use digital platforms to exchange resources in accordance with some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens.