Presentation 2004-12-17
Formal proof of correctness of scalable event-ordering system
Mizuhito OGAWA, Eiichi HORITA, Satoshi ONO,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) This paper proves two basic properties of the model of the single attack point-free event ordering system, developed by NTT. This model is based on an incremental construction of a Merkle tree, and we show correctness of (1) completion and (2) incremental sanity check. They are mainly proved under assistance of theorem prover MONA ; especially, this paper gives the first proof of correctness of incremental sanity check.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) Temporal authentication / theorem prover / event-ordering system
Paper # ISEC2004-105
Date of Issue

Conference Information
Committee ISEC
Conference Date 2004/12/10(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Information Security (ISEC)
Language ENG
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Formal proof of correctness of scalable event-ordering system
Sub Title (in English)
Keyword(1) Temporal authentication
Keyword(2) theorem prover
Keyword(3) event-ordering system
1st Author's Name Mizuhito OGAWA
1st Author's Affiliation Japan Advanced Institute of Science and Technology()
2nd Author's Name Eiichi HORITA
2nd Author's Affiliation NTT Information Sharing Platform Laboratories
3rd Author's Name Satoshi ONO
3rd Author's Affiliation NTT Information Sharing Platform Laboratories
Date 2004-12-17
Paper # ISEC2004-105
Volume (vol) vol.104
Number (no) 527
Page pp.pp.-
#Pages 10
Date of Issue