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.
- 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.
Download Coq formalization of our calculus, type system and soundness proof by Cătălin Hriţcu. Works with Coq 8.2.
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)
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@….