This paper introduces Expi2Java, a new code generator for cryptographic protocols that translates models written in an extensible variant of the Spi calculus into executable code in a substantial fragment of Java, featuring concurrency, synchronization between threads, exception handling and a sophisticated type system with generics and wildcards. Our code generator is highly extensible and customizable, which allows it to generate interoperable

In this paper we present a new technique for automatically verifying typing constraints in the setting of Dminor, a first-order data processing language with refinement types and dynamic type-tests. We achieve this by translating Dminor programs into a standard while language and then using a general-purpose verification tool. Our translation generates assertions in the while program that faithfully represent the sophisticated typing constraints

We present a new type system for verifying the security of cryptographic protocol implementations. 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 protocol implementations.