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.

• csl-91-4.dvi
• csl-91-4.ps