| Most protocol analyses only address security properties. However, other properties are important and can increase our understanding of protocols, as well as aid in the deployment and compilation of implementations. We investigate such analyses.;Unfortunately, existing high-level protocol implementation languages do not accept programs that match the style used by the protocol design community. These languages are designed to implement protocol roles independently, not whole protocols. Therefore, a different program must be written for each role. We define a language, WPPL, that avoids this problem. It avoids the need to create a new tool-chain, however, by compiling protocol descriptions into an existing, standard role-based protocol implementation language.;Next, we investigate two families of analyses. The first reveals the implicit design decisions of the protocol designer and enables fault-tolerance in implementations. The second characterizes the infinite space of all messages a protocol role could accept and enables scalability by determining the session state necessary to support concurrency.;Our entire work is formalized in a mechanical proof checker, the Coq proof assistant, to ensure its theoretical reliability. Our implementations are automatically extracted from the formal Coq theory, so they are guaranteed to implement the theory. |
