{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:17:51Z","timestamp":1743002271494,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030500856"},{"type":"electronic","value":"9783030500863"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-50086-3_7","type":"book-chapter","created":{"date-parts":[[2020,6,9]],"date-time":"2020-06-09T12:03:09Z","timestamp":1591704189000},"page":"115-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Trace Equivalence and Epistemic Logic to Express Security Properties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-4222","authenticated-orcid":false,"given":"Kiraku","family":"Minami","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,8]]},"reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3127586","journal-title":"J. ACM"},{"issue":"1\u20132","key":"7_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. 367(1\u20132), 2\u201332 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.032","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1\u201370 (1999). https:\/\/doi.org\/10.1006\/inco.1998.2740","journal-title":"Inf. Comput."},{"key":"7_CR4","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15240-5_5","volume-title":"Theoretical Computer Science","author":"MS Alvim","year":"2010","unstructured":"Alvim, M.S., Andr\u00e9s, M.E., Palamidessi, C., van Rossum, P.: Safe equivalences for security properties. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 55\u201370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15240-5_5"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:16)2014","DOI":"10.2168\/LMCS-10(1:16)2014"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.jcss.2017.09.007","volume":"94","author":"R Canetti","year":"2018","unstructured":"Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., Segala, R.: Task-structured probabilistic i\/o automata. J. Comput. Syst. Sci. 94, 63\u201397 (2018). https:\/\/doi.org\/10.1016\/j.jcss.2017.09.007","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-02138-1_12","volume-title":"Formal Techniques for Distributed Systems","author":"R Chadha","year":"2009","unstructured":"Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS\/FORTE -2009. LNCS, vol. 5522, pp. 182\u2013197. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02138-1_12"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-74407-8_4","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"K Chatzikokolakis","year":"2007","unstructured":"Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42\u201358. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_4"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols theory and practice. In: SP 2018, pp. 529\u2013546 (2018). https:\/\/doi.org\/10.1109\/SP.2018.00033","DOI":"10.1109\/SP.2018.00033"},{"key":"7_CR10","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. Theor. Comput. Sci. 492, 1\u201339 (2013). https:\/\/doi.org\/10.1016\/j.tcs.2013.04.016","journal-title":"Theor. Comput. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"7_CR12","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"issue":"4","key":"7_CR13","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435\u2013487 (2009). https:\/\/doi.org\/10.3233\/JCS-2009-0340","journal-title":"J. Comput. Secur."},{"issue":"2","key":"7_CR14","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.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-19249-9_16","volume-title":"FM 2015: Formal Methods","author":"C Eisentraut","year":"2015","unstructured":"Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248\u2013264. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_16"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: CSFW-14, pp. 160\u2013173 (2001). https:\/\/doi.org\/10.1109\/CSFW.2001.930144","DOI":"10.1109\/CSFW.2001.930144"},{"issue":"3","key":"7_CR17","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2009.10.005","volume":"253","author":"S Giro","year":"2009","unstructured":"Giro, S., D\u2019Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. Electron. Notes Theor. Comput. Sci. 253(3), 45\u201371 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.10.005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039066"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-76637-7_12","volume-title":"Programming Languages and Systems","author":"J Goubault-Larrecq","year":"2007","unstructured":"Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi\u2013calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175\u2013190. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_12"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"Automata, Languages and Programming","author":"M Hennessy","year":"1980","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299\u2013309. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10003-2_79"},{"key":"7_CR21","unstructured":"Horne, R.: A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties. arXiv:1811.02536 (2018)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-29485-3_14","volume-title":"Logic and Program Semantics","author":"S Knight","year":"2012","unstructured":"Knight, S., Mardare, R., Panangaden, P.: Combining epistemic logic and hennessy-milner logic. In: Constable, R.L., Silva, A. (eds.) Logic and Program Semantics. LNCS, vol. 7230, pp. 219\u2013243. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29485-3_14"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-32940-1_23","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"S Knight","year":"2012","unstructured":"Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_23"},{"key":"7_CR24","unstructured":"Mano, K.: Formal specification and verification of anonymity and privacy. Ph.D. thesis, Nagoya University (2013)"},{"issue":"6","key":"7_CR25","doi-asserted-by":"publisher","first-page":"1251","DOI":"10.1093\/logcom\/exq013","volume":"20","author":"K Mano","year":"2010","unstructured":"Mano, K., Kawabe, Y., Sakurada, H., Tsukada, Y.: Role interchange for anonymity and privacy of voting. J. Logic Comput. 20(6), 1251\u20131288 (2010). https:\/\/doi.org\/10.1093\/logcom\/exq013","journal-title":"J. Logic Comput."},{"issue":"1","key":"7_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"Inf. Comput."},{"issue":"1","key":"7_CR27","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, II. Inf. Comput. 100(1), 41\u201377 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90009-5","journal-title":"Inf. Comput."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Minami, K.: Trace equivalence and epistemic logic to express security properties. arXiv:1903.03719 (2019)","DOI":"10.1007\/978-3-030-50086-3_7"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Parrow, J., Borgstr\u00f6m, J., Eriksson, L.H., Gutkovas, R., Weber, T.: Modal logics for nominal transition systems. In: CONCUR 2015. LIPIcs, vol. 42, pp. 198\u2013211. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.198","DOI":"10.4230\/LIPIcs.CONCUR.2015.198"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995: Concurrency Theory","author":"R Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234\u2013248. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_17"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L.: A spatial-epistemic logic for reasoning about security protocols. In: SecCo 2010. EPTCS, vol. 51, pp. 1\u201315. Open Publishing Association (2011). https:\/\/doi.org\/10.4204\/EPTCS.51.1","DOI":"10.4204\/EPTCS.51.1"},{"issue":"2","key":"7_CR32","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s10472-016-9516-8","volume":"78","author":"Y Tsukada","year":"2016","unstructured":"Tsukada, Y., Sakurada, H., Mano, K., Manabe, Y.: On compositional reasoning about anonymity and privacy in epistemic logic. Ann. Math. Artif. Intell. 78(2), 101\u2013129 (2016). https:\/\/doi.org\/10.1007\/s10472-016-9516-8","journal-title":"Ann. Math. Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-50086-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,8]],"date-time":"2024-06-08T23:02:09Z","timestamp":1717887729000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-50086-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030500856","9783030500863"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-50086-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 June 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"40","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2020\/forte","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":"25","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":"10","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":"40% - 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":"3","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)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}