| Zugriffsnummer | 35002 |
| Dokumenttyp | Konferenzartikel |
| Peer Review | unbekannt |
| Sprache | Englisch |
| Titel | First results of a formal analysis of the NTS specification |
| Autor(in); Institution |
Teichel, Kristof; Q.4, Informationstechnologie, PTB-Braunschweig
Sibold, Dieter; Q.4, Informationstechnologie, PTB-Braunschweig
Milius, Stefan; Friedrich-Alexander Universität (FAU), Erlangen-Nürnberg, GERMANY
|
| Quelle/Jahr | Proceedings of the Security standardisation research:(2015), 30 S. |
| Schriftenreihe | Lecture notes in computer science: 9497 |
| ISBN | 978-3-319-27151-4 (print) ; 978-3-319-27152-1 (online) |
| DOI | |
| Verlag | Cham: Springer |
| Konferenzangaben | Security Standardization Research 2015 ; SSR 2015, Tokyo, 15-16, December, 2015, Japan |
| Freie Schlagworte | time synchronization ; security protocols ; formal verification ; model checking ; ProVerif |
| Zusammenfassung | This paper presents a first formal analysis of parts of a draft version of the Network Time Security specification. It presents the protocol model on which we based our analysis, discusses the decision for using the model checker ProVerif and describes how it is applied to analyze the protocol model. The analysis uncovers two possible attacks on the protocol. We present those attacks and show measures that can be taken in order to mitigate them and that have meanwhile been incorporated in the current draft specification. |
