{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:19:55Z","timestamp":1725794395869},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436127"},{"type":"electronic","value":"9783662436134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43613-4_8","type":"book-chapter","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T07:56:40Z","timestamp":1400572600000},"page":"117-132","source":"Crossref","is-referenced-by-count":5,"title":["A Program Logic for Verifying Secure Routing Protocols"],"prefix":"10.1007","author":[{"given":"Chen","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Limin","family":"Jia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hao","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cheng","family":"Luo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenchao","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boon Thau","family":"Loo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"ns\u00a03\u00a0project: Network Simulator 3, \n                    \n                      http:\/\/www.nsnam.org\/"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Arnaud, M., Cortier, V., Delaune, S.: Modeling and verifying ad hoc routing protocols. In: Proceedings of CSF (2010)","DOI":"10.1109\/CSF.2010.12"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-22438-6_6","volume-title":"Automated Deduction \u2013 CADE-23","author":"M. Arnaud","year":"2011","unstructured":"Arnaud, M., Cortier, V., Delaune, S.: Deciding security for protocols with recursive tests. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 49\u201363. Springer, Heidelberg (2011)"},{"key":"8_CR4","unstructured":"Bau, J., Mitchell, J.: A security evaluation of DNSSEC with NSEC3. In: Proceedings of NDSS (2010)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4) (2002)","DOI":"10.1145\/581771.581775"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur.\u00a017(4) (December 2009)","DOI":"10.3233\/JCS-2009-0339"},{"key":"8_CR7","unstructured":"Blanchet, B., Smyth, B.: Proverif 1.86: Automatic cryptographic protocol verifier, user manual and tutorial, \n                    \n                      http:\/\/www.proverif.ens.fr\/manual.pdf"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Chen, C., Jia, L., Loo, B.T., Zhou, W.: Reduction-based security analysis of internet routing protocols. In: WRiPE (2012)","DOI":"10.1109\/ICNP.2012.6459941"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chen, C., Jia, L., Xu, H., Luo, C., Zhou, W., Loo, B.T.: A program logic for verifying secure routing protocols. Tech. rep., CIS Dept. University of Pennsylvania (February 2014), \n                    \n                      http:\/\/netdb.cis.upenn.edu\/forte2014","DOI":"10.2168\/LMCS-11(4:19)2015"},{"key":"8_CR10","unstructured":"CNET: How pakistan knocked youtube offline, \n                    \n                      http:\/\/news.cnet.com\/8301-10784_3-9878655-7.html"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cortier, V., Degrieck, J., Delaune, S.: Analysing routing protocols: Four nodes topologies are sufficient. In: Degano, P., Guttman, J.D. (eds.) POST. LNCS, vol.\u00a07215, pp. 30\u201350. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28641-4_3"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A. Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electronic Notes in Theoretical Computer Science\u00a0172, 311\u2013358 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"8_CR13","unstructured":"Engler, D., Musuvathi, M.: Model-checking large network protocol implementations. In: Proceedings of NSDI (2004)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer: grammar generation. In: Proceedings of FMSE (2005)","DOI":"10.1145\/1103576.1103578"},{"key":"8_CR15","first-page":"49","volume":"265","author":"D. Garg","year":"2010","unstructured":"Garg, D., Franklin, J., Kaynar, D., Datta, A.: Compositional system security with interface-confined adversaries. ENTCS\u00a0265, 49\u201371 (2010)","journal-title":"ENTCS"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Goodloe, A., Gunter, C.A., Stehr, M.O.: Formal prototyping in early stages of protocol design. In: Proceedings of ACM WITS (2005)","DOI":"10.1145\/1045405.1045413"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of IEEE 802.11i and TLS. In: Proceedings of CCS (2005)","DOI":"10.1145\/1102120.1102124"},{"key":"8_CR18","unstructured":"Kamp, H.W.: Tense Logic and the Theory of Linear Order. Phd thesis, Computer Science Department, University of California at Los\u00a0Angeles, USA (1968)"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1109\/49.839934","volume":"18","author":"S. Kent","year":"2000","unstructured":"Kent, S., Lynn, C., Mikkelson, J., Seo, K.: Secure border gateway protocol (S-BGP). IEEE Journal on Selected Areas in Communications\u00a018, 103\u2013116 (2000)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative Networking: Language, Execution and Optimization. In: SIGMOD (2006)","DOI":"10.1145\/1142473.1142485"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative networking. Communications of the ACM (2009)","DOI":"10.1145\/1592761.1592785"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Naous, J., Walfish, M., Nicolosi, A., Mazieres, D., Miller, M., Seehra, A.: Verifying and enforcing network paths with ICING. In: Proceedings of CoNEXT (2011)","DOI":"10.1145\/2079296.2079326"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Nigam, V., Jia, L., Loo, B.T., Scedrov, A.: Maintaining distributed logic programs incrementally. In: Proceedings of PPDP (2011)","DOI":"10.1145\/2003476.2003495"},{"key":"8_CR24","unstructured":"One Hundred Eleventh Congress: 2010 report to congress of the u.s.-china economic and security review commission (2010), \n                    \n                      http:\/\/www.uscc.gov\/annual_report\/2010\/annual_report_full_10.pdf"},{"key":"8_CR25","unstructured":"Paulson, L.C.: Mechanized proofs for a recursive authentication protocol. In: Proceedings of CSFW (1997)"},{"key":"8_CR26","unstructured":"RapidNet: A Declarative Toolkit for Rapid Network Simulation and Experimentation, \n                    \n                      http:\/\/netdb.cis.upenn.edu\/rapidnet\/"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-77505-8_15","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"A. Roy","year":"2007","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C., Seifert, J.-P.: Secrecy analysis in protocol composition logic. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 197\u2013213. Springer, Heidelberg (2007)"},{"key":"8_CR28","unstructured":"Wan, T., Kranakis, E., Oorschot, P.C.: Pretty secure BGP (psBGP). In: Proceedings of NDSS (2005)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-92995-6_5","volume-title":"Practical Aspects of Declarative Languages","author":"A. Wang","year":"2008","unstructured":"Wang, A., Basu, P., Loo, B.T., Sokolsky, O.: Declarative network verification. In: Gill, A., Swift, T. (eds.) PADL 2009. LNCS, vol.\u00a05418, pp. 61\u201375. Springer, Heidelberg (2008)"},{"issue":"3","key":"8_CR30","first-page":"15","volume":"6","author":"R. White","year":"2003","unstructured":"White, R.: Securing bgp through secure origin BGP (soBGP). The Internet Protocol Journal\u00a06(3), 15\u201322 (2003)","journal-title":"The Internet Protocol Journal"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Zhang, X., Hsiao, H.C., Hasker, G., Chan, H., Perrig, A., Andersen, D.G.: Scion: Scalability, control, and isolation on next-generation networks. In: Proceedings of IEEE S&P (2011)","DOI":"10.21236\/ADA579930"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43613-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T21:33:41Z","timestamp":1558906421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43613-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436127","9783662436134"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43613-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}