Policies for Fair Exchanges of Resources

TL;DR

This paper introduces a formal framework for ensuring fair resource exchanges on digital platforms using a new policy language and logic, with applications demonstrated on blockchain-based NFT exchanges.

Contribution

It presents MuAC, a declarative policy language with formal semantics, and MuACL, a logic for verifying exchange fairness, including a proof of its decidability and a blockchain implementation.

Findings

MuACL logic is decidable for fairness verification.

A semantics-preserving compilation from MuAC to MuACL is established.

Application demonstrated on blockchain for NFT exchanges.

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.