# Evidential Transactions with Cyberlogic

arXiv: https://arxiv.org/abs/2304.00060 · HTML: https://mlsanity.com/paper/2304.00060/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 65 references that are in the map.
- First posted on arXiv 20 Mar 2023.

## Builds on (most cited first, 5 of 5)

- [Fast and Reliable Formal Verification of Smart Contracts with the Move Prover](https://mlsanity.com/paper/2110.08362/) (2021)
- [Towards an Accountable and Reproducible Federated Learning: A FactSheets Approach](https://mlsanity.com/paper/2202.12443/) (2022)
- [Systems Challenges for Trustworthy Embodied Systems](https://mlsanity.com/paper/2201.03413/) (2022)
- [The Curses of Blockchain Decentralization](https://mlsanity.com/paper/1810.02937/) (2018)
- [Pluralize: a Trustworthy Framework for High-Level Smart Contract-Draft](https://mlsanity.com/paper/1812.05444/) (2018)

## Abstract (arXiv)

Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are specified as distributed logic programs, and (3) verifiable evidence is collected by means of distributed proof search. Verifiable evidence, in particular, are constructed from extra-logical elements such as signed documents and cryptographic signatures. Despite this conceptual simplicity of Cyberlogic, central features of authorization policies including trust, delegation, and revocation of authority are definable. An expressive temporal-epistemic logic for specifying distributed authorization policies and protocols is therefore definable in Cyberlogic using a trusted time source. We describe the distributed execution of Cyberlogic programs based on the hereditary Harrop fragment in terms of distributed proof search, and we illustrate some fundamental issues in the distributed construction of certificates. The main principles of encoding and executing cryptographic protocols in Cyberlogic are demonstrated. Finally, a functional encryption scheme is proposed for checking certificates of evidential transactions when policies are kept private.