{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T03:21:52Z","timestamp":1778037712365,"version":"3.51.4"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,1,5]],"date-time":"2008-01-05T00:00:00Z","timestamp":1199491200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1007\/s10626-007-0032-1","type":"journal-article","created":{"date-parts":[[2008,1,4]],"date-time":"2008-01-04T13:58:36Z","timestamp":1199455116000},"page":"111-159","source":"Crossref","is-referenced-by-count":26,"title":["Analyzing Security Protocols Using Time-Bounded Task-PIOAs"],"prefix":"10.1007","volume":"18","author":[{"given":"Ran","family":"Canetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ling","family":"Cheung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilsun","family":"Kaynar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moses","family":"Liskov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy","family":"Lynch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Pereira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Segala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,5]]},"reference":[{"issue":"2","key":"32_CR1","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M Abadi","year":"2002","unstructured":"Abadi M, Rogaway P (2002) Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol 15(2):103\u2013127","journal-title":"J. Cryptol"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Barthe G, Cerderquist J, Tarento, S (2004) A machine-checked formalization of the generic model and the random oracle model. In: Automated reasoning: second international joint conference (IJCAR). LNCS, vol 3097, pp 385\u2013399","DOI":"10.1007\/978-3-540-25984-8_29"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet B (2005) A computationally sound mechanized prover for security protocols. Cryptology ePrint Archive, Report 2005\/401. http:\/\/eprint.iacr.org\/","DOI":"10.1109\/SP.2006.1"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet B (2006) A computationally sound mechanized prover for security protocols. In: IEEE symposium on security and privacy. Oakland, California, May, pp 140\u2013154","DOI":"10.1109\/SP.2006.1"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Backes M, Pfitzmann B, Waidner, M (2003) A composable cryptographic library with nested operations. In: Proceedings of the 10th ACM conference on computer and communications security (CCS)","DOI":"10.1145\/948109.948140"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Backes M, Pfitzmann B, Waidner M (2004a) A general composition theorem for secure reactive systems. In: First theory of cryptography conference (TCC 2004). LNCS, vol 2951, pp 336\u2013354","DOI":"10.1007\/978-3-540-24638-1_19"},{"key":"32_CR7","unstructured":"Backes M, Pfitzmann B, Waidner M (2004b) Secure asynchronous reactive systems. Cryptology ePrint Archive, Report 2004\/082. http:\/\/eprint.iacr.org\/"},{"key":"32_CR8","unstructured":"Bellare M, Rogaway P (2004) The game-playing technique and its application to triple encryption. Cryptology ePrint Archive, Report 2004\/331. http:\/\/eprint.iacr.org\/"},{"key":"32_CR9","first-page":"292","volume-title":"Advances in cryptology\u2014crypto \u201997. Lecture Notes in Computer Science, vol 1294","author":"C Cachin","year":"1997","unstructured":"Cachin C, Maurer UM (1997) Unconditional security against memory-bounded adversaries. In: Kaliski B (ed) Advances in cryptology\u2014crypto \u201997. Lecture Notes in Computer Science, vol 1294. Berlin, Springer-Verlag, pp 292\u2013306"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Canetti R (2001) Universally composable security: A new paradigm for cryptographic protocols. In: Proceedings of the 42nd Annual Conference on Foundations of Computer Science (FOCS). Full version available at http:\/\/eprint.iacr.org\/2000\/067","DOI":"10.1109\/SFCS.2001.959888"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Canetti R, Herzog J (2006) Universally composable symbolic analysis of mutual authentication and key exchange protocols. In: Halevi S, Rabin T (eds) Proceedings, theory of cryptography conference (TCC). LNCS, Springer, vol 3876, pp 380\u2013403 March. Full version available on http:\/\/eprint.iacr.org\/2004\/334","DOI":"10.1007\/11681878_20"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Canetti R, Lindell Y, Ostrovsky R, Sahai A (2002) Universally composable two-party and multi-party secure computation. In: Proceedings on 34th annual ACM symposium on theory of computing, AMCM, pp 494\u2013503","DOI":"10.1145\/509907.509980"},{"key":"32_CR13","unstructured":"Canetti R, Cheung L, Kaynar D, Liskov M, Lynch N, Pereira O, Segala R (2005) Using probabilistic i\/o automata to analyze an oblivious transfer protocol. Cryptology ePrint Archive, Report 2005\/452. http:\/\/eprint.iacr.org\/ . Version of February 16, 2007"},{"key":"32_CR14","unstructured":"Canetti R, Cheung L, Kaynar D, Liskov M, Lynch N, Pereira O, Segala R (2006a) Task-structured probabilistic I\/O automata. In: Proceedings of the 8th international workshop on discrete event systems (WODES), Ann Arbor, Michigan, July"},{"key":"32_CR15","unstructured":"Canetti R, Cheung L, Kaynar D, Liskov M, Lynch N, Pereira O, Segala R (2006b) Task-structured probabilistic I\/O automata. Technical Report MIT-CSAIL-TR-2006-060, CSAIL, MIT, Cambridge, MA. Submitted for journal publication. Most current version available at http:\/\/theory.csail.mit.edu\/~lcheung\/papers\/task-PIOA-TR.pdf"},{"key":"32_CR16","unstructured":"Canetti R, Cheung L, Kaynar D, Liskov M, Lynch N, Pereira O, Segala R (2006c) Using probabilistic I\/O automata to analyze an oblivious transfer protocol. Technical Report MIT-CSAIL-TR-2006-046, CSAIL, MIT. This is the revised version of Technical Reports MIT-LCS-TR-1001a and MIT-LCS-TR-1001."},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Canetti R, Cheung L, Kaynar D, Lynch N, Pereira O (2007a) Compositional security for Task-PIOAs. In: Proceedings of the 20th IEEE computer security foundations symposium (CSF-20), pp 125\u2013139","DOI":"10.1109\/CSF.2007.15"},{"key":"32_CR18","unstructured":"Canetti R, Cheung L, Lynch N, Pereira O (2007b) On the role of scheduling in simulation-based security. In: Proceedings of the 7th international workshop on issues in the theory of security (WITS\u201907), pp 22\u201337"},{"issue":"29","key":"32_CR19","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D Dolev","year":"1983","unstructured":"Dolev D, Yao AC (1983) On the security of public-key protocols. IEEE Trans Inf Theory 2(29):198\u2013208","journal-title":"IEEE Trans Inf Theory"},{"issue":"6","key":"32_CR20","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S Even","year":"1985","unstructured":"Even S, Goldreich O, Lempel A (1985) A randomized protocol for signing contracts. CACM 28(6):637\u2013647","journal-title":"CACM"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"Goldreich O (2001) Foundations of cryptography volume I basic tools. Cambridge Univ. Press","DOI":"10.1017\/CBO9780511546891"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Goldreich O (2004) Foundations of cryptography, volume II basic applications. Cambridge Univ. Press","DOI":"10.1017\/CBO9780511721656"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Goldreich O, Micali S, Wigderson A (1987) How to play any mental game. In: Proceedings of the 19th symposium on theory of computing (STOC), pp 218\u2013229","DOI":"10.1145\/28395.28420"},{"issue":"1","key":"32_CR24","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1137\/0218012","volume":"18","author":"S Goldwasser","year":"1989","unstructured":"Goldwasser S, Micali S, Rackoff C (1989) The knowledge complexity of interactive proof systems. SIAM J Comput 18(1):186\u2013208","journal-title":"SIAM J Comput"},{"key":"32_CR25","unstructured":"Halevi S (2005) A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181. http:\/\/eprint.iacr.org\/"},{"key":"32_CR26","doi-asserted-by":"crossref","unstructured":"K\u00fcsters R (2006) Simulation-based security with inexhaustible interactive Turing machines. In: Proceedings of the 19th IEEE computer security foundations workshop (CSFW-19 2006). IEEE Computer Society, pp 309\u2013320","DOI":"10.1109\/CSFW.2006.30"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Lincoln PD, Mitchell JC, Mitchell M, Scedrov A (1998) A probabilistic poly-time framework for protocol analysis. In: Proceedings of the 5th ACM conference on computer and communications security (CCS-5), pp 112\u2013121","DOI":"10.1145\/288090.288117"},{"issue":"4","key":"32_CR28","doi-asserted-by":"crossref","first-page":"977","DOI":"10.1137\/S0097539704446487","volume":"37","author":"N Lynch","year":"2007","unstructured":"Lynch N, Segala R, Vaandrager F (2007) Observing branching structure through probabilistic contexts. SIAM J Comput 37(4):977\u20131013","journal-title":"SIAM J Comput"},{"key":"32_CR29","unstructured":"Mateus P, Mitchell JC, Scedrov A (2003) Composition of cryptographic protocols in a probabilistic polynomial-time calculus. In: Proceedings of the 14th International Conference on Concurrency Theory (CONCUR). LNCS, vol 2761, pp 327\u2013349"},{"key":"32_CR30","first-page":"133","volume-title":"Proceedings of the first theory of cryptography conference, LNCS, vol 2951","author":"D Micciancio","year":"2004","unstructured":"Micciancio D, Warinschi B (2004) Soundness of formal encryption in the presence of active adversaries. In: Proceedings of the first theory of cryptography conference, LNCS, vol 2951, Springer, Cambridge, MA, USA, pp 133\u2013151"},{"key":"32_CR31","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Quade J, Unruh D (2007) Long-term security and universal composability. In: Theory of cryptography, proceedings of TCC 2007. Lecture Notes in Computer Science. Springer-Verlag, March. Preprint on IACR ePrint 2006\/422","DOI":"10.1007\/978-3-540-70936-7_3"},{"key":"32_CR32","doi-asserted-by":"crossref","unstructured":"Pfitzmann B, Waidner M (2000) Composition and integrity preservation of secure reactive systems. In: 7th ACM conference on computer and communications security, pp 245\u2013254","DOI":"10.1145\/352600.352639"},{"key":"32_CR33","doi-asserted-by":"crossref","unstructured":"Pfitzmann B, Waidner M (2001) A model for asynchronous reactive systems and its application to secure message transmission. In: IEEE symposium on security and privacy, pp 184\u2013200","DOI":"10.1109\/SECPRI.2001.924298"},{"issue":"3","key":"32_CR34","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/PL00008917","volume":"13","author":"A Pogosyants","year":"2000","unstructured":"Pogosyants A, Segala R, Lynch N (2000) Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distrib Comput 13(3):155\u2013186","journal-title":"Distrib Comput"},{"key":"32_CR35","doi-asserted-by":"crossref","unstructured":"Ramanathan A, Mitchell JC, Scedrov A, Teague V (2004) Probabilistic bisimulation and equivalence for security analysis of network protocols. In: Proceedings of foundations of sotware science and computation structires (FOSSACS). LNCS, vol 2987, pp 468\u2013483","DOI":"10.1007\/978-3-540-24727-2_33"},{"key":"32_CR36","unstructured":"Shoup V (2004) Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332. http:\/\/eprint.iacr.org\/"},{"key":"32_CR37","unstructured":"Segala R (1995) Modeling and verification of randomized distributed real-time systems. PhD Thesis, Department of Electrical Engineering and Computer Science, MIT, May 1995. Also, MIT\/LCS\/TR-676"},{"issue":"2","key":"32_CR38","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala R, Lynch N (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250\u2013273, August","journal-title":"Nord J Comput"},{"key":"32_CR39","unstructured":"Stoelinga MIA, Vaandrager FW (1999) Root contention in IEEE 1394. In: Proc. 5th International AMAST workshop on formal methods for real-time and probabilistic systems. LNCS, vol 1601, Springer, pp 53\u201374"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-007-0032-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-007-0032-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-007-0032-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T17:34:53Z","timestamp":1684172093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-007-0032-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,5]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["32"],"URL":"https:\/\/doi.org\/10.1007\/s10626-007-0032-1","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,5]]}}}