Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly executed by the named parties. For example, for issuing a Visa, an applicant demonstrates, among other evidence, that he has sufficient financial means to visit a foreign country. The form of evidence in ETs has traditionally been unstructured and informal, in the form of paper-based evidence. This paper proposes a formal treatment of evidence based on proof theory. In particular, we investigate the proof theory of Cyberlogic, an assertion logic for ETs, that enables the combination of evidence represented as logical derivations and as digital certificates, i.e., electronic evidence signed by a principal’s secret key. We propose a proof system for Cyberlogic, refining it with further constructions that support a wider range of ETs. We prove that the proof system admits cut-elimination.
Moreover, we propose a sound and complete focused proof system for the refinement of Cyberlogic thus enabling efficient proof-search. Furthermore, we identify a fragment of Cyberlogic, called Cyberlogic Programs, that can be used to efficiently program ETs using a variety of FOL engines. Finally, we propose Proof Certificate format for Cyberlogic Programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.
This is joint work with Giselle Reis, Harald Ruess, Dian Balta, Tewodros Beyene, and Natarajan Shankar.
