Formal analysis of fault-tolerant group key management using ZooKeeper

Stephen Skeirik; Rakesh B. Bobba; Jose Meseguer

doi:10.1109/CCGrid.2013.98

Formal analysis of fault-tolerant group key management using ZooKeeper

Stephen Skeirik, Rakesh B. Bobba, Jose Meseguer

Research output: Contribution to conference › Paper › peer-review

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 language	English (US)
Pages	636-641
Number of pages	6
DOIs	https://doi.org/10.1109/CCGrid.2013.98
State	Published - Aug 14 2013
Event	13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013 - Delft, Netherlands Duration: May 13 2013 → May 16 2013

Other

Other	13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013
Country/Territory	Netherlands
City	Delft
Period	5/13/13 → 5/16/13

Keywords

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

ASJC Scopus subject areas

Software

Online availability

10.1109/CCGrid.2013.98

Library availability

Discover UIUC Full Text

Cite this

@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 = aug,

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

T2 - 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013

Y2 - 13 May 2013 through 16 May 2013

ER -

Formal analysis of fault-tolerant group key management using ZooKeeper

Abstract

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this