Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations

Issue title: Foundational Aspects of Security

Guest editors: Konstantinos ChatzikokolakisGuest-Editor, Sebastian Alexander MödersheimGuest-Editor, Catuscia PalamidessiGuest-Editor and Jun PangGuest-Editor

Article type: Research Article

Authors: Backes, Michael^{a; b} | Hriţcu, Cătălin^{a; c; d; *} | Maffei, Matteo^a

Affiliations: [a] CISPA, Saarland University, Saarbrücken, Germany | [b] MPI-SWS, Saarbrücken and Kaiserslautern, Germany | [c] Inria, Paris-Rocquencourt, France | [d] University of Pennsylvania, Philadelphia, PA, USA

Correspondence: [*] Corresponding author. E-mail: catalin.hritcu@gmail.com

Abstract: We present a new type system for verifying the security of reference implementations of cryptographic protocols written in a core functional programming language. The type system combines prior work on refinement types, with union, intersection, and polymorphic types, and with the novel ability to reason statically about the disjointness of types. The increased expressivity enables the analysis of important protocol classes that were previously out of scope for the type-based analyses of reference protocol implementations. In particular, our types can statically characterize: (i) more usages of asymmetric cryptography, such as signatures of private data and encryptions of authenticated data; (ii) authenticity and integrity properties achieved by showing knowledge of secret data; (iii) applications based on zero-knowledge proofs. The type system comes with a mechanized proof of correctness and an efficient type-checker.

Keywords: Security protocols, reference implementations, zero-knowledge proofs, type systems, verification, refinement types, union types, intersection types, concurrent lambda-calculus, mechanized metatheory

DOI: 10.3233/JCS-130493

Journal: Journal of Computer Security, vol. 22, no. 2, pp. 301-353, 2014