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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
MONA project, http://www.brics.dk/mona/
Adams, C., et al.: RFC3161, internet X.509 public key infrastructure time-stamp protocol (TSP). Technical report, IETF (2001)
Buldas, A., Lipmaa, H., Schoenmakers, B.: Optimally efficient accountable time-stamping. In: Imai, H., Zheng, Y. (eds.) PKC 2000. LNCS, vol. 1751, pp. 293–305. Springer, Heidelberg (2000)
Comon, H.: Sequentiality, monadic second-order logic and tree automata. Information and Computation 157(1 & 2), 25–51 (2000); Previously presented. In: Proc. 10th IEEE Symposium on Logic in Computer Science, pp. 508–517 (1995)
Horita, E., Ono, S., Ishimoto, H.: Implementation mechanisms of scalable event-ordering system without single point of attack. Technical report, IEICE SIG-ISEC, 11, (in Japanese) (2004)
Huet, G., Lévy, J.-J.: Computations in orthogonal rewriting systems I,II. In: Computational Logic: Essays in Honor of Alan Robinson, pp. 395–443. MIT Press, Cambridge (1991); Previous version: Report 359, INRIA, (1979)
Jakobsson, M., Leighton, F.T., Micali, S., Szydlo, M.: Fractal merkle tree representation and traversal. In: Joye, M. (ed.) CT-RSA 2003. LNCS, vol. 2612, pp. 314–326. Springer, Heidelberg (2003)
Merkle, R.C.: Secrecy, Authentication, and Public Key Systems. UMI Research Press, 1982. also appears as Ph.D thesis at Stanford University (1979)
Michael, S.: Merkle tree traversal in log space and time. In: Cachin, C., Camenisch, J.L. (eds.) EUROCRYPT 2004. LNCS, vol. 3027, pp. 541–554. Springer, Heidelberg (2004)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 4, vol. B, pp. 133–192. Elsevier, Amsterdam (1990)
Villemson, J.: Size-efficient interval time stamps. PhD thesis, University of Tartu, Estonia (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ogawa, M., Horita, E., Ono, S. (2005). Proving Properties of Incremental Merkle Trees. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_31
Download citation
DOI: https://doi.org/10.1007/11532231_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28005-7
Online ISBN: 978-3-540-31864-4
eBook Packages: Computer ScienceComputer Science (R0)