{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:30:07Z","timestamp":1725474607921},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540499329"},{"type":"electronic","value":"9783540499336"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11943952_7","type":"book-chapter","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T19:01:12Z","timestamp":1164654072000},"page":"72-83","source":"Crossref","is-referenced-by-count":3,"title":["A Correctness Proof of the DSR Protocol"],"prefix":"10.1007","author":[{"given":"Huabing","family":"Yang","sequence":"first","affiliation":[]},{"given":"Xingyuan","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yuanyuan","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Johnson, D.B., Maltz, D.A., Hu, Y.: The dynamic source routing protocol for mobile ad hoc networks (dsr). Internet Draft: draft-ietf-manet-dsr-10.txt (2004)"},{"issue":"4","key":"7_CR2","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"Journal of the ACM"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Cavalli, A.R., Grepet, C., Maag, S., Tortajada, V.: A validation model for the dsr protocol. In: ICDCS Workshops, pp. 768\u2013773 (2004)","DOI":"10.1109\/ICDCSW.2004.1284120"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Renesse, R., Aghvami, A.H.: Formal verification of ad-hoc routing protocols using spin model checker. In: IEEE MELECON, Dubrovnik, Croatia (2004)","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"7_CR5","unstructured":"Lauschner, T., Macedo, A., Campos, S.: Formal verification and analysis of a routing protocol for ad-hoc networks (2000)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/986858.986861","volume-title":"SASN 2003: Proceedings of the 1st ACM workshop on Security of ad hoc and sensor networks","author":"S. Yang","year":"2003","unstructured":"Yang, S., Baras, J.S.: Modeling vulnerabilities of ad hoc routing protocols. In: SASN 2003: Proceedings of the 1st ACM workshop on Security of ad hoc and sensor networks, pp. 12\u201320. ACM Press, New York (2003)"},{"key":"7_CR7","unstructured":"Zhang, X., Yang, H., Wang, Y.: Liveness reasoning for inductive protocol verification. In: The \u2018Emerging Trend\u2019 of TPHOLs 2005, Oxford University Computing Lab. PRG-RR-05-02, pp. 221\u2013235 (2005)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M.T. Wenzel","year":"1999","unstructured":"Wenzel, M.T.: Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, p. 167. Springer, Heidelberg (1999)"},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"J. Computer Security"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci., 91\u2013130 (1991)","DOI":"10.1016\/0304-3975(91)90041-Y"}],"container-title":["Lecture Notes in Computer Science","Mobile Ad-hoc and Sensor Networks"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11943952_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:52:19Z","timestamp":1619509939000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11943952_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540499329","9783540499336"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11943952_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}