Formal Verification of an Intrusion-Tolerant Group Membership Protocol

Hari Govind V. Ramasamy, Michel Cukier, William H. Sanders

Research output: Contribution to journalArticlepeer-review


The traditional approach for establishing the correctness of group communication protocols is through rigorous arguments. While this is a valid approach, the likelihood of subtle errors in the design and implementation of such complex distributed protocols is not negligible. The use of formal verification methods has been widely advocated to instill confidence in the correctness of protocols. In this paper, we describe how we used the SPIN model checker to formally verify a group membership protocol that is part of an intrusion-tolerant group communication system. We describe how we successfully tackled the state-space explosion problem by determining the right abstraction level for formally specifying the protocol. The verification exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.

Original languageEnglish (US)
Pages (from-to)2612-2622
Number of pages11
JournalIEICE Transactions on Information and Systems
Issue number12
StatePublished - Dec 2003


  • Formal methods
  • Group communication systems
  • Intrusion tolerance
  • Validation

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence


Dive into the research topics of 'Formal Verification of an Intrusion-Tolerant Group Membership Protocol'. Together they form a unique fingerprint.

Cite this