Cryptographic Protocols From Goal-Driven Specifications
We present G2C, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from how the intended functionality is achieved, but instead lets the system designer concentrate on which functional features and security properties should be achieved. Our framework provides a compilation method for transforming G2C specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a G2C compiler to demonstrate the feasibility of our approach.
High-level AbstractionsDesigning cryptographic protocols is tremendously difficult and error-prone. Protocol designers struggle to keep pace with the variety of possible security vulnerabilities, which have affected early authentication protocols such as the Needham-Schroeder protocol, carefully designed de facto standards like SSL and PKCS, and even widely deployed products such as Microsoft Passport and Kerberos. The task of designing cryptographic protocols is made more and more challenging by the dimension and complexity of modern distributed architectures (e.g., collaborative platforms, content sharing applications, social networks) and the number of security properties that have to be simultaneously fulfilled (e.g., user anonymity, access control, secrecy, and authentication). There are only few suitable guidelines or automated tools to assist system designers and, at present, the development of cryptographic protocols is mostly carried out by relying on common practice and on the creativity and experience of designers, rather than on rigorous and formal design techniques.
Recent research has started to address this problem by providing techniques to compile high-level protocol specifications into concrete cryptographic protocols or to strengthen existing cryptographic protocols and make them resistant to sophisticated threat models. These approaches, however, take as input a detailed specification of the structural aspects of the protocol: one has to describe in depth which messages are exchanged between which participants and, in some cases, even which cryptographic primitives are used. In general, these techniques require expert knowledge in current security research and, arguably, they are hardly accessible to system designers. Ideally, designers should be required to solely state in a simple, yet precise, manner which functionality should be realized and which security properties should be guaranteed, without necessarily having to think how this can be achieved.
Towards a Formal SemanticsJan Balzer has extended G2C: Zero-knowledge proofs have been added to guarantee the correctness of computations, even if these are carried out by compromised participants.
The extension includes new syntactic constructs for the goal-driven language G2C, a type system as semantic backbone, and an automated derivation method for symbolic zero-knowledge proofs. The protocols generated by the extended G2C compiler are validated using ProVerif with an equational theory for non-interactive zero-knowledge proofs.