Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms

Samuel Judson, Ning Luo, Timos Antonopoulos, Ruzica Piskac

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Model checking is the problem of verifying whether an abstract model M of a computational system meets a specification of behavior ø. We apply the cryptographic theory of secure multiparty computation (MPC) to model checking. With our construction, adversarial parties D and A holding M and ø respectively may check satisfaction-notationally, whether M |= ø-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.

Original languageEnglish (US)
Title of host publicationWPES 2020 - Proceedings of the 19th Workshop on Privacy in the Electronic Society
PublisherAssociation for Computing Machinery
Pages101-115
Number of pages15
ISBN (Electronic)9781450380867
DOIs
StatePublished - Nov 9 2020
Externally publishedYes
Event19th 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 - Virtual, Online, United States
Duration: Nov 9 2020 → …

Publication series

NameWPES 2020 - Proceedings of the 19th Workshop on Privacy in the Electronic Society

Conference

Conference19th 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
Country/TerritoryUnited States
CityVirtual, Online
Period11/9/20 → …

Keywords

  • cryptography
  • model checking
  • multiparty computation
  • privacy
  • temporal logic
  • verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms'. Together they form a unique fingerprint.

Cite this