{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:41:49Z","timestamp":1759333309266,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131844"},{"type":"electronic","value":"9783031131851"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct <jats:italic>oblivious online monitoring<\/jats:italic>\u2014online monitoring conducted without revealing the private information of each party to the other\u2014against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on <jats:italic>fully homomorphic encryption (FHE)<\/jats:italic>, we propose two online algorithms (<jats:sc>Reverse<\/jats:sc> and <jats:sc>Block<\/jats:sc>) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol\u2019s practical relevance.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_22","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"447-468","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Oblivious Online Monitoring for\u00a0Safety LTL Specification via\u00a0Fully Homomorphic Encryption"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8610-9186","authenticated-orcid":false,"given":"Ryotaro","family":"Banno","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6642-1276","authenticated-orcid":false,"given":"Kotaro","family":"Matsuoka","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4497-3459","authenticated-orcid":false,"given":"Naoki","family":"Matsumoto","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0467-6203","authenticated-orcid":false,"given":"Song","family":"Bian","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9360-7490","authenticated-orcid":false,"given":"Masaki","family":"Waga","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abbas, H.: Private runtime verification: work-in-progress. In: EMSOFT 2019, p. 11. ACM (2019)","DOI":"10.1145\/3349568.3351552"},{"issue":"1","key":"22_CR2","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/S0019-9958(81)90090-5","volume":"51","author":"D Angluin","year":"1981","unstructured":"Angluin, D.: A note on the number of queries needed to identify regular languages. Inf. Control 51(1), 76\u201387 (1981)","journal-title":"Inf. Control"},{"issue":"15","key":"22_CR3","doi-asserted-by":"publisher","first-page":"2787","DOI":"10.1016\/j.comnet.2010.05.010","volume":"54","author":"L Atzori","year":"2010","unstructured":"Atzori, L., Iera, A., Morabito, G.: The internet of things: a survey. Comput. Netw. 54(15), 2787\u20132805 (2010)","journal-title":"Comput. Netw."},{"key":"22_CR4","unstructured":"Banno, R., Matsuoka, K., Matsumoto, N., Bian, S., Waga, M., Suenaga, K.: Oblivious online monitoring for safety LTL specification via fully homomorphic encryption (extended version). https:\/\/www.fos.kuis.kyoto-u.ac.jp\/~banno\/cav22.pdf"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"22_CR7","unstructured":"Bellare, M., Rogaway, P.: Introduction to Modern Cryptography. UCSD CSE, vol. 207, p. 207 (2005)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Bing, K., Fu, L., Zhuo, Y., Yanlei, L.: Design of an internet of things-based smart home system. In: ICICIP 2011, vol. 2, pp. 921\u2013924. IEEE (2011)","DOI":"10.1109\/ICICIP.2011.6008384"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-13739-6_4","volume-title":"Data and Applications Security and Privacy XXIV","author":"M Blanton","year":"2010","unstructured":"Blanton, M., Aliasgari, M.: Secure outsourcing of DNA searching via finite automata. In: Foresti, S., Jajodia, S. (eds.) DBSec 2010. LNCS, vol. 6166, pp. 49\u201364. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13739-6_4"},{"key":"22_CR10","unstructured":"Brakerski, Z., D\u00f6ttling, N., Garg, S., Malavolta, G.: Factoring and pairings are not necessary for IO: circular-secure LWE suffices. IACR Cryptology ePrint Archive, p. 1024 (2020)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Brakerski, Z., Gentry, C., Vaikuntanathan, V.: (leveled) Fully homomorphic encryption without bootstrapping. In: Goldwasser, S. (ed.) ITCS 2012, pp. 309\u2013325. ACM (2012)","DOI":"10.1145\/2090236.2090262"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23820-3_1","volume-title":"Runtime Verification","author":"F Cameron","year":"2015","unstructured":"Cameron, F., Fainekos, G., Maahs, D.M., Sankaranarayanan, S.: Towards a verified artificial pancreas: challenges and solutions for runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 3\u201317. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_1"},{"issue":"1","key":"22_CR13","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s00145-019-09319-x","volume":"33","author":"I Chillotti","year":"2020","unstructured":"Chillotti, I., Gama, N., Georgieva, M., Izabach\u00e8ne, M.: TFHE: fast fully homomorphic encryption over the torus. J. Cryptol. 33(1), 34\u201391 (2020)","journal-title":"J. Cryptol."},{"key":"22_CR14","unstructured":"Daemen, J., Rijmen, V.: AES proposal: Rijndael (1999)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Stasio, A.D., Fuggitti, F., Rubin, S.: Pure-past linear temporal and dynamic logic on finite traces. In: Bessiere, C. (ed.) IJCAI 2020, pp. 4959\u20134965 (2020)","DOI":"10.24963\/ijcai.2020\/690"},{"issue":"3","key":"22_CR16","doi-asserted-by":"publisher","first-page":"156","DOI":"10.4258\/hir.2016.22.3.156","volume":"22","author":"DV Dimitrov","year":"2016","unstructured":"Dimitrov, D.V.: Medical internet of things and big data in healthcare. Healthc. Inform. Res. 22(3), 156\u2013163 (2016)","journal-title":"Healthc. Inform. Res."},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-03769-7_13","volume-title":"Runtime Verification","author":"A El-Hokayem","year":"2018","unstructured":"El-Hokayem, A., Falcone, Y.: Bringing runtime verification home. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 222\u2013240. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_13"},{"key":"22_CR19","unstructured":"Fan, J., Vercauteren, F.: Somewhat practical fully homomorphic encryption. IACR Cryptology ePrint Archive, p. 144 (2012)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-03007-9_6","volume-title":"Data and Applications Security XXIII","author":"KB Frikken","year":"2009","unstructured":"Frikken, K.B.: Practical private DNA string searching and matching through efficient oblivious automata evaluation. In: Gudes, E., Vaidya, J. (eds.) DBSec 2009. LNCS, vol. 5645, pp. 81\u201394. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03007-9_6"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Gay, R., Pass, R.: Indistinguishability obfuscation from circular security. IACR Cryptology ePrint Archive, p. 1010 (2020)","DOI":"10.1145\/3406325.3451070"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-13013-7_20","volume-title":"Public Key Cryptography \u2013 PKC 2010","author":"R Gennaro","year":"2010","unstructured":"Gennaro, R., Hazay, C., Sorensen, J.S.: Text search protocols with simulation based security. In: Nguyen, P.Q., Pointcheval, D. (eds.) PKC 2010. LNCS, vol. 6056, pp. 332\u2013350. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13013-7_20"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Gentry, C.: Fully homomorphic encryption using ideal lattices. In: Mitzenmacher, M. (ed.) STOC 2009, pp. 169\u2013178. ACM (2009)","DOI":"10.1145\/1536414.1536440"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-40041-4_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2013","author":"C Gentry","year":"2013","unstructured":"Gentry, C., Sahai, A., Waters, B.: Homomorphic encryption from learning with errors: conceptually-simpler, asymptotically-faster, attribute-based. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013. LNCS, vol. 8042, pp. 75\u201392. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40041-4_5"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-540-70936-7_31","volume-title":"Theory of Cryptography","author":"Y Ishai","year":"2007","unstructured":"Ishai, Y., Paskin, A.: Evaluating branching programs on encrypted data. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 575\u2013594. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70936-7_31"},{"issue":"3","key":"22_CR26","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) ASE 2015, pp. 81\u201392. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.71"},{"key":"22_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"1","key":"22_CR29","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1177\/1932296813514502","volume":"8","author":"CD Man","year":"2014","unstructured":"Man, C.D., Micheletto, F., Lv, D., Breton, M., Kovatchev, B., Cobelli, C.: The UVA\/PADOVA type 1 diabetes simulator: new features. J. Diabetes Sci. Technol. 8(1), 26\u201334 (2014)","journal-title":"J. Diabetes Sci. Technol."},{"key":"22_CR30","unstructured":"Matsuoka, K., Banno, R., Matsumoto, N., Sato, T., Bian, S.: Virtual secure platform: a five-stage pipeline processor over TFHE. In: Bailey, M., Greenstadt, R. (eds.) USENIX Security 2021, pp. 4007\u20134024. USENIX Association (2021)"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-27954-6_25","volume-title":"Topics in Cryptology \u2013 CT-RSA 2012","author":"P Mohassel","year":"2012","unstructured":"Mohassel, P., Niksefat, S., Sadeghian, S., Sadeghiyan, B.: An efficient protocol for oblivious DFA evaluation and applications. In: Dunkelman, O. (ed.) CT-RSA 2012. LNCS, vol. 7178, pp. 398\u2013415. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27954-6_25"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies. (AM-34), pp. 129\u2013154. Princeton University Press, Princeton (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Regev, O.: On lattices, learning with errors, random linear codes, and cryptography. J. ACM 56(6), 34:1\u201334:40 (2009)","DOI":"10.1145\/1568318.1568324"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Sasakawa, H., Harada, H., duVerle, D., Arimura, H., Tsuda, K., Sakuma, J.: Oblivious evaluation of non-deterministic finite automata with application to privacy-preserving virus genome detection. In: Ahn, G., Datta, A. (eds.) WPES 2014, pp. 21\u201330. ACM (2014)","DOI":"10.1145\/2665943.2665954"},{"issue":"3","key":"22_CR36","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for systemC. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Troncoso-Pastoriza, J.R., Katzenbeisser, S., Celik, M.U.: Privacy preserving error resilient DNA searching through oblivious automata. In: Ning, P., di Vimercati, S.D.C., Syverson, P.F. (eds.) CCS 2007, pp. 519\u2013528. ACM (2007)","DOI":"10.1145\/1315245.1315309"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"Young, W., Corbett, J., Gerber, M.S., Patek, S., Feng, L.: DAMON: a data authenticity monitoring system for diabetes management. In: IoTDI 2018, pp. 25\u201336. IEEE Computer Society (2018)","DOI":"10.1109\/IoTDI.2018.00013"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:14:11Z","timestamp":1667495651000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}