{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T04:00:57Z","timestamp":1746504057917,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_20","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"300-315","source":"Crossref","is-referenced-by-count":4,"title":["TAuth: Verifying Timed Security Protocols"],"prefix":"10.1007","author":[{"given":"Li","family":"Li","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"TAuth tool and experiment models, http:\/\/www.comp.nus.edu.sg\/~li-li\/r\/tauth.html"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Software Eng.\u00a022(1), 6\u201315 (1996)","journal-title":"IEEE Trans. Software Eng."},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/BFb0015258","volume-title":"Computer Science Today","author":"R. Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Programming satan\u2019s computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 426\u2013440. Springer, Heidelberg (1995)"},{"issue":"2","key":"20_CR4","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/2019599.2019601","volume":"14","author":"D.A. Basin","year":"2011","unstructured":"Basin, D.A., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Secur.\u00a014(2), 16 (2011)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"20_CR5","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press (1957)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82\u201396. IEEE CS (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-48285-7_30","volume-title":"Advances in Cryptology - EUROCRYPT \u201993","author":"S. Brands","year":"1994","unstructured":"Brands, S., Chaum, D.: Distance bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol.\u00a0765, pp. 344\u2013359. Springer, Heidelberg (1994)"},{"issue":"1","key":"20_CR8","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst.\u00a08(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"2","key":"20_CR9","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/JSAC.2005.861380","volume":"24","author":"S. Capkun","year":"2006","unstructured":"Capkun, S., Hubaux, J.-P.: Secure positioning in wireless networks. IEEE Journal on Selected Areas in Communications\u00a024(2), 221\u2013232 (2006)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"20_CR10","unstructured":"CCITT. The directory authentication framework - Version 7, Draft Recommendation X.509 (1987)"},{"key":"20_CR11","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55\u201369. IEEE Computer Society (1999)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: FMSE, pp. 23\u201332. ACM (2004)","DOI":"10.1145\/1029133.1029137"},{"key":"20_CR13","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":"C.J.F. 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.\u00a05123, pp. 414\u2013418. Springer, Heidelberg (2008)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-24730-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2004","unstructured":"Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 342\u2013356. Springer, Heidelberg (2004)"},{"issue":"8","key":"20_CR15","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Commun. ACM\u00a024(8), 533\u2013536 (1981)","journal-title":"Commun. ACM"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/10722599_14","volume-title":"Computer Security - ESORICS 2000","author":"N. Evans","year":"2000","unstructured":"Evans, N., Schneider, S.: Analysing time dependent security properties in csp using pvs. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895, pp. 222\u2013237. Springer, Heidelberg (2000)"},{"key":"20_CR17","unstructured":"Francillon, A., Danev, B., Capkun, S.: Relay attacks on passive keyless entry and start systems in modern cars. In: NDSS. The Internet Society (2011)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-75698-9_5","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"G. Jakubowska","year":"2007","unstructured":"Jakubowska, G., Penczek, W.: Is your security protocol on time? In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol.\u00a04767, pp. 65\u201380. Springer, Heidelberg (2007)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Krawczyk, H.: Skeme: a versatile secure key exchange mechanism for internet. In: NDSS, pp. 114\u2013127. IEEE Computer Society (1996)","DOI":"10.1109\/NDSS.1996.492418"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters\u00a056, 131\u2013133 (1995)","journal-title":"Information Processing Letters"},{"key":"20_CR21","unstructured":"Lowe, G.: A family of attacks upon authentication protocols. Technical report, Department of Mathematics and Computer Science, University of Leicester (1997)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specification. In: CSFW, pp. 31\u201344. IEEE Computer Society (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"issue":"1-2","key":"20_CR23","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security\u00a06(1-2), 53\u201384 (1998)","journal-title":"Journal of Computer Security"},{"issue":"1","key":"20_CR24","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/JCS-1999-72-302","volume":"7","author":"G. Lowe","year":"1999","unstructured":"Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security\u00a07(1), 89\u2013146 (1999)","journal-title":"Journal of Computer Security"},{"key":"20_CR25","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.\u00a08044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"issue":"12","key":"20_CR26","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Rasmussen, K.B., Castelluccia, C., Heydt-Benjamin, T.S., Capkun, S.: Proximity-based access control for implantable medical devices. In: CCS, pp. 410\u2013419. ACM (2009)","DOI":"10.1145\/1653662.1653712"},{"issue":"1","key":"20_CR28","doi-asserted-by":"crossref","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"A.W. Roscoe","year":"1999","unstructured":"Roscoe, A.W., Broadfoot, P.J.: Proving security protocols with model checkers by data independence techniques. Journal of Computer Security\u00a07(1), 147\u2013190 (1999)","journal-title":"Journal of Computer Security"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Sastry, N., Shankar, U., Wagner, D.: Secure verification of location claims. In: Workshop on Wireless Security, pp. 1\u201310. ACM (2003)","DOI":"10.1145\/941312.941313"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Sedighpour, S., Capkun, S., Ganeriwal, S., Srivastava, M.B.: Implementation of attacks on ultrasonic ranging systems (demo). In: SenSys, p. 312. ACM (2005)","DOI":"10.1145\/1098918.1098977"},{"issue":"1-2","key":"20_CR31","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D.X. Song","year":"2001","unstructured":"Song, D.X., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security\u00a09(1-2), 47\u201374 (2001)","journal-title":"Journal of Computer Security"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:24:58Z","timestamp":1746419098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}