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

Model checking
Viruses
Managers
Statistical Models

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

Formal analysis of fault-tolerant group key management using ZooKeeper. / Skeirik, Stephen; Bobba, Rakesh B.; Meseguer, Jose.

2013. 636-641 Paper presented at 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands.

Research output: Contribution to conferencePaper

Skeirik, S, Bobba, RB & Meseguer, J 2013, 'Formal analysis of fault-tolerant group key management using ZooKeeper' Paper presented at 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands, 5/13/13 - 5/16/13, pp. 636-641. https://doi.org/10.1109/CCGrid.2013.98
Skeirik S, Bobba RB, Meseguer J. Formal analysis of fault-tolerant group key management using ZooKeeper. 2013. 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
Skeirik, Stephen ; Bobba, Rakesh B. ; Meseguer, Jose. / Formal analysis of fault-tolerant group key management using ZooKeeper. Paper presented at 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands.6 p.
@conference{92c7adba7a8a444eb28783c86ed319a3,
title = "Formal analysis of fault-tolerant group key management using ZooKeeper",
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.",
keywords = "Formal verification, Group key management, Maude, Security-as-a-Service",
author = "Stephen Skeirik and Bobba, {Rakesh B.} and Jose Meseguer",
year = "2013",
month = "8",
day = "14",
doi = "10.1109/CCGrid.2013.98",
language = "English (US)",
pages = "636--641",
note = "13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013 ; Conference date: 13-05-2013 Through 16-05-2013",

}

TY - CONF

T1 - Formal analysis of fault-tolerant group key management using ZooKeeper

AU - Skeirik, Stephen

AU - Bobba, Rakesh B.

AU - Meseguer, Jose

PY - 2013/8/14

Y1 - 2013/8/14

N2 - 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.

AB - 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.

KW - Formal verification

KW - Group key management

KW - Maude

KW - Security-as-a-Service

UR - http://www.scopus.com/inward/record.url?scp=84881308224&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84881308224&partnerID=8YFLogxK

U2 - 10.1109/CCGrid.2013.98

DO - 10.1109/CCGrid.2013.98

M3 - Paper

AN - SCOPUS:84881308224

SP - 636

EP - 641

ER -