Proving Properties of Incremental Merkle Trees

DOI IR

Search this article

Description

This paper proves two basic properties of the model of a single attack point-free event ordering system, developed by NTT. This model is based on an incremental construction of Merkle trees, and we show the correctness of (1) completion and (2) an incremental sanity check. These are mainly proved using the theorem prover MONA; especially, this paper gives the first proof of the correctness of the incremental sanity check.

identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/5035

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top