{"_buckets": {"deposit": "5417adc3-a7f2-472f-a46c-b2afee185c65"}, "_deposit": {"id": "11442", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "11442"}, "status": "published"}, "_oai": {"id": "oai:soar-ir.repo.nii.ac.jp:00011442"}, "item_6_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2013-08", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "4", "bibliographicPageEnd": "48", "bibliographicPageStart": "37", "bibliographicVolumeNumber": "2", "bibliographic_titles": [{"bibliographic_title": "Artificial Intelligence Research"}]}]}, "item_6_description_20": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "Security proofs for cryptographic systems are very important. The ultimate objective of our study is to prove the security of cryptographic systems using the Mizar proof checker. In this study, we formalize the probability on a finite and discrete sample space to achieve our aim. Therefore, we introduce a formalization of the probability distribution and prove the correctness of the formalization using the Mizar proof checking system as a formal verification tool.", "subitem_description_type": "Abstract"}]}, "item_6_description_30": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7\uff08\u30b3\u30f3\u30c6\u30f3\u30c4\u306e\u7a2e\u985e\uff09", "attribute_value_mlt": [{"subitem_description": "Article", "subitem_description_type": "Other"}]}, "item_6_description_5": {"attribute_name": "\u5f15\u7528", "attribute_value_mlt": [{"subitem_description": "Artificial Intelligence Research. 2(4):37-48 (2013)", "subitem_description_type": "Other"}]}, "item_6_link_3": {"attribute_name": "\u4fe1\u5dde\u5927\u5b66\u7814\u7a76\u8005\u7dcf\u89a7\u3078\u306e\u30ea\u30f3\u30af", "attribute_value_mlt": [{"subitem_link_text": "Okazaki, Hiroyuki", "subitem_link_url": "http://soar-rd.shinshu-u.ac.jp/profile/ja.geDNbpkh.html"}, {"subitem_link_text": "Shidama, Yasunari", "subitem_link_url": "http://soar-rd.shinshu-u.ac.jp/profile/ja.OeceZVkh.html"}]}, "item_6_publisher_4": {"attribute_name": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "Sciedu Press"}]}, "item_6_relation_48": {"attribute_name": "DOI", "attribute_value_mlt": [{"subitem_relation_name": [{"subitem_relation_name_text": "10.5430/air.v2n4p37"}], "subitem_relation_type_id": {"subitem_relation_type_id_text": "http://dx.doi.org/10.5430/air.v2n4p37", "subitem_relation_type_select": "DOI"}}]}, "item_6_rights_62": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "This work is licensed under a Creative Commons Attribution 3.0 License."}]}, "item_6_select_64": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_6_source_id_35": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "1927-6974", "subitem_source_identifier_type": "ISSN"}]}, "item_6_source_id_39": {"attribute_name": "NII ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "1927-6974", "subitem_source_identifier_type": "ISSN"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Okazaki,  Hiroyuki"}], "nameIdentifiers": [{"nameIdentifier": "35545", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Futa,  Yuichi"}], "nameIdentifiers": [{"nameIdentifier": "35546", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Shidama,  Yasunari"}], "nameIdentifiers": [{"nameIdentifier": "35547", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2015-09-28"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "Formal_definition_probability_finite_discrete_sample.pdf", "filesize": [{"value": "127.4 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 127400.0, "url": {"label": "Formal_definition_probability_finite_discrete_sample.pdf", "url": "https://soar-ir.repo.nii.ac.jp/record/11442/files/Formal_definition_probability_finite_discrete_sample.pdf"}, "version_id": "14cfd520-4283-42bc-ab57-ddd16735695a"}]}, "item_keyword": {"attribute_name": "\u30ad\u30fc\u30ef\u30fc\u30c9", "attribute_value_mlt": [{"subitem_subject": "Formal verification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Probability on a finite and discrete sample space", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Cryptographic system", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar"}]}, "item_type_id": "6", "owner": "1", "path": ["1162/1163"], "permalink_uri": "http://hdl.handle.net/10091/17168", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_name_i18n": "\u516c\u958b\u65e5", "attribute_value": "2013-09-19"}, "publish_date": "2013-09-19", "publish_status": "0", "recid": "11442", "relation": {}, "relation_version_is_last": true, "title": ["Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar"], "weko_shared_id": null}