We define the basic concepts for modular, layered design: protocols, systems, configurations, executions, and models, and three relations: indistinguishability (between two systems), satisfaction (of a model by a system), and realization (by protocol, of one model over another model). We prove several basic properties, including the {\em layering lemma} and the {\em indistinguishability lemma}. The indistinguishability lemma shows that if two systems \Gamma_L, \Gamma_R are indistinguishable, and \Gamma_L satisfies some model M, then \Gamma_R also satisfies M. The layering lemma shows that given protocols {\pi_i}^u_{i=1}, if every protocol \pi_i realizes model M_i over model M_{i-1}, then the composite protocol \pi_{1||...||u} realizes model M_u over M_0. This allows specification, design and analysis of each layer independently, and combining the results to ensure properties of the complete system.
Our framework is based on {\em games}, following many works in applied cryptography. This differs from existing frameworks allowing compositions of cryptographic protocols, based on {\em simulatability of ideal functionality}. Game-based models are more general and flexible than ideal functionality specifications, supporting different adversarial models and avoiding over-specification, which is essential for practical distributed systems and networks.
Category / Keywords: foundations / Layered specifications, secure e-commerce layers, composability. Publication Info: This is draft of full version; extended abstract (with some errors) will appear in proc. of TCC'08. Date: received 8 Nov 2006, last revised 22 Jun 2008 Contact author: amir herzberg at gmail com Available formats: PDF | BibTeX Citation Note: This is draft of full version; extended abstract (with some errors) will appear in proc. of TCC'08. Version: 20080622:140011 (All versions of this report) Discussion forum: Show discussion | Start new discussion