{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:30Z","timestamp":1762459710414},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030190514"},{"type":"electronic","value":"9783030190521"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-19052-1_8","type":"book-chapter","created":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T01:11:42Z","timestamp":1558573902000},"page":"89-111","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Timed Trace Equivalence"],"prefix":"10.1007","author":[{"given":"Vivek","family":"Nigam","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]},{"given":"Abra\u00e3o Aires","family":"Urquiza","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,28]]},"reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1016\/j.tcs.2003.12.023","volume":"322","author":"M Abadi","year":"2004","unstructured":"Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427\u2013476 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S095679689700261X","volume":"7","author":"G Agha","year":"1997","unstructured":"Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7, 1\u201372 (1997)","journal-title":"J. Funct. Program."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, 17\u201319 July 2010, pp. 107\u2013121 (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D., Sebastian M\u00f6dersheim, L.V.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. (2004). \n                    https:\/\/doi.org\/10.1007\/s10207-004-0055-7","DOI":"10.1007\/s10207-004-0055-7"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Computer Security \u2014 ESORICS 98","author":"G Bella","year":"1998","unstructured":"Bella, G., Paulson, L.C.: Kerberos version IV: inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361\u2013375. Springer, Heidelberg (1998). \n                    https:\/\/doi.org\/10.1007\/BFb0055875"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Benton, N., Hofmann, M., Nigam, V.: Effect-dependent transformations for concurrent programs. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 5\u20137 September 2016, Edinburgh, United Kingdom, pp. 188\u2013201 (2016)","DOI":"10.1145\/2967973.2968602"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Brands, S., Chaum, D.: Distance-bounding protocols (extended abstract). In: EUROCRYPT, pp. 344\u2013359 (1993)","DOI":"10.1007\/3-540-48285-7_30"},{"key":"8_CR9","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55\u201369 (1999)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-662-46666-7_15","volume-title":"Principles of Security and Trust","author":"V Cheval","year":"2015","unstructured":"Cheval, V., Cortier, V.: Timing attacks in security protocols: symbolic framework and proof techniques. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 280\u2013299. Springer, Heidelberg (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-662-46666-7_15"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-14577-3_5","volume-title":"Financial Cryptography and Data Security","author":"T Chothia","year":"2010","unstructured":"Chothia, T., Smirnov, V.: A traceability attack against e-passports. In: Sion, R. (ed.) FC 2010. LNCS, vol. 6052, pp. 20\u201334. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-14577-3_5"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, FMSE 2004, New York, NY, USA, pp. 23\u201332. ACM (2004)","DOI":"10.1145\/1029133.1029137"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, 8\u201310 July 2009, pp. 266\u2013276 (2009)","DOI":"10.1109\/CSF.2009.9"},{"issue":"2","key":"8_CR15","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"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-40229-1_13","volume-title":"Automated Reasoning","author":"F Dur\u00e1n","year":"2016","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Built-in variant generation and unification, and their applications in Maude 2.7. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 183\u2013192. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-40229-1_13"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9","volume-title":"Computer Aided Verification","year":"2014","unstructured":"Biere, A., Bloem, R. (eds.): CAV 2014. LNCS, vol. 8559. Springer, Cham (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-08867-9"},{"key":"8_CR18","unstructured":"Dutertre, B.: Solving exists\/forall problems with yices. In: SMT (2015)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"8_CR20","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. 1895, pp. 222\u2013237. Springer, Heidelberg (2000). \n                    https:\/\/doi.org\/10.1007\/10722599_14"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-66399-9_1","volume-title":"Computer Security \u2013 ESORICS 2017","author":"I Gazeau","year":"2017","unstructured":"Gazeau, I., Kremer, S.: Automated analysis of equivalence properties for security protocols using else branches. In: Foley, S.N., Gollmann, D., Snekkenes, E. (eds.) ESORICS 2017. LNCS, vol. 10493, pp. 1\u201320. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66399-9_1"},{"key":"8_CR22","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., Aparicio-S\u00e1nchez, D., Escobar, S., Meadows, C.A., Meseguer, J.: Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. In: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 400\u2013417 (2018)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., Santiago, S., Escobar, S., Meadows, C.A., Meseguer, J.: Analysis of the PKCS#11 API using the Maude-NPA tool. In: Proceedings of the Security Standardisation Research - Second International Conference, SSR 2015, Tokyo, Japan, 15\u201316 December 2015, pp. 86\u2013106 (2015)","DOI":"10.1007\/978-3-319-27152-1_5"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-36575-3_9","volume-title":"Programming Languages and Systems","author":"R Gorrieri","year":"2003","unstructured":"Gorrieri, R., Locatelli, E., Martinelli, F.: A simple language for real-time cryptographic protocol analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 114\u2013128. Springer, Heidelberg (2003). \n                    https:\/\/doi.org\/10.1007\/3-540-36575-3_9"},{"key":"8_CR25","series-title":"Foundations of Computing","volume-title":"Semantics of Programming Languages - Structures and Techniques","author":"CA Gunter","year":"1993","unstructured":"Gunter, C.A.: Semantics of Programming Languages - Structures and Techniques. Foundations of Computing. MIT Press, Cambridge (1993)"},{"key":"8_CR26","unstructured":"Ho, G., Boneh, D., Ballard, L., Provos, N.: Tick tock: building browser red pills from timing side channels. In: Bratus, S., Lindner, F.F.X. (eds.) 8th USENIX Workshop on Offensive Technologies, WOOT 2014 (2014)"},{"issue":"3\u20134","key":"8_CR27","first-page":"363","volume":"79","author":"G Jakubowska","year":"2007","unstructured":"Jakubowska, G., Penczek, W.: Modelling and checking timed authentication of security protocols. Fundam. Inf. 79(3\u20134), 363\u2013378 (2007)","journal-title":"Fundam. Inf."},{"key":"8_CR28","unstructured":"Kanovich, M.I., Kirigin, T.B., Nigam, V., Scedrov, A., Talcott, C.L.: Towards timed models for cyber-physical security protocols (2014). Available in Nigam\u2019s homepage"},{"key":"8_CR29","unstructured":"Kanovich, M.I., Kirigin, T.B., Nigam, V., Scedrov, A., Talcott, C.L., Perovic, R.: A rewriting framework for activities subject to regulations. In: 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Nagoya, Japan, 28 May\u20132 June 2012, pp. 305\u2013322 (2012)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Mason, I.A., Talcott, C.L.: IOP: The interoperability platform & IMaude: an interactive extension of Maude. In: Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004). Electronic Notes in Theoretical Computer Science. Elsevier (2004)","DOI":"10.1016\/j.entcs.2004.06.016"},{"issue":"2","key":"8_CR31","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113\u2013131 (1996)","journal-title":"J. Logic Program."},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Meadows, C.A.: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: 1999 IEEE Symposium on Security and Privacy, pp. 216\u2013231 (1999)","DOI":"10.21236\/ADA465466"},{"issue":"1\/2","key":"8_CR33","doi-asserted-by":"publisher","first-page":"143","DOI":"10.3233\/JCS-2001-91-206","volume":"9","author":"CA Meadows","year":"2001","unstructured":"Meadows, C.A.: A cost-based framework for analysis of denial of service networks. J. Comput. Secur. 9(1\/2), 143\u2013164 (2001)","journal-title":"J. Comput. Secur."},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Meadows, C.A., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.F.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks, pp. 279\u2013298 (2007)","DOI":"10.1007\/978-0-387-46276-9_12"},{"key":"8_CR35","volume-title":"Communicating and Mobile Systems - The Pi-Calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems - The Pi-Calculus. Cambridge University Press, Cambridge (1999)"},{"issue":"12","key":"8_CR36","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). \n                    https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"8_CR37","unstructured":"Nigam, V., Talcott, C., Urquiza, A.A.: Symbolic timed observational equivalence (2018). \n                    https:\/\/arxiv.org\/abs\/1801.04066"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-319-45741-3_23","volume-title":"Computer Security \u2013 ESORICS 2016","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450\u2013470. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-45741-3_23"},{"key":"8_CR39","unstructured":"Rocha, C.: Symbolic reachability analysis for rewrite theories. Ph.D. thesis, University of Illinois at Urbana-Champagne (2012)"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-319-11851-2_11","volume-title":"Security and Trust Management","author":"S Santiago","year":"2014","unstructured":"Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162\u2013177. Springer, Cham (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-11851-2_11"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security, Protocols, and Equational Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-19052-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T01:13:18Z","timestamp":1558573998000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-19052-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030190514","9783030190521"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-19052-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}