{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T16:51:53Z","timestamp":1725987113647},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319989372"},{"type":"electronic","value":"9783319989389"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_8","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T15:08:34Z","timestamp":1533740914000},"page":"130-150","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua D.","family":"Guttman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John D.","family":"Ramsdell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","volume":"51","author":"S Abramsky","year":"1991","unstructured":"Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51, 1\u201377 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"8_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: version 2.0. In: Proceedings of 8th International Workshop on Satisfiability Modulo Theories, vol. 13, p.14 (2010)"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., De Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Logic 7, 58\u201374 (2009)","journal-title":"J. Appl. Logic"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Pironti, A., Strub, P.-Y.: Triple handshakes and cookie cutters: breaking and fixing authentication over TLS. In: IEEE Symposium on Security and Privacy (2014)","DOI":"10.1109\/SP.2014.14"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B Blanchet","year":"2002","unstructured":"Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342\u2013359. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45789-5_25"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: Proceedings of the 2004 IEEE Symposium on Security and Privacy, pp. 86\u2013100. IEEE CS Press, May 2004","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"8_CR7","unstructured":"Blanchet, B.: V\u00e9rification automatique de protocoles cryptographiques: mod\u00e8le formel et mod\u00e8le calculatoire. Habilitation thesis, Universit\u00e9 Paris-Dauphine, November 2008"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3\u201351 (2008)","journal-title":"J. Log. Algebr. Program."},{"issue":"4","key":"8_CR9","doi-asserted-by":"publisher","first-page":"23:1","DOI":"10.1145\/2926715","volume":"17","author":"R Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1\u201323:32 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR10","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: CADE Workshop on Model Computation-Principles, Algorithms, Applications (2003)"},{"key":"8_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78636-8","volume-title":"Operational Semantics and Verification of Security Protocols","author":"C Cremers","year":"2012","unstructured":"Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-540-78636-8"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR13","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, 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"8_CR14","unstructured":"Dougherty, D.J., Guttman, J.D., Ramsdell, J. D.: Homomorphisms and minimality for enrich-by-need security analysis. arXiv.org http:\/\/arxiv.org\/abs\/1804.07158 , April 2018"},{"issue":"4","key":"8_CR15","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/s00493-015-3003-4","volume":"37","author":"PL Erd\u00f6s","year":"2017","unstructured":"Erd\u00f6s, P.L., P\u00e1lv\u00f6lgyi, D., Tardif, C., Tardos, G.: Regular families of forests, antichains and duality pairs of relational structures. Combinatorica 37(4), 651\u2013672 (2017)","journal-title":"Combinatorica"},{"key":"8_CR16","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). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/1061318.1061323","volume":"30","author":"R Fagin","year":"2005","unstructured":"Fagin, R., Kolaitis, P., Popa, L.: Data exchange: getting to the core. ACM Trans. Database Syst. (TODS) 30(1), 174\u2013210 (2005)","journal-title":"ACM Trans. Database Syst. (TODS)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-31987-0_11","volume-title":"Programming Languages and Systems","author":"C Fournet","year":"2005","unstructured":"Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 141\u2013156. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_11"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s00165-004-0058-1","volume":"17","author":"AD Gordon","year":"2005","unstructured":"Gordon, A.D., Pucella, R.: Validating a web service security abstraction by typing. Formal Asp. Comput. 17(3), 277\u2013318 (2005)","journal-title":"Formal Asp. Comput."},{"key":"8_CR20","unstructured":"Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)"},{"issue":"2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"201","DOI":"10.3233\/JCS-140497","volume":"22","author":"JD Guttman","year":"2014","unstructured":"Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201\u2013267 (2014)","journal-title":"J. Comput. Secur."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11580850_8","volume-title":"Trustworthy Global Computing","author":"JD Guttman","year":"2005","unstructured":"Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116\u2013145. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11580850_8"},{"issue":"2","key":"8_CR23","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/S0304-3975(01)00139-6","volume":"283","author":"JD Guttman","year":"2002","unstructured":"Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoret. Comput. Sci. 283(2), 333\u2013380 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-24725-8_23","volume-title":"Programming Languages and Systems","author":"JD Guttman","year":"2004","unstructured":"Guttman, J.D., Thayer, F.J., Carlson, J.A., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Trust management in strand spaces: a Rely-Guarantee method. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 325\u2013339. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_23"},{"issue":"1\u20133","key":"8_CR25","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0012-365X(92)90282-K","volume":"109","author":"P Hell","year":"1992","unstructured":"Hell, P., Ne\u0161et\u0159il, J.: The core of a graph. Discret. Math. 109(1\u20133), 117\u2013126 (1992)","journal-title":"Discret. Math."},{"key":"8_CR26","volume-title":"Software Abstractions","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions, 2nd edn. MIT Press, Cambridge (2012)","edition":"2"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Rowe, P.D., Thayer, F.J.: Completeness of CPSA. Technical Report MTR110479, The MITRE Corporation, March 2011. http:\/\/www.mitre.org\/publications\/technical-papers\/completeness-of-cpsa","DOI":"10.21236\/ADA562264"},{"key":"8_CR28","volume-title":"Foundations of Disjunctive Logic Programming","author":"J Lobo","year":"1992","unstructured":"Lobo, J., Minker, J., Rajasekar, A.: Foundations of Disjunctive Logic Programming. MIT Press, Cambridge (1992)"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"McCune, W.: MACE 2.0 Reference Manual and Guide. CoRR (2001)","DOI":"10.2172\/797949"},{"key":"8_CR30","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. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"8_CR31","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: 35th International Conference on Software Engineering (ICSE), pp. 232\u2013241 (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"8_CR34","unstructured":"Ramsdell, J.D.: Deducing security goals from shape analysis sentences. The MITRE Corporation, April 2012. http:\/\/arxiv.org\/abs\/1204.0480"},{"key":"8_CR35","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA4: a cryptographic protocol shapes analyzer (2017). https:\/\/github.com\/ramsdell\/cpsa"},{"key":"8_CR36","unstructured":"Ramsdell, J.D., Guttman, J.D., Liskov, M.: CPSA: a cryptographic protocol shapes analyzer (2016). http:\/\/hackage.haskell.org\/package\/cpsa"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Rescorla, E., Ray, M., Dispensa, S., Oskov, N.: Transport Layer Security (TLS) Renegotiation Indication Extension. RFC 5746 (Proposed Standard), February 2010","DOI":"10.17487\/rfc5746"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_42"},{"key":"8_CR39","volume-title":"Handbook of Automated Reasoning","author":"A Robinson","year":"2001","unstructured":"Robinson, A.: Handbook of Automated Reasoning, vol. 2. Elsevier, Hoboken (2001)"},{"issue":"3","key":"8_CR40","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1379759.1379763","volume":"55","author":"B Rossman","year":"2008","unstructured":"Rossman, B.: Homomorphism preservation theorems. J. ACM (JACM) 55(3), 15 (2008)","journal-title":"J. ACM (JACM)"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Int. J. Inf. Secur. (2016). https:\/\/doi.org\/10.1007\/s10207-016-0319-z . http:\/\/web.cs.wpi.edu\/~guttman\/pubs\/ijis_measuring-security.pdf","DOI":"10.1007\/s10207-016-0319-z"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-319-21401-6_30","volume-title":"Automated Deduction \u2013 CADE-25","author":"S Saghafi","year":"2015","unstructured":"Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434\u2013449. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_30"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98938-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T01:01:43Z","timestamp":1571706103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}