{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:15:19Z","timestamp":1743066919409,"version":"3.40.3"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030906351"},{"type":"electronic","value":"9783030906368"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-90636-8_1","type":"book-chapter","created":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T09:02:36Z","timestamp":1636016556000},"page":"3-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Learning Assumptions for Verifying Cryptographic Protocols Compositionally"],"prefix":"10.1007","author":[{"given":"Zichao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arthur Azevedo","family":"de Amorim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Limin","family":"Jia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,28]]},"reference":[{"key":"1_CR1","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. CoRR abs\/1609.03003 (2016). http:\/\/arxiv.org\/abs\/1609.03003"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6\u201315 (1996). https:\/\/doi.org\/10.1109\/32.481513","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548\u2013562. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_52"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/BFb0015258","volume-title":"Computer Science Today","author":"R Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Programming Satan\u2019s computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 426\u2013440. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0015258"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Andova, S., Cremers, C., Gj\u00f8steen, K., Mauw, S., Mj\u00f8lsnes, S.F., Radomirovi\u0107, S.: A framework for compositional verification of security protocols. Inf. Comput. 206(2), 425\u2013459 (2008). Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA 2006). https:\/\/doi.org\/10.1016\/j.ic.2007.07.002. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540107001228","DOI":"10.1016\/j.ic.2007.07.002"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","journal-title":"Inf. Comput."},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21\u201323 January 2009, pp. 90\u2013101. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-01465-9_1","volume-title":"Formal Aspects in Security and Trust","author":"G Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Zanella B\u00e9guelin, S.: Formal certification of ElGamal encryption. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 1\u201319. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01465-9_1"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15\u201319 October 2018, pp. 1383\u20131396. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243846","DOI":"10.1145\/3243734.3243846"},{"issue":"5","key":"1_CR11","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1145\/381906.381946","volume":"20","author":"SM Bellovin","year":"1990","unstructured":"Bellovin, S.M., Merritt, M.: Limitations of the Kerberos authentication system. SIGCOMM Comput. Commun. Rev. 20(5), 119\u2013132 (1990). https:\/\/doi.org\/10.1145\/381906.381946","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, 22\u201326 May 2017, pp. 483\u2013502. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/SP.2017.26","DOI":"10.1109\/SP.2017.26"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 445\u2013456 (2010). https:\/\/doi.org\/10.1145\/1706299.1706350","DOI":"10.1145\/1706299.1706350"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), Cape Breton, Nova Scotia, Canada, 11\u201313 June 2001, pp. 82\u201396. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/CSFW.2001.930138","DOI":"10.1109\/CSFW.2001.930138"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy (S&P 2006), Berkeley, California, USA, 21\u201324 May 2006, pp. 140\u2013154. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/SP.2006.1","DOI":"10.1109\/SP.2006.1"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proceedings of the 2006 IEEE Symposium on Security and Privacy, SP 2006, pp. 140\u2013154. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/SP.2006.1","DOI":"10.1109\/SP.2006.1"},{"issue":"1\u20132","key":"1_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/3300000004","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016). https:\/\/doi.org\/10.1561\/3300000004","journal-title":"Found. Trends Priv. Secur."},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: Symbolic and computational mechanized verification of the ARINC823 avionic protocols. In: 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, 21\u201325 August 2017, pp. 68\u201382. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/CSF.2017.7","DOI":"10.1109\/CSF.2017.7"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135\u2013148. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_14"},{"issue":"1","key":"1_CR20","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18\u201336 (1990). https:\/\/doi.org\/10.1145\/77648.77649","journal-title":"ACM Trans. Comput. Syst."},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Computer Aided Verification","author":"S Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 534\u2013547. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_51"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-14295-6_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2010","unstructured":"Chen, Y.-F., Clarke, E.M., Farzan, A., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y.: Automated assume-guarantee reasoning through implicit learning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 511\u2013526. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_44"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-F Chen","year":"2009","unstructured":"Chen, Y.-F., Farzan, A., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31\u201345. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_3"},{"key":"1_CR24","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0102s\u0102reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"CJF Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The Scyther Tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414\u2013418. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_38"},{"key":"1_CR27","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). Electron. Notes Theor. Comput. Sci. 172, 311\u2013358 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.02.012","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"8","key":"1_CR28","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"DE Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Commun. ACM 24(8), 533\u2013536 (1981). https:\/\/doi.org\/10.1145\/358722.358740","journal-title":"Commun. ACM"},{"issue":"2","key":"1_CR29","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"},{"issue":"1","key":"1_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/JCS-191358","volume":"28","author":"J Dreier","year":"2020","unstructured":"Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Verification of stateful cryptographic protocols with exclusive OR. J. Comput. Secur. 28(1), 1\u201334 (2020). https:\/\/doi.org\/10.3233\/JCS-191358","journal-title":"J. Comput. Secur."},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, 19\u201323 May 2019, pp. 1202\u20131219. IEEE (2019). https:\/\/doi.org\/10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"1_CR32","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"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.Y.: Modular code-based cryptographic verification. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, pp. 341\u2013350. Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/2046707.2046746","DOI":"10.1145\/2046707.2046746"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. Proc. ACM Program. Lang. 3(POPL), 63:1\u201363:30 (2019). https:\/\/doi.org\/10.1145\/3290376","DOI":"10.1145\/3290376"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. In: 2001 Proceedings of the 14th IEEE Computer Security Foundations Workshop, pp. 145\u2013159 (2001)","DOI":"10.1109\/CSFW.2001.930143"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Kobeissi, N., Bhargavan, K., Blanchet, B.: Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach. In: 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, 26\u201328 April 2017, pp. 435\u2013450. IEEE (2017). https:\/\/doi.org\/10.1109\/EuroSP.2017.38","DOI":"10.1109\/EuroSP.2017.38"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Kohl, J., Neuman, C., et al.: The Kerberos network authentication service (V5). Technical report, RFC 1510, September 1993","DOI":"10.17487\/rfc1510"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Liao, K., Hammer, M.A., Miller, A.: ILC: a calculus for composable, computational cryptography. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 640\u2013654. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314607","DOI":"10.1145\/3314221.3314607"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147\u2013166. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_43"},{"key":"1_CR41","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31\u201343. IEEE (1997)"},{"key":"1_CR42","volume-title":"Concurrency: State Models and Java Programs","author":"J Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Hoboken (1999)"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 110\u2013121. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028738"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 342\u2013346. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_30"},{"key":"1_CR45","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"},{"issue":"4","key":"1_CR46","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), Pacific Grove, California, USA, 5\u20138 June 1989, pp. 14\u201323. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 139\u2013153. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_14"},{"issue":"12","key":"1_CR49","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). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"1_CR50","unstructured":"Panti, M., Spalazzi, L., Tacconi, S.: Using the NuSMV model checker to verify the Kerberos protocol (2002)"},{"issue":"3","key":"1_CR51","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS Pasareanu","year":"2008","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175\u2013205 (2008). https:\/\/doi.org\/10.1007\/s10703-008-0049-6","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR52","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, vol. 13, pp. 123\u2013144. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5"},{"key":"1_CR53","doi-asserted-by":"publisher","unstructured":"Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, 25\u201327 June 2012, pp. 78\u201394. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/CSF.2012.25","DOI":"10.1109\/CSF.2012.25"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Whitefield, J., Chen, L., Sasse, R., Schneider, S., Treharne, H., Wesemeyer, S.: A symbolic analysis of ECC-based direct anonymous attestation. In: IEEE European Symposium on Security and Privacy, EuroS&P 2019, Stockholm, Sweden, 17\u201319 June 2019, pp. 127\u2013141. IEEE (2019). https:\/\/doi.org\/10.1109\/EuroSP.2019.00019","DOI":"10.1109\/EuroSP.2019.00019"},{"issue":"1","key":"1_CR55","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/2.108052","volume":"25","author":"TYC Woo","year":"1992","unstructured":"Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39\u201352 (1992)","journal-title":"Computer"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 178\u2013194. IEEE (1993)","DOI":"10.1109\/RISP.1993.287633"},{"key":"1_CR57","unstructured":"Zhang, Z., de Amorim, A.A., Jia, L., P\u0103s\u0103reanu, C.: Automating compositional analysis of authentication protocols. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020 (2020)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-90636-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T13:33:56Z","timestamp":1726061636000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-90636-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030906351","9783030906368"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-90636-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"28 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/facs2021.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1,7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}