{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:38:14Z","timestamp":1753889894724,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,12,29]],"date-time":"2015-12-29T00:00:00Z","timestamp":1451347200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The Internet, as it stands today, is highly vulnerable to attacks. However,\nlittle has been done to understand and verify the formal security guarantees of\nproposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In\nthis paper, we develop a sound program logic for SANDLog-a declarative\nspecification language for secure routing protocols for verifying properties of\nthese protocols. We prove invariant properties of SANDLog programs that run in\nan adversarial environment. As a step towards automated verification, we\nimplement a verification condition generator (VCGen) to automatically extract\nproof obligations. VCGen is integrated into a compiler for SANDLog that can\ngenerate executable protocol implementations; and thus, both verification and\nempirical evaluation of secure routing protocols can be carried out in this\nunified framework. To validate our framework, we encoded several proposed\nsecure routing mechanisms in SANDLog, verified variants of path authenticity\nproperties by manually discharging the generated verification conditions in\nCoq, and generated executable code based on SANDLog specification and ran the\ncode in simulation.<\/jats:p>","DOI":"10.2168\/lmcs-11(4:19)2015","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:46:40Z","timestamp":1479736000000},"source":"Crossref","is-referenced-by-count":5,"title":["A Program Logic for Verifying Secure Routing Protocols"],"prefix":"10.46298","volume":"Volume 11, Issue 4","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":"25203","published-online":{"date-parts":[[2015,12,29]]},"reference":[{"key":"1104:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1620\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1620\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:08:03Z","timestamp":1681243683000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1620"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,29]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(4:19)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1510.03531","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1510.03531","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,12,29]]},"article-number":"1620"}}