F5 Toolchain for RCF

F5 is a toolchain for Refined Concurrent FPC (RCF) including a type-checker with union, intersection, and polymorphic types, as well as static reasoning about type disjointness, and a user-friendly GUI for examining typing derivations; an automatic code generator for symbolic implementations of zero-knowledge; a visual debugger, and more.

Papers

• Michael Backes, Cătălin Hriţcu, and Matteo Maffei.  Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations, Submitted to special issue of the  Journal of Computer Security (JCS) for TOSCA-SecCo?, January 16, 2012.

• Michael Backes, Cătălin Hriţcu, Matteo Maffei.  Union and Intersection Types for Secure Protocol Implementations. Invited paper in  Theory of Security and Applications (TOSCA'11), February 2011.

Formalization

Download Coq formalization of our calculus, type system and soundness proof by Cătălin Hriţcu. Works with Coq 8.2.

•  Preliminary release 2010-12-26 (tar.gz 4.6 MB)
•  Preliminary release 2011-02-06 (tar.gz 4.9 MB)

Implementation

Download F5 tool-chain for RCF by Thorsten Tarrach and Cătălin Hriţcu  Apache License, Version 2.0.

•  Preliminary release 2010-11-22 (zip containing Windows binaries, symbolic cryptographic library and samples; 3.1MB) (README)

Screenshots

Bug Tracker

Because of a recent spam wave you need to be logged-in to create new tickets. If you need an account or want to report a bug directly please contact catalin.hritcu@….