{"id":231987,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00231987","sets":["934:935:11486:11487"]},"path":["11487"],"owner":"44499","recid":"231987","title":["Rabbit: A Modeling Language for Verifying Data-flow Security"],"pubdate":{"attribute_name":"公開日","attribute_value":"2024-01-31"},"_buckets":{"deposit":"68ad57cc-50bb-472c-8bad-f6cf4abd88ca"},"_deposit":{"id":"231987","pid":{"type":"depid","value":"231987","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Rabbit: A Modeling Language for Verifying Data-flow Security","author_link":["627596","627589","627593","627590","627595","627592","627591","627594"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Rabbit: A Modeling Language for Verifying Data-flow Security"},{"subitem_title":"Rabbit: A Modeling Language for Verifying Data-flow Security","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[発表概要, Unrefereed Presentatin Abstract] ","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2024-01-31","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"School of Informatics, Kyoto University"},{"subitem_text_value":"National Institute of Informatics"},{"subitem_text_value":"School of Informatics, Kyoto University"},{"subitem_text_value":"National Institute of Informatics"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"School of Informatics, Kyoto University","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics","subitem_text_language":"en"},{"subitem_text_value":"School of Informatics, Kyoto University","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/231987/files/IPSJ-TPRO1701003.pdf","label":"IPSJ-TPRO1701003.pdf"},"date":[{"dateType":"Available","dateValue":"2026-01-31"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO1701003.pdf","filesize":[{"value":"30.1 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"fb52f879-969e-47aa-bcb1-04ec2e509a21","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2024 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Terunobu, Inaba"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Taro, Sekiyama"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Atsushi, Igarashi"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yutaka, Ishikawa"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Terunobu, Inaba","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Taro, Sekiyama","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Atsushi, Igarashi","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yutaka, Ishikawa","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"In systems with high-security requirements such as IoT systems, it is desired to confirm that security requirements are met via formal verification. However, verification often has notations that are largely different from those of general-purpose programming languages. In this presentation, we propose a modeling language called Rabbit, which has both simplicity and an ability of security verification on data flow. In Rabbit, systems are modeled as a parallel process, together with security assumptions, i.e., which variables and communication channels are eavesdropped or tampered. Given a model and security requirements, such as secrecy and integrity, Rabbit verifies whether the model meets the requirements. The verification part is performed by Tamarin Prover, a powerful verification tool for security protocols. The system model in Rabbit is translated into a Tamarin model, and then symbolic model checking is conducted. We implemented a translator from Rabbit to Tamarin Prover. To mitigate computational complexity in the model checking part, we experiment with different translation strategies. We confirmed that Rabbit is sufficiently expressive and the verification via Tamarin Prover finishes in reasonable time in several case studies.","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"In systems with high-security requirements such as IoT systems, it is desired to confirm that security requirements are met via formal verification. However, verification often has notations that are largely different from those of general-purpose programming languages. In this presentation, we propose a modeling language called Rabbit, which has both simplicity and an ability of security verification on data flow. In Rabbit, systems are modeled as a parallel process, together with security assumptions, i.e., which variables and communication channels are eavesdropped or tampered. Given a model and security requirements, such as secrecy and integrity, Rabbit verifies whether the model meets the requirements. The verification part is performed by Tamarin Prover, a powerful verification tool for security protocols. The system model in Rabbit is translated into a Tamarin model, and then symbolic model checking is conducted. We implemented a translator from Rabbit to Tamarin Prover. To mitigate computational complexity in the model checking part, we experiment with different translation strategies. We confirmed that Rabbit is sufficiently expressive and the verification via Tamarin Prover finishes in reasonable time in several case studies.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"12","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"12","bibliographicIssueDates":{"bibliographicIssueDate":"2024-01-31","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"1","bibliographicVolumeNumber":"17"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"updated":"2025-01-19T10:34:37.710911+00:00","created":"2025-01-19T01:32:35.085598+00:00","links":{}}