{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:40:40Z","timestamp":1774946440022,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642547911","type":"print"},{"value":"9783642547928","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54792-8_2","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:35:12Z","timestamp":1395408912000},"page":"22-41","source":"Crossref","is-referenced-by-count":13,"title":["Stateful Applied Pi Calculus"],"prefix":"10.1007","author":[{"given":"Myrto","family":"Arapinis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jia","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eike","family":"Ritter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Ryan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"LinkedIn investigates hacking claims, http:\/\/www.guardian.co.uk\/technology\/2012\/jun\/06\/linkedin-hacking"},{"issue":"1-2","key":"2_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci.\u00a0367(1-2), 2\u201332 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115. ACM Press (2001)","DOI":"10.1145\/373243.360213"},{"issue":"3","key":"2_CR4","doi-asserted-by":"publisher","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.\u00a0322(3), 427\u2013476 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: 4th ACM Conference on Computer and Communications Security, pp. 36\u201347. ACM Press (1997)","DOI":"10.1145\/266420.266432"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of IEEE 23rd Computer Security Foundations Symposium, CSF 2010, pp. 107\u2013121 (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Ritter, E., Ryan, M.D.: Statverif: Verification of stateful processes. In: Proceedings of IEEE 24th Computer Security Foundations Symposium, CSF 2011, pp. 33\u201347 (2011), http:\/\/markryan.eu\/research\/statverif\/","DOI":"10.1109\/CSF.2011.10"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: IEEE Symposium on Security and Privacy, pp. 202\u2013215 (2008)","DOI":"10.1109\/SP.2008.23"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: A\u00a0generic tool for computing intruder knowledge. ACM Transactions on Computational Logic\u00a014 (2013)","DOI":"10.1145\/2422085.2422089"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science\u00a07(1) (2011)","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, CCS 2008, pp. 459\u2013468. ACM (2008)","DOI":"10.1145\/1455770.1455828"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic Proof of Strong Secrecy for Security Protocols. In: IEEE Symposium on Security and Privacy, pp. 86\u2013100 (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"issue":"4","key":"2_CR13","doi-asserted-by":"crossref","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. Journal of Computer Security\u00a017(4), 363\u2013434 (2009)","journal-title":"Journal of Computer Security"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-28869-2_6","volume-title":"Programming Languages and Systems","author":"R. Chadha","year":"2012","unstructured":"Chadha, R., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 108\u2013127. Springer, Heidelberg (2012)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-14203-1_35","volume-title":"Automated Reasoning","author":"V. Cheval","year":"2010","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Automating security analysis: Symbolic equivalence of constraint systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 412\u2013426. Springer, Heidelberg (2010)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011), pp. 321\u2013330 (2011)","DOI":"10.1145\/2046707.2046744"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.04.016","volume":"492","author":"V. Cheval","year":"2013","unstructured":"Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoretical Computer Science\u00a0492, 1\u201339 (2013)","journal-title":"Theoretical Computer Science"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF 2009, pp. 266\u2013276. IEEE Computer Society Press (July 2009)","DOI":"10.1109\/CSF.2009.9"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-3(3:2)2007","volume":"3","author":"V. Cortier","year":"2007","unstructured":"Cortier, V., Rusinowitch, M., Zalinescu, E.: Relating two standard notions of secrecy. Logical Methods in Computer Science\u00a03, 1\u201329 (2007)","journal-title":"Logical Methods in Computer Science"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security (2009)","DOI":"10.1007\/978-3-642-12980-3_18"},{"issue":"2","key":"2_CR21","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-2010-0363","volume":"18","author":"S. Delaune","year":"2010","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Symbolic bisimulation for the applied pi calculus. Journal of Computer Security\u00a018(2), 317\u2013377 (2010)","journal-title":"Journal of Computer Security"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proc. of the 24th IEEE Computer Security Foundations Symposium (CSF 2011). IEEE Computer Society Press (2011)","DOI":"10.1109\/CSF.2011.12"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A relational modal logic for higher-order stateful ADTs. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 185\u2013198 (2010)","DOI":"10.1145\/1706299.1706323"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-12510-2_14","volume-title":"Smart Card Research and Advanced Application","author":"F.D. Garcia","year":"2010","unstructured":"Garcia, F.D., van Rossum, P.: Modeling privacy for off-line RFID systems. In: Gollmann, D., Lanet, J.-L., Iguchi-Cartigny, J. (eds.) CARDIS 2010. LNCS, vol.\u00a06035, pp. 194\u2013208. Springer, Heidelberg (2010)"},{"key":"2_CR25","unstructured":"Guttman, J.D.: Fair exchange in strand spaces. Journal of Automated Reasoning (2012)"},{"key":"2_CR26","unstructured":"Koutarou, M.O., Suzuki, K., Kinoshita, S.: Cryptographic approach to \u201cprivacy-friendly\u201d tags. RFID Privacy Workshop (2003)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-38004-4_17","volume-title":"Security and Trust Management","author":"R. K\u00fcnnemann","year":"2013","unstructured":"K\u00fcnnemann, R., Steel, G.: YubiSecure? formal security analysis results for the Yubikey and YubiHSM. In: J\u00f8sang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol.\u00a07783, pp. 257\u2013272. Springer, Heidelberg (2013)"},{"key":"2_CR28","unstructured":"Liu, J.: A proof of coincidence of labeled bisimilarity and observational equivalence in applied pi calculus. Technical Report, ISCAS-SKLCS-11-05 (2011), http:\/\/mail.ios.ac.cn\/~jliu\/papers\/Proof.pdf"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.tcs.2012.07.034","volume":"458","author":"J. Liu","year":"2012","unstructured":"Liu, J., Lin, H.: A complete symbolic bisimulation for full applied pi calculus. Theoretical Computer Science\u00a0458, 76\u2013112 (2012)","journal-title":"Theoretical Computer Science"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proc. 17th ACM Conference on Computer and Communications Security (CCS 2010), pp. 351\u2013360. ACM (2010)","DOI":"10.1145\/1866307.1866348"},{"key":"2_CR31","unstructured":"Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols. Pearson Education (2001)"},{"key":"2_CR32","volume-title":"The \u03c0-calculus: A Theory of Mobile Processes","author":"D. Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of diffie-hellman protocols and advanced security properties. In: 25th Computer Security Foundations Symposium (CSF), pp. 78\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP 2013, pp. 377\u2013390 (2013)","DOI":"10.1145\/2544174.2500600"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54792-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:47:05Z","timestamp":1746157625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54792-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642547911","9783642547928"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54792-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}