Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper

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 witha central group key manager. Specifically, we analyze are writing 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.