Towards Adaptive Secure Group Communication

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.  We extend an executable specification of a state-of-the-art secure group communication subsystem to explore several dimensions of adaptability (synchrony, security, mobility, reliability, timeliness) and propose various generic optimizations, while preserving essential security guarantees.

The general methodology we employ for system design and analysis is based on an executable specification language called Maude (see Maude web page ). Its theoretical foundation is rewriting logic, a logic with an operational as well as a model-theoretic semantics. Formal prototyping is a key ingredient of our methodology, which allows us to experiment with a abstract mathematical but executable specification of the system early in the design phase. Our experience indicates that the combination of mathematical rigor with execution and analysis tools such as Maude leads to better understanding of the system and often pinpoints potential problems. To employ this methodology in the exploration of adaptive secure group communication, we build upon abstract executable specifications of all relevant components of Secure Spread (see Towards a Formal Specification of the Spread Group Communication System web page ).

Relevant References:

1. M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer and C. Talcott: The Maude 2.0 System.  In Robert Nieuwenhuis, editor, Rewriting Techniques and Aplications, volume 2706 in Lecture Notes in Computer Science, pp. 76-87. Springer-Verlag, 2003. Available here[ pdf ].
   
2. J. Meseguer: Conditional Rewriting Logic as a Unified Model of Concurrency. In Theoretical Computer Science 96(1):73-155. 1992. [ ACM Digital Library ].
   
3. Y. Amir, Y. Kim, C. Nita-Rotaru, J. Schultz, J. Stanton, G. Tsudik: Secure Group Communication Using Robust Contributory Key Agreement.  IEEE Transactions on Parallel and Distributed Systems archive, pp. 468 - 480, 15(5). IEEE Press, 2004. Available here [ pdf ].
4. S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, and C. Talcott: Exploring Adaptability of Secure Group Communication using Formal Prototyping Techniques. 3rd Workshop on Adaptive and Reflective Middleware, Middleware 2004. Available here [ pdf ].
5. S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, and C. Talcott: Towards Adaptive Secure Group Communication: Bridging the Gap between Formal Specification and Network Simulation. 12th IEEE International Symposium on Pacific Rim Dependable Computing, 2006 . Available here [ pdf ]. 
6. S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, and C. Talcott: Relaxing Consistency in Group Communication for Mobile Networks. Available here [ pdf ].

Presentations:

1. Secure Group Communication: Exploring Adaptability using Formal Prototyping Techniques. ONR-MURI PI Meeting. June 7-8, 2004. Slides available here [ pdf ].
   
2. A Formal Methods Approach to Adaptive Secure Group Communication. ONR-MURI Review Meeting, November 18-19, 2004. Slides available here [ pdf ].
3. Towards Adaptive Secure Group Communication. PRDC'06, December, 2006. Slides available here [ pdf ].

The current state of our specification is available below, but please note that it is a snapshot of ongoing work and still incomplete regarding various aspects.

The Formal Specification in Maude 2.0 (available here ) can be found here .
This package contains the following files:

• README :  instructions on how to run the examples

• Common data types and operations
  

natutil.maude	natural numbers and operations
proc.maude	processes (server daemons)
agent.maude	agents (potential clients)
group.maude	logical groups
state.maude	distributed system state
mode.maude	message delivery modes

• Configuration layer
  

conf.maude	configurations (instances of process membership in connected components)
cmessage.maude	configuration layer messages
constraints.maude	delivery contraints
capi.maude	configuration level API
ccommon.maude	common for the following two modes
coperational.maude	normal operational mode
cchange.maude	transitional mode
cspread.maude	combined configuration layer specification

• Group layer
  

view.maude	views (instances of agent membership)
gmessage.maude	group layer messages
gapi.maude	group layer API
spread.maude	combined group layer specification

• Flush layer
  

fmessage.maude	flush layer messages
fapi.maude	flush layer API
flushspread.maude	combined flush layer specification

• Secure layer
  

cliques.maude	Cliques toolkit specification
smessage.maude	secure layer message
sapi.maude	secure layer API
groupvar.maude	group specific variables
assockey.maude	history of keys indexed by keyid
assocmembset.maude	history of keys indexed by  membership
securespread.maude	combined secure layer specification

• Load all layers
  

all.maude

Load all layers

• Controller
  

controller.maude	a simple controller language
test.maude	prelude for configuration layer testing
gtest.maude	prelude for group layer testing
ftest.maude	prelude for flush layer testing
stest.maude	prelude for secure layer testing

• Examples: 

stestvs1.maude (blocking)	R: stestvs1.out
stestvs2.maude (non-blocking)	R: stestvs2.out
stestevs1.maude (eager)	R: stestevs1.out
stestevs2.maude (changing-time)	R: stestevs2.out
stestevs3.maude (sending-time)	R: stestevs3.out
stestevs4.maude (combined-sct)	R: stestevs4.out
stestevs5.maude (req-sending-view)	R: stestevs5.out
stestevs6.maude (crash example 1)	R: stestevs6.out