{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:16:38Z","timestamp":1712369798281},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,2,12]],"date-time":"2014-02-12T00:00:00Z","timestamp":1392163200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s11227-014-1099-8","type":"journal-article","created":{"date-parts":[[2014,2,11]],"date-time":"2014-02-11T19:15:17Z","timestamp":1392146117000},"page":"629-672","source":"Crossref","is-referenced-by-count":6,"title":["A BSP algorithm for on-the-fly checking CTL* formulas on security protocols"],"prefix":"10.1007","volume":"69","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Gava","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franck","family":"Pommereau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u00ebl","family":"Guedj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,12]]},"reference":[{"issue":"4","key":"1099_CR1","doi-asserted-by":"crossref","first-page":"403","DOI":"10.3166\/jancl.19.403-429","volume":"19","author":"A Armando","year":"2009","unstructured":"Armando A, Carbone R, Compagna L (2009) Ltl model checking for security protocols. Appl Non Class Log 19(4):403\u2013429","journal-title":"Appl Non Class Log"},{"key":"1099_CR2","unstructured":"Armando A, et al (2005) The AVISPA tool for the automated validation of Internet security protocols and applications. In: Etessami K, Rajamani SK (eds) Proceedings of Computer Aided Verification (CAV), LNCS. Springer, vol 3576, pp 281\u2013285"},{"key":"1099_CR3","unstructured":"Backes M, Unruh D (2008) Theory and application of cryptology and information security (ASIACRYPT), LNCS. In: Pieprzyk J (ed) Limits of constructive security proofs. Springer, New York, pp 290\u2013307"},{"key":"1099_CR4","unstructured":"Barnat J, Brim L, C\u00ebern\u00e1 I (2002) Property driven distribution of nested dfs. In: Leuschel M, Ultes-Nitsche U (eds) Workshop on verification and computational logic (VCL), vol DSSE-TR-2002-5, pp 1\u201310. Department of Electronics and Computer Science, University of Southampton (DSSE), UK, Technical Report"},{"issue":"1","key":"1099_CR5","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1093\/logcom\/exp003","volume":"21","author":"J Barnat","year":"2011","unstructured":"Barnat J, Chaloupka J, Pol JVD (2011) Distributed algorithms for SCC decomposition. J Log Comput 21(1):23\u201344","journal-title":"J Log Comput"},{"key":"1099_CR6","volume-title":"Model checking security protocols, chap 24","author":"D Basin","year":"2011","unstructured":"Basin D, Cremers C, Meadows C (2011) Model checking security protocols, chap 24. Springer, New York"},{"key":"1099_CR7","doi-asserted-by":"crossref","unstructured":"Bhat G, Cleaveland R, Grumberg O (1995) Efficient on-the-fly model checking for ctl*. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, pp 388\u2013398","DOI":"10.1109\/LICS.1995.523273"},{"key":"1099_CR8","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198529392.001.0001","volume-title":"Parallel scientific computation. A structured approach using BSP and MPI","author":"RH Bisseling","year":"2004","unstructured":"Bisseling RH (2004) Parallel scientific computation. A structured approach using BSP and MPI. Oxford University Press, Oxford"},{"key":"1099_CR9","doi-asserted-by":"crossref","unstructured":"Blanchet B (2001) An efficient cryptographic protocol verifier based on Prolog rules. In: IEEE CSFW\u201901. IEEE Computer Society","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"1","key":"1099_CR10","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1093\/logcom\/exp004","volume":"21","author":"S Blom","year":"2011","unstructured":"Blom S, Lisser B, van de Pol J, Weber M (2011) A database approach to distributed state-space generation. J Log Comput 21(1):45\u201362","journal-title":"J Log Comput"},{"issue":"1\/2","key":"1099_CR11","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1504\/IJCCBS.2012.045076","volume":"3","author":"MC Boukala","year":"2012","unstructured":"Boukala MC, Petrucci L (2012) Distributed model-checking and counterexample search for ctl logic. IJCCBS 3(1\/2):44\u201359","journal-title":"IJCCBS"},{"key":"1099_CR12","doi-asserted-by":"crossref","unstructured":"Brucker AD, M\u00f6dersheim S (2009) Integrating automated and interactive protocol verification. In: Formal Aspects in Security and Trust (FAST), LNCS, vol 5983. Springer, New York, pp 248\u2013262","DOI":"10.1007\/978-3-642-12459-4_18"},{"key":"1099_CR13","doi-asserted-by":"crossref","unstructured":"Chaou S, Utard G, Pommereau F (2011) Evaluating a peer-to-peer storage system in presence of malicious peers. In: Smari WW, McIntire JP (eds) High performance computing and simulation (HPCS). IEEE, pp 419\u2013426","DOI":"10.1109\/HPCSim.2011.5999855"},{"key":"1099_CR14","doi-asserted-by":"crossref","unstructured":"Christensen S, Kristensen LM, Mailund T (2001) A sweep-line method for state space exploration. In: Margaria T, Yi W (eds) Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol 2031. Springer, New York, pp 450\u2013464","DOI":"10.1007\/3-540-45319-9_31"},{"issue":"1","key":"1099_CR15","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1287\/ijoc.10.1.82","volume":"10","author":"G Ciardo","year":"1998","unstructured":"Ciardo G, Gluckman J, Nicol DM (1998) Distributed state space generation of discrete-state stochastic models. INFORMS J Computg 10(1):82\u201393","journal-title":"INFORMS J Computg"},{"key":"1099_CR16","unstructured":"Comon-Lundh H, Cortier V (2011) How to prove security of communication protocols? a discussion on the soundness of formal models w.r.t. computational ones. In: STACS, pp 29\u201344"},{"key":"1099_CR17","first-page":"30","volume-title":"Analysing routing protocols: four nodes topologies are sufficient","author":"V Cortier","year":"2012","unstructured":"Cortier V, Degrieck J, Delaune S (2012) Principles of security and trust (POST), LNCS. In: Degano P, Guttman JD (eds) Analysing routing protocols: four nodes topologies are sufficient. Springer, New York, pp 30\u201350"},{"key":"1099_CR18","unstructured":"Cremers CJF (2006) Scyther-semantics and verification of security protocols. Ph.D. thesis, Technische Universiteit Eindhoven"},{"key":"1099_CR19","doi-asserted-by":"crossref","unstructured":"Cremers JF, Lafourcade P, Nadeau P (2009) Comparing state spaces in automatic security protocol analysis. In: Formal to Practical Security, LNCS, vol 5458. Springer, New York, pp 70\u201394","DOI":"10.1007\/978-3-642-02002-5_5"},{"issue":"2","key":"1099_CR20","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev D, Yao AC (1983) On the security of public key protocols. IEEE Trans Inf Theory 29(2):198\u2013208","journal-title":"IEEE Trans Inf Theory"},{"key":"1099_CR21","first-page":"248","volume-title":"Hybrid on-the-fly ltl model checking with the sweep-line method","author":"S Evangelista","year":"2012","unstructured":"Evangelista S, Kristensen LM (2012) Application and theory of petri nets, LNCS. In: Haddad S, Pomello L (eds) Hybrid on-the-fly ltl model checking with the sweep-line method. Springer, New York, pp 248\u2013267"},{"issue":"1","key":"1099_CR22","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.entcs.2007.10.020","volume":"198","author":"J Ezekiel","year":"2008","unstructured":"Ezekiel J, L\u00fcttgen G (2008) Measuring and evaluating parallel state-space exploration algorithms. Electron Notes Theor Comput Sci 198(1):47\u201361","journal-title":"Electron Notes Theor Comput Sci"},{"key":"1099_CR23","first-page":"191","volume-title":"Partial order reduction for branching security protocols","author":"W Fokkink","year":"2010","unstructured":"Fokkink W, Dashti MT, Wijs A (2010) Conference on Application of Concurrency to System Design (ACSD). In: Gomes L, Khomenko V, Fernandes JM (eds) Partial order reduction for branching security protocols. IEEE Computer Society, Portugal, pp 191\u2013200"},{"key":"1099_CR24","first-page":"217","volume-title":"Parallel state space construction for model-checking","author":"H Garavel","year":"2001","unstructured":"Garavel H, Mateescu R, Smarandache IM (2001) Proceedings of SPIN, LNCS. In: Dwyer MB (ed) Parallel state space construction for model-checking. Springer, New York, pp 217\u2013234"},{"key":"1099_CR25","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/j.entcs.2010.04.009","volume":"262","author":"V Goranko","year":"2010","unstructured":"Goranko V, Kyrilov A, Shkatov D (2010) Tableau tool for testing satisfiability in ltl: implementation and experimental analysis. Electron Notes Theor Comput Sci 262:113\u2013125","journal-title":"Electron Notes Theor Comput Sci"},{"key":"1099_CR26","unstructured":"Guedj M (2012) Bsp algorithms for ltl & ctl* model checking of security protocols. Ph.D. thesis, University of Paris-Est"},{"key":"1099_CR27","doi-asserted-by":"crossref","unstructured":"Hinsen K (2007) Parallel scripting with Python. Comput Sci Eng 9(6):82\u201389","DOI":"10.1109\/MCSE.2007.117"},{"key":"1099_CR28","first-page":"23","volume-title":"On nested depth first search (extended abstract)","author":"G Holzmann","year":"1996","unstructured":"Holzmann G, Peled D, Yannakakis M (1996) The spin verification system. On nested depth first search (extended abstract). American Mathematical Society, USA, pp 23\u201332"},{"key":"1099_CR29","unstructured":"Inggs C, Barringer H, Nenadic A, Zhang N (2004) Model checking a security protocol. In: Southern African Telecommunications Network and Applications Conference (SATNAC)"},{"issue":"2","key":"1099_CR30","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/s10703-006-0008-z","volume":"29","author":"CP Inggs","year":"2006","unstructured":"Inggs CP, Barringer H (2006) Ctl $$^{\\text{* }}$$ * model checking on a shared-memory architecture. Form Methods Syst Des 29(2):135\u2013155","journal-title":"Form Methods Syst Des"},{"key":"1099_CR31","unstructured":"Losup A, Sonmez O, Anoep S, Epema D (2008) The performance of bags-of-tasks in large-scale distributed systems. In: Symposium on High performance distributed computing (HPDC). ACM, USA, pp 97\u2013108"},{"issue":"17","key":"1099_CR32","doi-asserted-by":"crossref","first-page":"1606","DOI":"10.1016\/S0140-3664(02)00049-X","volume":"25","author":"S Kremer","year":"2002","unstructured":"Kremer S, Markowitch O, Zhou J (2002) An intensive survey of fair non-repudiation protocols. Comput Commun 25(17):1606\u20131621","journal-title":"Comput Commun"},{"key":"1099_CR33","doi-asserted-by":"crossref","unstructured":"Kumar R, Mercer EG (2005) Load balancing parallel explicit state model checking. In: ENTCS, vol 128. Elsevier, Amsterdam, pp 19\u201334","DOI":"10.1016\/j.entcs.2004.10.016"},{"key":"1099_CR34","first-page":"22","volume-title":"Distributed-memory model checking with SPIN","author":"F Lerda","year":"1999","unstructured":"Lerda F, Sista R (1999) Proceedings of SPIN, no. 1680 in LNCS. In: Dams D, Gerth R, Leue S, Massink M (eds) Distributed-memory model checking with SPIN. Springer, New York, pp 22\u201339"},{"key":"1099_CR35","doi-asserted-by":"crossref","unstructured":"Leucker M, Somla R, Weber M (2003) Parallel model checking for ltl, ctl*, l. Electron Notes Theor Comput Sci 1\u20131","DOI":"10.1016\/S1571-0661(05)80093-3"},{"key":"1099_CR36","unstructured":"Margaria T, Steffen B (eds) (1996) Tools and algorithms for construction and analysis of systems (TACAS), LNCS. Breaking and fixing the needham-schroeder public-key protocol using fdr. Springer, New York, pp 147\u2013166"},{"key":"1099_CR37","first-page":"187","volume-title":"Using spin to verify security properties of cryptographic protocols","author":"P Maggi","year":"2002","unstructured":"Maggi P, Sisto R (2002) Model Checking of Software (SPIN), LNCS. In: Bosnacki D, Leue S (eds) Using spin to verify security properties of cryptographic protocols. Springer, New York, pp 187\u2013204"},{"key":"1099_CR38","unstructured":"Mitchell JC, Mitchell M, Stern U (1997) Automated analysis of cryptographic protocols using murphi. In: IEEE Symposium on Security and Privacy. IEEE Computer Society, pp 141\u2013151"},{"key":"1099_CR39","unstructured":"Orzan S, van de Pol J, Espada M (2005) A state space distributed policy based on abstract interpretation. In: ENTCS, vol 128. Elsevier, Amsterdam, pp 35\u201345"},{"issue":"1\u20132","key":"1099_CR40","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6(1\u20132):85\u2013128","journal-title":"J Comput Secur"},{"key":"1099_CR41","doi-asserted-by":"crossref","unstructured":"Petcu D (2003) Parallel explicit state reachability analysis and state space construction. In: Proceedings of ISPDC. IEEE Computer Society, pp 207\u2013214","DOI":"10.1109\/ISPDC.2003.1267665"},{"key":"1099_CR42","volume-title":"Algebras of coloured petri nets","author":"F Pommereau","year":"2010","unstructured":"Pommereau F (2010) Algebras of coloured petri nets. Lambert Academic Publisher, Germany (ISBN 978-3-8433-6113-2)"},{"issue":"2","key":"1099_CR43","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1023\/A:1008771324652","volume":"18","author":"U Stern","year":"2001","unstructured":"Stern U, Dill DL (2001) Parallelizing the murj verifier. Form Methods Syst Des 18(2):117\u2013129","journal-title":"Form Methods Syst Des"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1099-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11227-014-1099-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1099-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T14:39:30Z","timestamp":1565188770000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11227-014-1099-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,12]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["1099"],"URL":"https:\/\/doi.org\/10.1007\/s11227-014-1099-8","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,12]]}}}