Abstract
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. © Springer-Verlag Berlin Heidelberg 2005.
Author supplied keywords
Cite
CITATION STYLE
Ogawa, M., Horita, E., & Ono, S. (2005). Proving properties of incremental Merkle trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3632 LNAI, pp. 424–440). Springer Verlag. https://doi.org/10.1007/11532231_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
