Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations (bibtex)
by Michael Backes, Catalin Hritcu, Matteo Maffei
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.
Reference:
Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations (Michael Backes, Catalin Hritcu, Matteo Maffei), In Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security, IOS Press, volume 22, 2014.
Bibtex Entry:
@article{Backes:Hritcu:Maffei:14jcs,
  author = {Michael Backes and
            Catalin Hritcu and
            Matteo Maffei},
  title = {Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations},
  journal = {Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security},
  volume = {22},
  number = {2},
  pages = {301--353},
  publisher = {IOS Press},
  month = feb,
  year = 2014,
  doi = {10.3233/JCS-130493},
  ee = {http://iospress.metapress.com/content/G0531100122U1K6K},
  url = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/rcf-and-or-coq-jcs2014.pdf},
  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.},
}
Powered by bibtexbrowser