{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T10:58:40Z","timestamp":1791284320059,"version":"4.1.0"},"reference-count":23,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2001,1]]},"abstract":"<jats:p>Contextual equivalences for cryptographic process calculi, like the spi-calculus, can be used to reason about correctness of protocols, but their definition suffers from quantification over all possible contexts. Here, we focus on two such equivalences, namely may-testing and barbed equivalence, and investigate tractable proof methods for them. To this aim, we design an enriched labelled transition system, where transitions are constrained by the knowledge the environment has of names and keys. The new transition system is then used to define a trace equivalence and a weak bisimulation equivalence that avoid quantification over contexts. Our main results are soundness and completeness of trace and weak bisimulation equivalence with respect to may-testing and barbed equivalence, respectively. They lead to more direct proof methods for equivalence checking. The use of these methods is illustrated with a few examples concerning implementation of secure channels and verification of protocol correctness.<\/jats:p>","DOI":"10.1137\/s0097539700377864","type":"journal-article","created":{"date-parts":[[2003,6,11]],"date-time":"2003-06-11T11:12:06Z","timestamp":1055329926000},"page":"947-986","source":"Crossref","is-referenced-by-count":53,"title":["Proof Techniques for Cryptographic Processes"],"prefix":"10.1137","volume":"31","author":[{"given":"Michele","family":"Boreale","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rosario","family":"Pugliese","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2012,2,17]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","unstructured":"M. Abadi,\n                      Protection in programming\u2010language translations\n                      , in Proceedings ICALP\u201998, Lecture Notes in Comput. Sci. 1443, K. G. Larsen, S. Skyum, and G. Winskel, eds., Springer\u2010Verlag, New York, 1998, pp. 868\u2013883.","DOI":"10.1007\/BFb0055109"},{"key":"R2","doi-asserted-by":"crossref","unstructured":"M. Abadi,\n                      Secrecy by typing in security protocols\n                      , in Proceedings STACS\u201997, Lecture Notes in Comput. Sci. 1281, Springer\u2010Verlag, New York, 1997, pp. 611\u2013638.","DOI":"10.1007\/BFb0014571"},{"key":"R3","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00223-5"},{"key":"R4","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, and G. Gonthier,\n                      Secure implementation of channel abstractions\n                      , in Proceedings of the 13th IEEE Symposium Logic Computer Science (LICS\u201998), IEEE Computer Society Press, Los Alamitos, CA, 1998, pp. 105\u2013116.","DOI":"10.1109\/LICS.1998.705647"},{"key":"R5","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. D. Gordon,\n                      Reasoning about cryptographic protocols in the spi calculus\n                      , in Proceedings CONCUR\u201997, A. Mazurkiewicz and J. Winkowsky, eds., Lecture Notes in Comput. Sci. 1243, Springer\u2010Verlag, New York, 1997, pp. 59\u201373.","DOI":"10.1007\/3-540-63141-0_5"},{"key":"R6","first-page":"267","volume":"5","author":"Abadi Mart\u00edn","year":"1998","journal-title":"Nordic J. Comput."},{"key":"R7","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"R8","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1114"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"M. Boreale, R. De Nicola, and R. Pugliese,\n                      Proof techniques for cryptographic processes\n                      , in Proceedings of the 14th IEEE Symposium Logic in Computer Science (LICS\u201999), IEEE Computer Society Press, Los Alamitos, CA, 1999, pp. 157\u2013166.","DOI":"10.1109\/LICS.1999.782608"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"M. Boreale and D. Sangiorgi,\n                      Bisimulation in name\u2010passing calculi without matching\n                      , in Proceedings of the 13th IEEE Symposium Logic in Computer Science (LICS\u201998), IEEE Computer Society Press, Los Alamitos, CA, 1998, pp. 165\u2013175.","DOI":"10.1109\/LICS.1998.705653"},{"key":"R11","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"R12","unstructured":"Anders Elkj\u00e6r, Michael H\u00f6hle, Hans H\u00fcttel, Kasper Overg\u00e5rd, Towards automatic bisimilarity checking in the spi calculus, Aust. Comput. Sci. Commun., Vol. 21, Springer, Singapore, 1999, 175\u20131891717558"},{"key":"R13","doi-asserted-by":"crossref","unstructured":"P. D. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov,\n                      A probabilistic poly\u2010time framework for protocol analysis\n                      , in Fifth ACM Conference on Computer and Communication Security (CCS\u20105), San Francisco, CA, 1998, pp. 112\u2013121.","DOI":"10.1145\/288090.288117"},{"key":"R14","doi-asserted-by":"crossref","unstructured":"G. Lowe,\n                      Breaking and fixing the Needham\u2010Schroeder public\u2010key protocol using fdr\n                      , in Proceedings TACAS\u201996, T. Margaria and B. Steffen, eds., Lecture Notes in Comput. Sci. 1055, Springer\u2010Verlag, New York, 1996, pp. 147\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"R15","unstructured":"R. Milner,\n                      Communication and Concurrency\n                      , Prentice\u2013Hall, New York, 1989."},{"key":"R16","doi-asserted-by":"crossref","unstructured":"Robin Milner, The polyadic \u03c0\u2010calculus: a tutorial, NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., Vol. 94, Springer, Berlin, 1993, 203\u201324694j:68066","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"R17","first-page":"0","volume":"100","author":"Milner Robin","year":"1992","journal-title":"Inform. and Comput."},{"key":"R18","first-page":"0","volume":"100","author":"Milner Robin","year":"1992","journal-title":"Inform. and Comput."},{"key":"R19","doi-asserted-by":"crossref","unstructured":"R. Milner and D. Sangiorgi,\n                      Barbed bisimulation\n                      , in Proceedings ICALP\u201992, W. Kuich, ed., Lecture Notes in Comput. Sci. 623, Springer\u2010Verlag, New York, 1992, pp. 685\u2013695.","DOI":"10.1007\/3-540-55719-9_114"},{"key":"R20","unstructured":"A. W. Roscoe,\n                      Modelling and verifying key\u2010exchange using CSP and FDR\n                      , in 8th Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos, CA, 1995."},{"key":"R21","unstructured":"M. C. Sanderson,\n                      Proof Techniques for CCS\n                      , Internal report CST\u201019\u201082, Department of Computer Science, University of Edinburgh, UK, 1982."},{"key":"R22","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"R23","doi-asserted-by":"publisher","DOI":"10.1109\/32.713329"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/S0097539700377864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:18:33Z","timestamp":1787336313000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/S0097539700377864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,1]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,1]]}},"alternative-id":["10.1137\/S0097539700377864"],"URL":"https:\/\/doi.org\/10.1137\/s0097539700377864","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,1]]}}}