Evidential Transactions with Cyberlogic
- URL: http://arxiv.org/abs/2304.00060v1
- Date: Mon, 20 Mar 2023 10:18:43 GMT
- Title: Evidential Transactions with Cyberlogic
- Authors: Harald Ruess and Natarajan Shankar
- Abstract summary: Cyberlogic is an enabling logical foundation for building and analyzing digital transactions.
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.
- Score: 0.6091702876917281
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
Related papers
- On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials [39.4080639822574]
Verifiable credentials are a digital analogue of physical credentials.
They can be presented to verifiers to reveal attributes or even predicates about the attributes included in the credential.
One way to preserve privacy during presentation consists in selectively disclosing the attributes in a credential.
arXiv Detail & Related papers (2024-01-16T08:22:28Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
This approach allows for the computer-assisted analysis of abstract dialectical frameworks.
Exemplary applications include the formal analysis and verification of meta-theoretical properties.
arXiv Detail & Related papers (2023-12-08T09:32:26Z) - LpiCT: A logic security analysis framework for protocols [1.4852249222037588]
This paper introduces logic rules and proofs, binary tree and the KMP algorithm, and proposes a new extension the pi calculus theory, a logic security analysis framework and an algorithm.
Empirical results show that the new extension theory, the logic security analysis framework and the algorithm can effectively analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol.
arXiv Detail & Related papers (2023-11-01T12:06:47Z) - Logic-induced Diagnostic Reasoning for Semi-supervised Semantic
Segmentation [85.12429517510311]
LogicDiag is a neural-logic semi-supervised learning framework for semantic segmentation.
Our key insight is that conflicts within pseudo labels, identified through symbolic knowledge, can serve as strong yet commonly ignored learning signals.
We showcase the practical application of LogicDiag in the data-hungry segmentation scenario, where we formalize the structured abstraction of semantic concepts as a set of logic rules.
arXiv Detail & Related papers (2023-08-24T06:50:07Z) - CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic.
Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations.
On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
arXiv Detail & Related papers (2023-05-20T11:26:51Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
Passage-level logical relations represent entailment or contradiction between propositional units (e.g., a concluding sentence)
We propose logic structural-constraint modeling to solve the logical reasoning QA and introduce discourse-aware graph networks (DAGNs)
The networks first construct logic graphs leveraging in-line discourse connectives and generic logic theories, then learn logic representations by end-to-end evolving the logic relations with an edge-reasoning mechanism and updating the graph features.
arXiv Detail & Related papers (2022-07-04T14:38:49Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic.
This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
arXiv Detail & Related papers (2021-10-18T10:45:59Z) - Logical Credal Networks [87.25387518070411]
This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability.
We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
arXiv Detail & Related papers (2021-09-25T00:00:47Z) - Logic-Driven Context Extension and Data Augmentation for Logical
Reasoning of Text [65.24325614642223]
We propose to understand logical symbols and expressions in the text to arrive at the answer.
Based on such logical information, we put forward a context extension framework and a data augmentation algorithm.
Our method achieves the state-of-the-art performance, and both logic-driven context extension framework and data augmentation algorithm can help improve the accuracy.
arXiv Detail & Related papers (2021-05-08T10:09:36Z) - Modelling Value-oriented Legal Reasoning in LogiKEy [0.0]
We show how LogiKEy can harness interactive and automated theorem proving technology to provide a testbed for the development and formal verification of legal domain-specific languages and theories.
We establish novel bridges between latest research in knowledge representation and reasoning in non-classical logics, automated theorem proving, and applications in legal reasoning.
arXiv Detail & Related papers (2020-06-23T06:57:15Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.