A Theoretical Foundation for Communication Network Protocols

该研究将侧重于使用一种状态转换形式，这种形式在数学上是严格的，但对于普通工程师来说，它很容易用于分析和综合网络协议。在过去的工作中，主要研究者已经开发了通信网络协议理论的基本原理，本研究将发展广泛的理论基础，研究协议分析和综合的合理和有效的方法，并将这些方法应用于协议的设计。协议的分析将解决两种问题：逻辑属性和定量性能。逻辑属性必须与协议的功能需求有关，并由协议的可达状态和“允许的行为”决定。被形式化为逻辑属性的关注点包括安全性、进度和实时进度。仍然需要形式化的关注点包括保密性、真实性、匿名性、隐私性和可访问性。定量性能与协议的吞吐量和响应时间特征有关。将概率分布或时间界限等定量度量引入状态转换形式主义。此外，研究将包括通过改进和组合技术开发协议构建方法，以派生协议转换器和适配器，以及在不断变化的环境中维护和修改网络协议。

The research will focus on using a state transition formalism that is mathematically rigorous, yet easily accessible to the average engineer for the analysis and synthesis of network protocols. Building on past work in which the principal investigator has developed rudiments of a theory for communication network protocols, this research will develop a broad theoretical foundation, investigate sound and efficient methods for protocol analysis and synthesis, and apply these methods to the design of protocols. The analysis of protocols will address two kinds of concerns: logical properties and quantitative performance. Logical properties have to do with the functional requirements of a protocol and are determined by the reachable states and "allowed behaviors" of the protocol. The concerns formalized as logical properties include safety, progress, and real-time progress. Concerns that still need to be formalized included secrecy, authenticity, anonymity, privacy, and accessibility. Quantitative performance has to do with the throughput and response time characteristics of a protocol. Quantitative measures such as probability distributions or time bounds will be introduced into the state transition formalism. In addition, the research will include the development of methods for protocol construction by refinement and composition techniques for deriving protocol converters and adapters, as well as for maintaining and modifying network protocols in a changing environment.