Exploring adaptability of secure group communication using formal prototyping techniques

ABSTRACT

Traditionally, adaptability in communication frameworks has been restricted to predefined choices without taking into consideration tradeoffs between them and the application requirements. Furthermore, different applications with an entire spectrum of requirements will have to adapt to these predefined choices instead of tailoring the communication framework to fit their needs. In this paper we extend an executable specification of a state-of-the-art secure group communication subsystem to explore two dimensions of adaptability, namely security and synchrony. In particular, we relax the traditional requirement of virtual synchrony (a well-known bottleneck) and propose various generic optimizations, while preserving essential security guarantees.

References

1. The Keyed-Hash Message Authentication Code (HMAC). In No. FIPS 198, National Institute for Standards and Technology, 2002.]]
2. A. Fekete, N. Lynch and A. Shvartsman. Specifying and using a Partitionable Group Communication Service. In 16th Annual ACM Symposium on Principles of Distributed Computing, 1997.]]
3. C. Talcott and M.-O. Stehr. Specification of the Group Diffie-Hellman Protocol as a Component of the Cliques Toolkit. Website: http://formal.cs.uiuc.edu/stehr/cliques_eng.html, 2003.]]
4. C. Talcott, M.-O. Stehr and G. Denker. Towards a Formal Specification of the Spread Group Communication System. Website: http://formal.cs.uiuc.edu/stehr/spread_eng.html, 2004.]]
5. J. Meseguer. Conditional Rewriting Logic as a Unified Model of Concurrency. In Theoretical Computer Science 96(1):73--155, 1992.]]
6. J. Schultz. Partitionable Virtual Synchrony Using Extended Virtual Synchrony. Master Thesis, Department of Computer Science, Johns Hopkins University, 2001.]]
7. K. P. Kihlstrom, L. E. Moser and P. M. Melliar-Smith. The SecureRing Protocols for Securing Group Communication. In IEEE 31st Hawaii International Conference on System Sciences, 1998.]]
8. L. E. Moser, Y. Amir, P. M. Melliar-Smith and D. A. Agarwal. Extended Virtual Synchrony. In 14th International Conference on Distributed Computing Systems, 1994.]]
9. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer and C. Talcott. The Maude 2.0 System. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science, pages 76--87. Springer-Verlag, June 2003.]]
10. M. K. Reiter. Secure Agreement Protocols: Reliable and Atomic Group Multicast in Rampart. In 2nd ACM Conference on Computer and Communications Security, 1994.]]
11. M. Steiner, G. Tsudik and M. Waidner. Key Agreement in Dynamic Peer Groups. In IEEE Transactions on Parallel and Distributed Systems, 2000.]]
12. O. Rodeh, K. Birman, M. Hayden, Z. Xiao and D. Dolev. Ensemble Security. Technical Report TR98--1703, Cornell University, 2000. Department of Computer Science.]]
13. P. McDaniel, A. Prakash and P. Honeyman. Antigone: A Flexible Communication for Secure Group Communication. In Proceedings of the 8th USENIX Security Symposium, 1999.]]
14. R. van Renesse, K. Birman and S. Maffeis. Horus: A Flexible Group Communication System. Communication of the ACM, 39(4):76--83, 1996.]]
15. S. Floyd, V. Jacobson, C. Liu, S. McCanne and L. Zhang. A Reliable Multicast Framework for Light-weight Session and Application Level Framing. In IEEE/ACM Transactions on Networking, (5):784--803, 1997.]]
16. Y. Amir. Replication Using Group Communication Over a Partitioned Network. Ph.D. Thesis, Hebrew University of Jerusalem, 1995.]]
17. Y. Amir and J. Stanton. The Spread Wide Area Group Communication System. Technical Report Technical Report CNDS-98-4, Johns Hopkins University, 1998.]]
18. Y. Amir, C. Nita-Rotaru, J. Stanton and G. Tsudik. Scaling Secure Group Communication Systems: Beyond Peer-to-Peer. In DARPA Information Survivability Conference and Exposition, 2003.]]
19. Y. Amir, D. Dolev, S. Kramer and D Malki. Transis: A Communication Subsystem for High Availability. In 22nd International Symposium on Fault-Tolerant Computing Systems, 1992.]]
20. Y. Amir, G. Ateniese, D. Hasse, Y. Kim, C. Nita-Rotaru, T. Schlossnagle, J. Schultz, J. Stanton and G. Tsudik. Secure Group Communication in Asynchronous Networks with Failures: Integration and Experiments. In 20th International Conference on Distributed Computing Systems, 2000.]]
21. Y. Amir, L. E. Moser, P. M. Melliar-Smith, D. Agarwal and P. Ciarfella. The Totem Single-Ring Ordering and Membership Protocol. In ACM Transactions on Computer Systems, 1995.]]
22. Y. Amir, Y. Kim, C. Nita-Rotaru, J. Schultz, J. Stanton and G. Tsudik. Secure Group Communication Using Robust Contributory Key Agreement. In IEEE Transactions on Parallel and Distributed Systems, 2004.]]
23. Y. Kim, A. Perrig and G. Tsudik. Simple and Fault-Tolerant Key Agreement for Dynamic Collaborative Groups. In ACM CCS, 2000.]]
24. Y. Kim, A. Perrig and G. Tsudik. Communication-efficient Group Key Agreement. In IFIP SEC 2001, 2001.]]