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.

翻译：随着数字平台的日益普及，人们越来越多地依据特定策略进行资源交换，这些策略规定了用户提供何种资源以及要求何种回报。本文提出此类环境的形式化模型，重点关注用户策略的定义与执行机制，以确保恶意用户无法利用诚实用户。为此，我们引入声明式策略语言MuAC，并为其配备形式语义。为判定资源交换是否公平（即是否遵循现行MuAC策略），我们提出结合非线性、线性和契约性特征的非标准逻辑MuACL，并证明其可判定性。值得注意的是，MuACL的契约蕴涵算子无法在线性逻辑中表达。我们定义了将MuAC策略编译为MuACL的语义保持转换，从而将交换公平性问题归约为MuACL中的证明寻找问题。最后，我们演示了如何将本方法应用于区块链环境以实现非同质化代币的交换。