Parallel Verification of Natural Deduction Proof Graphs
Authors:
James T. Oswald,
Brandon Rozek
Abstract:
Graph-based interactive theorem provers offer a visual representation of proofs, explicitly representing the dependencies and inferences between each of the proof steps in a graph or hypergraph format. The number and complexity of these dependency links can determine how long it takes to verify the validity of the entire proof. Towards this end, we present a set of parallel algorithms for the form…
▽ More
Graph-based interactive theorem provers offer a visual representation of proofs, explicitly representing the dependencies and inferences between each of the proof steps in a graph or hypergraph format. The number and complexity of these dependency links can determine how long it takes to verify the validity of the entire proof. Towards this end, we present a set of parallel algorithms for the formal verification of graph-based natural-deduction (ND) style proofs. We introduce a definition of layering that captures dependencies between the proof steps (nodes). Nodes in each layer can then be verified in parallel as long as prior layers have been verified. To evaluate the performance of our algorithms on proof graphs, we propose a framework for finding the performance bounds and patterns using directed acyclic network topologies (DANTs). This framework allows us to create concrete instances of DANTs for empirical evaluation of our algorithms. With this, we compare our set of parallel algorithms against a serial implementation with two experiments: one scaling both the problem size and the other scaling the number of threads. Our findings show that parallelization results in improved verification performance for certain DANT instances. We also show that our algorithms scale for certain DANT instances with respect to the number of threads.
△ Less
Submitted 17 November, 2023;
originally announced November 2023.
CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms
Authors:
Dalton Chichester,
Wei Du,
Raymond Kauffman,
Hai Lin,
Christopher Lynch,
Andrew M. Marshall,
Catherine A. Meadows,
Paliath Narendran,
Veena Ravishankar,
Luis Rovira,
Brandon Rozek
Abstract:
Recently, interest has been emerging in the application of symbolic techniques to the specification and analysis of cryptosystems. These techniques, when accompanied by suitable proofs of soundness/completeness, can be used both to identify insecure cryptosystems and prove sound ones secure. But although a number of such symbolic algorithms have been developed and implemented, they remain scattere…
▽ More
Recently, interest has been emerging in the application of symbolic techniques to the specification and analysis of cryptosystems. These techniques, when accompanied by suitable proofs of soundness/completeness, can be used both to identify insecure cryptosystems and prove sound ones secure. But although a number of such symbolic algorithms have been developed and implemented, they remain scattered throughout the literature. In this paper, we present a tool, CryptoSolve, which provides a common basis for specification and implementation of these algorithms, CryptoSolve includes libraries that provide the term algebras used to express symbolic cryptographic systems, as well as implementations of useful algorithms, such as unification and variant generation. In its current initial iteration, it features several algorithms for the generation and analysis of cryptographic modes of operation, which allow one to use block ciphers to encrypt messages more than one block long. The goal of our work is to continue expanding the tool in order to consider additional cryptosystems and security questions, as well as extend the symbolic libraries to increase their applicability.
△ Less
Submitted 21 September, 2022;
originally announced September 2022.
