Matching Logic, Cryptography and Blockchains

August 2024 – December 2025
Research Partners:
Research Team:
ILDS Management Team:
Description:
Objective 1. Applicative matching logic and Lean

In a previous project, we implemented in Lean a formalization of Applicative Matching Logic (AML), including, among other things, definitions of the syntax, proof system, and a proof of the soundness theorem.

KORE is the intermediate representation language used by the 𝕂 Framework. As definitions written in KORE are descriptions of Matching Logic theories, it is crucial for these theories to be consistent.

Matching Logic Language (MLL) is a new format, currently under development, for representing Matching Logic theories and proofs. As the language is intended to be well suited for Zero-Knowledge verification, some design choices departing from a more traditional representation of proofs might be required (for example regarding the handling of metavariables, or of syntactical side-conditions in the proof system etc.). As such, it is important to be sure that all proofs representable in MLL are indeed valid AML proofs.

We propose the following sub-objectives:

O1.1. Verifying the consistency of KORE theories

The first sub-objective is to verify the consistency of KORE theories. Our main strategy is to use our existing Lean formalization of AML in order to show that models can be given for such theories. The existence of models, together with the formalized proof of soundness for AML, will imply that ⊥ cannot be proved from the theory.

Towards this end, using Lean, we will:

  • define the KORE language as an AML theory, using notations on top of our formalization. We will follow the Metamath implementation of KORE [5], and also define some of the specifications from [2];
  • use the above to syntactically prove lemmas about KORE in Lean;
  • implement a mechanism to automatically import KORE files into Lean;
  • construct models for the theories corresponding to KORE files, starting by formalizing the general semantics of KORE, then manually defining models for different KORE specifications, and, finally, investigating and implementing methods to automate the construction of models and for proving their correctness.

O1.2. Verifying the soundness of MLL

We will formalize in Lean:

  • the MLL format for representing theories and proofs;
  • the soundness of such proof system, relative to the standard AML semantics;
  • a translation between the MLL format and our existing formalized AML proof system.

Objective 2. Cryptography for blockchain implementation

Privacy and security play a crucial role in blockchain implementations. In particular, cryptographic primitives and techniques help achieve transaction validity, client anonymity, and smart contracts’ security, supporting fundamental properties of the blockchain, such as consensus and tamper resistance [6]. Cryptography is indispensable for blockchains; in fact, ENISA refers to blockchains as “cryptographic tools” [3]. However, cryptographic mechanisms might also lead to significant costs in computation and communication that affect the overall efficiency and, in the end, the system’s usability [4, 7]. In the last years, there has been an increasing interest in using Zero-Knowledge (ZK) proofs for blockchain, mostly non-interactive ZK with short proofs and efficient verification (SNARKs) [8]. A close study of the usage of cryptography in general (and ZK proofs in particular) might bring up ideas for better joint security and performance.

We will look into zk-Proofs obtained from mathematical proofs. More precise, the interest is on ZK implementations that can create a succinct proof [1] for the existence of a mathematical proof and allow fast verification. As a relatively novel concept of interest, the zero-knowledge Virtual Machine (zkVM) extends the idea of a zk-Proof to a virtual machine dedicated to execute smart contracts.

Specifically, we will:

  • study and understand the state-of-the-art ZK concepts and zkVMs implementations (such as Jolt, Risc zero, zkWASM, etc.);
  • identify specific properties of the current solutions that can be beneficial for the particular needs of the project;
  • investigate state-of-the-art and novel encoding mechanisms with specific properties, such as homomorphisms, that allow on-the-fly computation, leading to better performing proofs or verifications (optional, if time permits).

References:

[1] B. Bailey, X. Chen, A. Fiedler, H. Malvai, A. Miller, P. Mishra, N. Rodrigues, G. Roșu, Matching Logic Proofs Meet Succinct Cryptographic Proofs. Preprint, 2023.
[2] X. Chen, D. Lucanu, G. Roșu, Matching logic explained. Journal of Logical and Algebraic Methods in Programming 120, 100638, 2021.
[3] ENISA, Glossary – Blockchain.
[4] M. A. Ferrag, The performance evaluation of blockchain-based security and privacy systems for the Internet of Things: A tutorial. IEEE Internet of Things Journal 8, no. 24, 17236–17260, 2021.
[5] 𝕂 Team, Matching logic proof checker (github).
[6] NIST, NISTIR 8202 Blockchain Technology Overview.
[7] E. Raso, L. Bracciale, P. Gallo, G. Bernardinetti, G. Bianchi, E. R. Sanseverino, P. Loreti, Performance Evaluation of Cryptographic Schemes for Blockchain Security of Smart Grids. In: 2022 Workshop on Blockchain for Renewables Integration (BLORIN) (pp. 113–117), IEEE, 2022.
[8] X. Sun, F. R. Yu, P. Zhang, Z. Sun, W. Xie, X. Peng, A survey on Zero-Knowledge Proof in Blockchain. IEEE Network 35, no. 4, 198–205, 2021.