@inproceedings{23374bc53a314c2084c0b3235b23fb0c,
title = "Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms",
abstract = "Model checking is the problem of verifying whether an abstract model M of a computational system meets a specification of behavior {\o}. We apply the cryptographic theory of secure multiparty computation (MPC) to model checking. With our construction, adversarial parties D and A holding M and {\o} respectively may check satisfaction-notationally, whether M |= {\o}-while maintaining privacy of all other meaningful information. Our protocol adopts oblivious graph algorithms to provide for secure computation of global explicit state model checking with specifications in Computation Tree Logic (CTL), and its design ameliorates the asymptotic overhead required by generic MPC schemes. We therefore introduce the problem of privacy preserving model checking (PPMC) and provide an initial step towards applicable and efficient constructions.",
keywords = "cryptography, model checking, multiparty computation, privacy, temporal logic, verification",
author = "Samuel Judson and Ning Luo and Timos Antonopoulos and Ruzica Piskac",
note = "Publisher Copyright: {\textcopyright} 2020 ACM.; 19th ACM Workshop on Privacy in the Electronic Society, WPES 2020, held in conjunction with the 27th ACM Conference on Computer and Communication Security, CCS 2020 ; Conference date: 09-11-2020",
year = "2020",
month = nov,
day = "9",
doi = "10.1145/3411497.3420212",
language = "English (US)",
series = "WPES 2020 - Proceedings of the 19th Workshop on Privacy in the Electronic Society",
publisher = "Association for Computing Machinery",
pages = "101--115",
booktitle = "WPES 2020 - Proceedings of the 19th Workshop on Privacy in the Electronic Society",
address = "United States",
}