SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Mechanical Verification of a Schematic Protocol for Byzantine Fault Tolerant Clock Synchronization
 by Dr. Natarajan Shankar.

Abstract
Schneider [1] generalizes a number of protocols for Byzantine fault tolerant clock synchronization and presents a uniform proof for their correctness. We present a machine checked proof of this schematic protocol that revises some of the details in Schneider's original analysis. The verification was carried out with the EHDM system [2] developed at the SRI Computer Science Lab oratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm [3] satisfies the requirements of Schneider's protocol.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy