文献

J-GLOBAL ID：202202247115750716   整理番号：22A0578839

位置ベースサービスシステムにおけるプライバシー保護プロトコルのためのプロセス計算【JST・京大機械翻訳】

A process calculus for privacy-preserving protocols in location-based service systems

著者 (2件)： Bavendiek Kai (Hamburg University of Technology, Institute for Software Systems, Am Schwarzenberg Campus 3, 21073 Hamburg, Germany) ,  Schupp Sibylle (Hamburg University of Technology, Institute for Software Systems, Am Schwarzenberg Campus 3, 21073 Hamburg, Germany)
資料名： Journal of Logical and Algebraic Methods in Programming  (Journal of Logical and Algebraic Methods in Programming)
巻： 125  ページ： Null  発行年： 2022年 
JST資料番号： W1593A  ISSN： 2352-2208  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 位置ベースサービス(LBS)のユーザを漏洩個人データのプライバシー脅威から保護するために,位置プライバシー保護機構(LPPM)を導入した。これらの機構は,悪意のあるパーティーが敏感な個人データを引き出すことができないような方法で,LBSへの通信を変化させる。文献では,様々なプライバシー保証を持つ多くの異なるLPPMを見つけることができるが,これらのメカニズムとそれらのプライバシー保証の全てを比較するための形式的フレームワークは存在していない。LPPMと位置プライバシー保証のモデリングを可能にするσ-計算を提案した。この計算は,プロセス言語,特性言語,およびプロセスモデル上の位置プライバシー特性の検証を可能にする時間-K-レス-エピステリックモーダル論理を必要とする。σ-calculusは,計算的に安価であるが,LBS通信におけるプライバシー違反のモデリングに充分である標準集合演算に基づく,新しいプロセス計算である。計算は,LPPMsの幅広いアレイのモデルおよび理由に対する最初の形式的フレームワークであり,位置プライバシー特性の自動検証を可能にするモデル検査アルゴリズムを提示する。位置プライバシー特性のベンチマーク集合を記述することにより,文献からの多数のLPPMと筆者らの特性言語の表現性をモデル化することにより,著者らのプロセス言語の表現性を評価した。さらに,LPPMアルゴリズム設計者の拡張例によるプライバシー特性の検証を示した。モデル検査アルゴリズムを実装するツールLP3Verifを開発した。オープンソースツールはJavaで書かれ,バックエンドとしてSMTソルバCVC4を使用する。Copyright 2022 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  言語 ,  *保護 ,  *プライバシー ,  通信 ,  *プロトコル ,  利用者 ,  ベンチマーク ,  モデル検査 ,  Java ,  フレームワーク【ソフトウェア開発】
準シソーラス用語： 表現力 ,  ソルバ ,  *プライバシー保護 ,  低価格 ,  オープンソース , 【Automatic Indexing@JST】

著者キーワード (5件)： プロセス計算 ,  時間認識様相論理 ,  モデル検査 ,  位置プライバシー保護機構 ,  位置ベースサービス

分類 (2件)： データ保護  (JD01020V) ,  移動通信  (ND08030H)

タイトルに関連する用語 (5件)： サービス ,  プライバシー ,  プロトコル ,  プロセス ,  計算