Clock synchronization protocol, as an important component of the time-triggered networks, is the key to the instantaneity and certainty of the time-triggered networks. The modeling and verification of clock synchronization protocol were studied. The protocol′s behaviors were modeled by the extended labeled transition systems, and its correctness was verified by model checking technique. The verification results certified the correctness of this protocol even under different startup scenarios. Experimental results also show the effectiveness of extended labeled transition systems in protocol verification.