Beschreibung
The central research question underlying this thesis is how to best provide information security for digital clock synchronization methods, most prominently authenticity and integrity protection of synchronization messages on whose basis devices would adjust their clocks. The problem is especially challenging because the "best" way of providing security appears to involve balancing strength of security guarantees versus achievable performance and strain of involved devices, in particular good scalability of the efforts demanded of time emitters with increasing numbers of receivers that have to be provided with synchronization data. This thesis makes a primary distinction between two-way and one-way techniques for clock synchronization, both because the optimal methods for adding security mechanisms change and because the achievable security guarantees of the resulting designs for two-way environments are much better than for one-way environments. The problem is then treated for those two cases separately, but with equal methods that include engineering our own designs, evaluating design candidates with model checking, testing implementations for their behavior in practice, and verifying the most promising ones with machine-assisted theorem proving. In creating our own designs, we nd that, regarding both two-way and one-way synchronization, the methodology for adding security is relatively mature. We further find that those methods commonly used for two-way synchronization are solid in that they provide good security guarantees at high synchronization performance with very benign scaling by number of receiver per emitter. This is both theoretically verified with automated tools and tested in practice. For one-way methods, on the other hand, we find that any mechanism is vulnerable to so-called delay attacks, and that for certain security mechanisms this vulnerability can cause critical failures. We follow up on this theoretical attack (that we discover ourselves for a particular use-case of ours, but that also appears in more general descriptions in the literature) with model checking and successfully realize a practical implementation of it in a testbed scenario. We further establish, however, that as long as participant clocks maintain at least a degree of rough synchronization, authenticity of messages is still guaranteed. After the separate treatment of two-way and one-way synchronization, we discuss possible uses of combinations of the two, as well as procedures to use the presented mechanisms to achieve provable synchronization and traceability. An overall take-home message of this thesis comprises four points: First, the problem of providing security for two-way clock synchronization is solved to a very high degree. Second, the same problem for one-way synchronization has a number of unsolved and potentially unsolvable issues remaining; these issues relate to the ultimate lack of reliability of one-way messages with regard to freshness. Third, the implications of this are significant in view of the widespread usage of oneway synchronization technologies, most prominently in satellite navigation systems such as GPS and Galileo. Fourth, combinations of one-way mechanisms with two-way control methods should be refined in order to mitigate the negative implications of the latter two points.
