{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T21:08:51Z","timestamp":1790024931686,"version":"4.0.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_4","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"28-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["The DEEPSEC Prover"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Cheval","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Itsaka","family":"Rakotonirina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3127586","volume":"65","author":"M Abadi","year":"2017","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM 65(1), 1\u201341 (2017)","journal-title":"J. ACM"},{"issue":"3","key":"4_CR2","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1016\/j.tcs.2003.12.023","volume":"322","author":"M Abadi","year":"2004","unstructured":"Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427\u2013476 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR3","unstructured":"Adida, B.: Helios: web-based open-audit voting. In: Proceedings of 17th USENIX Security Symposium, USENIX 2008, pp. 335\u2013348. USENIX Association (2008)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.D.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of 23rd Computer Security Foundations Symposium, CSF 2010, pp. 107\u2013121. IEEE Computer Society Press (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-45741-3_13","volume-title":"Computer Security \u2013 ESORICS 2016","author":"M Arapinis","year":"2016","unstructured":"Arapinis, M., Cortier, V., Kremer, S.: When are three voters enough for privacy properties? In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 241\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_13"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Mancini, L., Ritter, E., Ryan, M., Golde, N., Redon, K., Borgaonkar, R.: New privacy issues in mobile telephony: fix and verification. In: Proceedings of 19th Conference on Computer and Communications Security, CCS 2012, pp. 205\u2013216. ACM Press (2012)","DOI":"10.1145\/2382196.2382221"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of Internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27"},{"key":"4_CR8","unstructured":"Baelde, D., Delaune, S., Hirschi, L.: Partial order reduction for security protocols. In: Proceedings of 26th International Conference on Concurrency Theory, CONCUR 2015. Leibniz International Proceedings in Informatics, vol. 42, pp. 497\u2013510. Leibniz-Zentrum f\u00fcr Informatik, September 2015"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Proceedings of 22nd Conference on Computer and Communications Security, CCS 2015, pp. 1144\u20131155. ACM Press (2015)","DOI":"10.1145\/2810103.2813662"},{"issue":"1\u20132","key":"4_CR10","first-page":"1","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)","journal-title":"Found. Trends Priv. Secur."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proceedings of Symposium on Logic in Computer Science, LICS 2005, pp. 331\u2013340. IEEE Computer Society Press (2005)","DOI":"10.1109\/LICS.2005.8"},{"issue":"4","key":"4_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2926715","volume":"23","author":"R Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocol. ACM Trans. Comput. Log. 23(4), 1\u201332 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-642-54862-8_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Cheval","year":"2014","unstructured":"Cheval, V.: APTE: an algorithm for proving trace equivalence. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587\u2013592. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_50"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols - theory and practice. In: Proceedings of 39th IEEE Symposium on Security and Privacy, S&P 2018, pp. 525\u2013542. IEEE Computer Society Press (2018)","DOI":"10.1109\/SP.2018.00033"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S., Dallon, A.: Sat-equiv: an efficient tool for equivalence properties. In: Proceedings of 30th IEEE Computer Security Foundations Symposium, CSF 2017, pp. 481\u2013494. IEEE Computer Society Press (2017)","DOI":"10.1109\/CSF.2017.15"},{"issue":"1","key":"4_CR16","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/JCS-2012-0458","volume":"21","author":"V Cortier","year":"2013","unstructured":"Cortier, V., Smyth, B.: Attacking and fixing helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89\u2013148 (2013)","journal-title":"J. Comput. Secur."},{"key":"4_CR17","unstructured":"The DeepSec Prover, January 2018. https:\/\/deepsec-prover.github.io"},{"issue":"4","key":"4_CR18","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. In: Proceedings of 22nd Symposium on Foundations of Computer Science, FOCS 1981, pp. 350\u2013357. IEEE Computer Society Press (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"4_CR20","unstructured":"MathJax: Beautiful Math in All Browsers. https:\/\/www.mathjax.org"},{"key":"4_CR21","unstructured":"PKI Task Force: PKI for machine readable travel documents offering ICC read-only access. Technical report, International Civil Aviation Organization (2004)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11863908_20","volume-title":"Computer Security \u2013 ESORICS 2006","author":"PYA Ryan","year":"2006","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Pr\u00eat \u00e0 voter with re-encryption mixes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 313\u2013326. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11863908_20"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-319-11851-2_11","volume-title":"Security and Trust Management","author":"S Santiago","year":"2014","unstructured":"Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162\u2013177. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11851-2_11"},{"key":"4_CR24","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":"4_CR25","doi-asserted-by":"crossref","unstructured":"Tiu, A., Dawson, J.: Automating open bisimulation checking for the spi-calculus. In: Proceedings of 23rd Computer Security Foundations Symposium, CSF 2010, pp. 307\u2013321. IEEE Computer Society Press (2010)","DOI":"10.1109\/CSF.2010.28"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-47958-3_5","volume-title":"Programming Languages and Systems","author":"A Tiu","year":"2016","unstructured":"Tiu, A., Nguyen, N., Horne, R.: SPEC: an equivalence checker for security protocols. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 87\u201395. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:20:31Z","timestamp":1571613631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}