Formal analysis of fault-tolerant group key management using ZooKeeper

Stephen Skeirik, Rakesh B. Bobba, Jose Meseguer

Research output: Contribution to conferencePaper

Abstract

Security-as-a-Service (SecaaS) is gaining popularity, with cloud-based anti-spam and anti-virus leading the way. In this work we look at key management as a security service and focus on group key management with a central group key manager. Specifically, we analyze a rewriting logic model of a ZooKeeper-based group key management service specified in Maude and study its tolerance to faults and performance as it scales to service larger groups using the PVeStA statistical model checking tool.

Original languageEnglish (US)
Pages636-641
Number of pages6
DOIs
StatePublished - Aug 14 2013
Event13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013 - Delft, Netherlands
Duration: May 13 2013May 16 2013

Other

Other13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013
CountryNetherlands
CityDelft
Period5/13/135/16/13

    Fingerprint

Keywords

  • Formal verification
  • Group key management
  • Maude
  • Security-as-a-Service

ASJC Scopus subject areas

  • Software

Cite this

Skeirik, S., Bobba, R. B., & Meseguer, J. (2013). Formal analysis of fault-tolerant group key management using ZooKeeper. 636-641. Paper presented at 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands. https://doi.org/10.1109/CCGrid.2013.98