{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:44:41Z","timestamp":1750347881912},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319663340"},{"type":"electronic","value":"9783319663357"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66335-7_8","type":"book-chapter","created":{"date-parts":[[2017,8,9]],"date-time":"2017-08-09T23:53:48Z","timestamp":1502322828000},"page":"123-139","source":"Crossref","is-referenced-by-count":4,"title":["A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage"],"prefix":"10.1007","author":[{"given":"Marco","family":"Baldi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Chiaraluce","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cucchiarelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linda","family":"Senigagliesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Spalazzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Spegni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-662-44584-6_9","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109\u2013124. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-44584-6_9"},{"key":"8_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. Springer, Heidelberg (2008)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Baldi, M., Cucchiarelli, A., Senigagliesi, L., Spalazzi, L., Spegni, F.: Parametric and probabilistic model checking of confidentiality in data dispersal algorithms. In: Proceedings of HPCS 2016: International Conference on High Performance Computing and Simulation, pp. 476\u2013483 (2016)","DOI":"10.1109\/HPCSim.2016.7568373"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Baldi, M., Maturo, N., Montali, E., Chiaraluce, F.: AONT-LT: a data protection scheme for cloud and cooperative storage systems. In: Proceedings of HPCS 2014: International Conference on High Performance Computing and Simulation, pp. 566\u2013571 (2014)","DOI":"10.1109\/HPCSim.2014.6903736"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19835-9_30"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Cremers, C., Meadows, C.A.: Model checking security protocols. In: Handbook of Model Checking. Springer, Heidelberg (2017)","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"8_CR7","unstructured":"Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: Proceedings of FSTTCS 2013: The IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 24, pp. 501\u2013513 (2013)"},{"issue":"2","key":"8_CR8","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/2951860.2951873","volume":"47","author":"R Bloem","year":"2016","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability in parameterized verification. SIGACT News 47(2), 53\u201364 (2016)","journal-title":"SIGACT News"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Bowers, K.D., Juels, A., Oprea, A.: Hail: a high-availability and integrity layer for cloud storage. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, pp. 187\u2013198. ACM (2009)","DOI":"10.1145\/1653662.1653686"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Chung, J.Y., Joe-Wong, C., Ha, S., Hong, J.W.K., Chiang, M.: Cyrus: towards client-defined cloud storage. In: Proceedings of the 10th European Conference on Computer Systems, p. 17. ACM (2015)","DOI":"10.1145\/2741948.2741951"},{"issue":"5","key":"8_CR11","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-57220-1_47","volume-title":"Advances in Cryptology \u2014 AUSCRYPT \u201992","author":"Y Desmedt","year":"1993","unstructured":"Desmedt, Y.: Threshold cryptosystems. In: Seberry, J., Zheng, Y. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 1\u201314. Springer, Heidelberg (1993). doi: 10.1007\/3-540-57220-1_47"},{"issue":"2","key":"8_CR13","doi-asserted-by":"crossref","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\u2013207 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Durumeric, Z., Kasten, J., Adrian, D., Halderman, J.A., Bailey, M., Li, F., Weaver, N., Amann, J., Beekman, J., Payer, M., Paxson, V.: The matter of heartbleed. In: Proceedings of the 2014 Internet Measurement Conference, pp. 475\u2013488. ACM (2014)","DOI":"10.1145\/2663716.2663755"},{"issue":"1\u20132","key":"8_CR15","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C.A., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1\u20132), 162\u2013202 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Georgiev, M., Iyengar, S., Jana, S., Anubhai, R., Boneh, D., Shmatikov, V.: The most dangerous code in the world: validating SSL certificates in non-browser software. In: Proceedings of the ACM Conference on Computer and Communications Security, pp. 38\u201349 (2012)","DOI":"10.1145\/2382196.2382204"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-30793-5_2","volume-title":"Formal Techniques for Distributed Systems","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE-2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30793-5_2"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_47"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16612-9_11"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-662-54577-5_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Leng\u00e1l","year":"2017","unstructured":"Leng\u00e1l, O., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 499\u2013517. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_29"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1016\/j.compeleceng.2015.02.019","volume":"47","author":"G Lenzini","year":"2015","unstructured":"Lenzini, G., Mauw, S., Ouchani, S.: Security analysis of socio-technical physical systems. Comput. Electr. Eng. 47, 258\u2013274 (2015)","journal-title":"Comput. Electr. Eng."},{"issue":"3","key":"8_CR22","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/MIC.2016.45","volume":"20","author":"M Li","year":"2016","unstructured":"Li, M., Qin, C., Li, J., Lee, P.P.: CDstore: toward reliable, secure, and cost-efficient cloud storage via convergent dispersal. IEEE Internet Comp. 20(3), 45\u201353 (2016)","journal-title":"IEEE Internet Comp."},{"issue":"2","key":"8_CR23","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/s00165-014-0315-x","volume":"27","author":"Y Li","year":"2015","unstructured":"Li, Y., Pang, J.: Formalizing provable anonymity in Isabelle\/HOL. Formal Aspects Comput. 27(2), 255\u2013282 (2015)","journal-title":"Formal Aspects Comput."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Merani, M.L., Barcellona, C., Tinnirello, I.: Multi-cloud privacy preserving schemes for linear data mining. In: Proceedings of ICC 2015: IEEE International Conference on Communications, pp. 7095\u20137101 (2015)","DOI":"10.1109\/ICC.2015.7249458"},{"issue":"7","key":"8_CR25","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1007\/s00607-015-0445-x","volume":"97","author":"S Ouchani","year":"2015","unstructured":"Ouchani, S., Debbabi, M.: Specification, verification, and quantification of security in model-based systems. Computing 97(7), 691\u2013711 (2015)","journal-title":"Computing"},{"issue":"3","key":"8_CR26","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1016\/j.future.2011.11.010","volume":"29","author":"F Pagliarecci","year":"2013","unstructured":"Pagliarecci, F., Spalazzi, L., Spegni, F.: Model checking grid security. Fut. Gener. Comput. Syst. 29(3), 811\u2013827 (2013)","journal-title":"Fut. Gener. Comput. Syst."},{"key":"8_CR27","unstructured":"Panti, M., Spalazzi, L., Tacconi, S., Valenti, S.: Automatic verification of security in payment protocols for electronic commerce. In: ICEIS 2002, Proceedings of the 4th International Conference on Enterprise Information Systems, pp. 968\u2013974 (2002)"},{"key":"8_CR28","unstructured":"Pei, G., Henderson, T.: Validation of OFDM error rate model in ns-3 (2010). www.nsnam.org\/pei\/80211ofdm.pdf"},{"key":"8_CR29","unstructured":"Resch, J., Plank, J.: AONT-RS: blending security and performance in dispersed storage systems. In: Proceedings 9th FAST Conference (2011)"},{"issue":"2","key":"8_CR30","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1109\/22.120091","volume":"40","author":"SY Seidel","year":"1992","unstructured":"Seidel, S.Y., Rappaport, T.S.: 914 MHz path loss prediction models for indoor wireless communications in multifloored buildings. IEEE Trans. Microwave Theory Tech. 40(2), 202\u2013217 (1992)","journal-title":"IEEE Trans. Microwave Theory Tech."},{"issue":"11","key":"8_CR31","doi-asserted-by":"crossref","first-page":"612","DOI":"10.1145\/359168.359176","volume":"22","author":"A Shamir","year":"1979","unstructured":"Shamir, A.: How to share a secret. Commun. ACM 22(11), 612\u2013613 (1979)","journal-title":"Commun. ACM"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-319-27137-8_51","volume-title":"Algorithms and Architectures for Parallel Processing","author":"L Shen","year":"2015","unstructured":"Shen, L., Feng, S., Sun, J., Li, Z., Wang, G., Liu, X.: CloudS: a multi-cloud storage system with multi-level security. In: Wang, G., Zomaya, A., Perez, G.M., Li, K. (eds.) ICA3PP 2015. LNCS, vol. 9530, pp. 703\u2013716. Springer, Cham (2015). doi: 10.1007\/978-3-319-27137-8_51"},{"issue":"3\u20134","key":"8_CR33","doi-asserted-by":"crossref","first-page":"355","DOI":"10.3233\/JCS-2004-123-403","volume":"12","author":"V Shmatikov","year":"2004","unstructured":"Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3\u20134), 355\u2013377 (2004)","journal-title":"J. Comput. Secur."},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-12154-3_15","volume-title":"Verified Software: Theories, Tools and Experiments","author":"L Spalazzi","year":"2014","unstructured":"Spalazzi, L., Spegni, F.: Parameterized model-checking of timed systems with conjunctive guards. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 235\u2013251. Springer, Cham (2014). doi: 10.1007\/978-3-319-12154-3_15"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Strunk, A., Mosch, M., Gro\u00df, S., Tho\u00df, Y., Schill, A.: Building a flexible service architecture for user controlled hybrid clouds. In: Proceedings of the 2012 Seventh International Conference on Availability, Reliability and Security (ARES), pp. 149\u2013154. IEEE (2012)","DOI":"10.1109\/ARES.2012.47"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Tang, H., Liu, F., Shen, G., Jin, Y., Guo, C.: Unidrive: synergize multiple consumer cloud storage services. In: Proceedings of the 16th Annual Middleware Conference, pp. 137\u2013148. ACM (2015)","DOI":"10.1145\/2814576.2814729"},{"issue":"7","key":"8_CR37","doi-asserted-by":"crossref","first-page":"3414","DOI":"10.1007\/s10773-016-2969-z","volume":"55","author":"F Yang","year":"2016","unstructured":"Yang, F., Yang, G., Hao, Y.: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking. Int. J. Theor. Phys. 55(7), 3414\u20133427 (2016)","journal-title":"Int. J. Theor. Phys."}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66335-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T02:38:52Z","timestamp":1569983932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66335-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319663340","9783319663357"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66335-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}