{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T04:18:32Z","timestamp":1775017112608,"version":"3.50.1"},"reference-count":12,"publisher":"Pleiades Publishing Ltd","issue":"8","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1134\/s0361768822080035","type":"journal-article","created":{"date-parts":[[2022,12,20]],"date-time":"2022-12-20T22:02:39Z","timestamp":1671573759000},"page":"781-787","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Optimization of ProVerif Programs for AKE Protocols"],"prefix":"10.1134","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7328-0942","authenticated-orcid":false,"given":"E. M.","family":"Vinarskii","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6573-7925","authenticated-orcid":false,"given":"A. V.","family":"Demakov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2022,12,21]]},"reference":[{"key":"3715_CR1","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Symbolic and computational mechanized verification of the ARINC823 avionic protocols, Proc. 30th IEEE Computer Security Foundations Symp. (CSF), 2017, pp. 68\u201382.","DOI":"10.1109\/CSF.2017.7"},{"key":"3715_CR2","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., and Kobeissi, N., Verified models and reference implementations for the TLS 1.3 standard candidate, Research Report RR-9040, Inria, 2017.","DOI":"10.1109\/SP.2017.26"},{"key":"3715_CR3","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., and Kobeissi, N., Verified models and reference implementations for the TLS 1.3 standard candidate, Proc. IEEE Symp. Security and Privacy (S&P), pp. 483\u2013503.","DOI":"10.1109\/SP.2017.26"},{"key":"3715_CR4","doi-asserted-by":"crossref","unstructured":"Meier, S., Schmidt, B., et al., The TAMARIN prover for the symbolic analysis of security protocols, Proc. 25th Int. Conf. Computer Aided Verification, 2013, pp.\u00a0696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"3715_CR5","unstructured":"Meier, S., Advancing automated security protocol verification, PhD Thesis, ETH Zurich, 2013."},{"key":"3715_CR6","unstructured":"Schmidt, B., Formal analysis of key exchange protocols and physical protocols, PhD Thesis, ETH Zurich, 2012."},{"key":"3715_CR7","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 Privacy Secur., 2016, vol. 1, nos. 1\u20132, pp. 1\u2013135.","journal-title":"Found. Trends Privacy Secur."},{"key":"3715_CR8","doi-asserted-by":"publisher","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B., Automatic verification of correspondences for security protocols, J. Comput. Secur., 2009, vol.\u00a017, no. 4, pp. 363\u2013434.","journal-title":"J. Comput. Secur."},{"key":"3715_CR9","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-10082-1_3","volume":"8604","author":"B. Blanchet","year":"2012","unstructured":"Blanchet, B., Automatic verification of security protocols in the symbolic model: The verifier ProVerif, Lect. Notes Comput. Sci., 2012, vol. 8604, pp. 54\u201387.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3715_CR10","unstructured":"Blanchet, B., CryptoVerif: A computationally sound mechanized prover for cryptographic protocols, Proc. Dagstuhl Seminar on Formal Protocol Verification Applied, 2007."},{"key":"3715_CR11","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1109\/TIT.1985.1057074","volume":"31","author":"T. Elgamal","year":"1985","unstructured":"Elgamal, T., A public-key cryptosystem and a signature scheme based on discrete logarithms, IEEE Trans. Inf. Theory, 1985, vol. 31, no. 4, pp. 469\u2013472.","journal-title":"IEEE Trans. Inf. Theory"},{"key":"3715_CR12","unstructured":"Vinarskii, E., Proverif_code_optimisation. \nhttps:\/\/github.com\/vinevg1996\/proverif_code_optimisation. Accessed October 24, 2021."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768822080035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768822080035","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768822080035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:42:21Z","timestamp":1775011341000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768822080035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":12,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["3715"],"URL":"https:\/\/doi.org\/10.1134\/s0361768822080035","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"12 January 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 February 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 March 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 December 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}