Cryptol: The Language of Cryptography
This project contains various supporting libraries for lean to reason about protocols.
Presentation slides and examples for the SAW workshop at StrangeLoop 2017
Convert regular expressions into efficient matrix branching programs
Crucible is a library for symbolic simulation of imperative programs
The SAW scripting language.
Translator from SAWCore to EasyCrypt
The Cryptol Symbolic Simulator, part of SAW.
Translator from Lean theorem prover into saw-core
convert simple cryptol expressions into finite-state machines
Simulator backend for saw-core based on SBV
The SAW core language.
Parser for the llvm bitcode format
A DSL for generating GR(1) problems
The LLVM Symbolic Simulator, part of SAW.
The Java Symbolic Simulator, part of SAW.
Simulator backend for saw-core based on AIGs
The seL4 microkernel
Component Architecture test suite and example apps.
Lean Theorem Prover
s2n : an implementation of the TLS/SSL protocols
Virtual Machine build as a CAmkES component.
Haskell bindings for the pcap library, which provides a low level interface to packet capture systems.
Semantics for Cryptol
CAmkES code and examples
An interpreter for the Mistral language.
The Ivory EDSL
A set of utilities for using indexed types including containers, equality, and comparison.
Haskell Bindings to the Lean Theorem Prover http://leanprover.github.io/