{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:20:27Z","timestamp":1740097227026,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319271514"},{"type":"electronic","value":"9783319271521"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-27152-1_12","type":"book-chapter","created":{"date-parts":[[2015,12,8]],"date-time":"2015-12-08T23:55:10Z","timestamp":1449618910000},"page":"218-245","source":"Crossref","is-referenced-by-count":2,"title":["First Results of a Formal Analysis of the Network Time Security Specification"],"prefix":"10.1007","author":[{"given":"Kristof","family":"Teichel","sequence":"first","affiliation":[]},{"given":"Dieter","family":"Sibold","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74810-6_1","volume-title":"Foundations of Security Analysis and Design IV","author":"M Abadi","year":"2007","unstructured":"Abadi, M.: Security protocols: principles and calculi. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 4677, pp. 1\u201323. Springer, Heidelberg (2007)"},{"key":"12_CR2","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 104\u2013115. ACM, New York (2001). \n                      http:\/\/doi.acm.org\/10.1145\/360204.360213"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Archer, M.: Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In: Workshop on Issues in the Theory of Security, pp. 14\u201315 (2002)","DOI":"10.21236\/ADA464932"},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2019599.2019601","volume":"14","author":"D Basin","year":"2011","unstructured":"Basin, D., Capkun, S., Schaller, P., Schmidt, B.: Formal Reasoning About Physical Properties of Security Protocols. ACM Trans. Inf. Syst. Secur. 14(2), 16:1\u201316:28 (2011)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"12_CR6","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.88: automatic cryptographic protocol verifier, user manual and tutorial. Technical report, INRIA Paris-Rocquencourt, 08 2013"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). \n                      http:\/\/dblp.uni-trier.de\/db\/conf\/itp\/itp2010.html#BlanchetteN10"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"CJF Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414\u2013418. Springer, Heidelberg (2008). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-540-70545-1_38"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"NA Durgin","year":"2004","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2), 247\u2013311 (2004). \n                      http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs215","journal-title":"J. Comput. Secur."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Ganeriwal, S., P\u00f6pper, C., Capkun, S., Srivastava, M.B.: Secure time synchronization in sensor networks (E-SPS). In: Proceedings of 2005 ACM Workshop on Wireless Security (WiSe 2005), pp. 97\u2013106. ACM, Sept 2005","DOI":"10.1145\/1080793.1080809"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0040-1","volume":"3","author":"P Hopcroft","year":"2004","unstructured":"Hopcroft, P., Lowe, G.: Analysing a stream authentication protocol using model checking. Int. J. Inf. Secur. 3(1), 2\u201313 (2004)","journal-title":"Int. J. Inf. Secur."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Housley, R.: Cryptographic Message Syntax (CMS). RFC 5652, RFC Editor, September 2009. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc5652.txt","DOI":"10.17487\/rfc5652"},{"key":"12_CR14","unstructured":"IEEE: IEEE Standard for a Precision Clock Synchronization Protocol for Networked Measurement and Control Systems (2008). \n                      http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=4579757"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Krawczyk, H., Bellare, M., Canetti, R.: HMAC: Keyed-Hashing for Message Authentication. RFC 2104, RFC Editor, 02 1997. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc2104.txt","DOI":"10.17487\/rfc2104"},{"issue":"6","key":"12_CR16","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1088\/0026-1394\/45\/6\/S22","volume":"45","author":"J Levine","year":"2008","unstructured":"Levine, J.: A Review of Time and Frequency Transfer Methods. Metrologia 45(6), 162\u2013174 (2008)","journal-title":"Metrologia"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-319-11737-9_20","volume-title":"Formal Methods and Software Engineering","author":"L Li","year":"2014","unstructured":"Li, L., Sun, J., Liu, Y., Dong, J.S.: TAuth: verifying timed security protocols. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 300\u2013315. Springer, Heidelberg (2014). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-319-11737-9_20"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"12_CR19","unstructured":"Milius, S., Sibold, D., Teichel, K.: An Attack Possibility on Time Synchronization Protocols Secured with TESLA-Like Mechanisms, Draft version: \n                      https:\/\/www8.cs.fau.de\/staff\/milius\/AttackPossibilityTimeSyncTESLA.pdf"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Mills, D., Haberman, B.: Network Time Protocol Version 4: Autokey Specification. RFC 5906, RFC Editor, 06 2010. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc5906.txt","DOI":"10.17487\/rfc5906"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Mills, D., Martin, J., Burbank, J., Kasch, W.: Network Time Protocol Version 4: Protocol and Algorithms Specification. RFC 5905, RFC Editor, 06 2010. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc5905.txt","DOI":"10.17487\/rfc5905"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Mizrahi, T.: Security Requirements of Time Protocols in Packet Switched Networks. RFC 7384, RFC Editor, 10 2014. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc7384.txt","DOI":"10.17487\/rfc7384"},{"key":"12_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer, Heidelberg (2002)"},{"issue":"1\u20132","key":"12_CR24","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1\u20132), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Perrig, A., Song, D., Canetti, R., Tygar, J.D., Briscoe, B.: Timed Efficient Stream Loss-Tolerant Authentication (TESLA): Multicast Source Authentication Transform Introduction. RFC 4082, RFC Editor, 06 2005. \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc4082.txt","DOI":"10.17487\/rfc4082"},{"key":"12_CR26","unstructured":"R\u00f6ttger, S.: Analysis of the NTP Autokey Procedures, 2 2012. \n                      http:\/\/zero-entropy.de\/autokey_analysis.pdf"},{"key":"12_CR27","unstructured":"Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Chap. 6. IOS Press (2011). \n                      http:\/\/www.bensmyth.com\/files\/Smyth10-applied-pi-calculus.pdf"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-05119-2_8","volume-title":"Trustworthy Global Computing","author":"N Saeedloei","year":"2014","unstructured":"Saeedloei, N., Gupta, G.: Timed \n                      \n                        \n                      \n                      $$\\pi $$\n                      \n                        \n                          \u03c0\n                        \n                      \n                    -calculus. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 119\u2013135. Springer, Heidelberg (2014)"},{"key":"12_CR29","unstructured":"Sibold, D., Teichel, K., R\u00f6ttger, S.: Network time security. Technical report, IETF Secretariat, 07 2013. \n                      https:\/\/datatracker.ietf.org\/doc\/draft-ietf-ntp-network-time-security\/history\/"},{"key":"12_CR30","unstructured":"Sibold, D., Teichel, K., R\u00f6ttger, S., Housley, R.: Protecting network time security messages with the cryptographic message syntax (CMS). Technical report, IETF Secretariat, 10 2014. \n                      https:\/\/datatracker.ietf.org\/doc\/draft-ietf-ntp-cms-for-nts-message\/history\/"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Sun, K., Ning, P., Wang, C.: TinySeRSync: secure and resilient time synchronization in wireless sensor networks. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, pp. 264\u2013277. ACM, New York (2006)","DOI":"10.1145\/1180405.1180439"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Syverson, P., Meadows, C., Cervesato, I.: Dolev-yao is no better than machiavelli. In: Degano, P. (ed.) First Workshop on Issues in the Theory of Security \u2013 WITS 2000, pp. 87\u201392, Jul 2000. \n                      http:\/\/theory.stanford.edu\/~iliano\/papers\/wits00.ps.gz","DOI":"10.21236\/ADA464936"}],"container-title":["Lecture Notes in Computer Science","Security Standardisation Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27152-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T16:58:20Z","timestamp":1559321900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27152-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319271514","9783319271521"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27152-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}