Cryptoverif Alternatives

Similar projects and alternatives to cryptoverif

Wren

44 6,748 0.0 Wren cryptoverif VS Wren

The Wren Programming Language. Wren is a small, fast, class-based concurrent scripting language.
tinyssh

8 1,389 5.0 C cryptoverif VS tinyssh

TinySSH is small server (less than 100000 words of code)
WorkOS

workos.com sponsored

The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
dracut-sshd

7 203 4.6 Shell cryptoverif VS dracut-sshd

Provide SSH access to initramfs early user space on Fedora and other systems that use Dracut
ssh

4 3,412 4.6 Go cryptoverif VS ssh

Easy SSH servers in Golang
ultrablue

2 126 - Kotlin cryptoverif VS ultrablue

User-friendly Lightweight TPM Remote Attestation over Bluetooth
cryptsetup-ssh-unlocker

1 14 - Python cryptoverif VS cryptsetup-ssh-unlocker

Utility for unattended remote unlock of LUKS encrypted LVM using SSH and cryptsetup

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better cryptoverif alternative or higher similarity.

Suggest an alternative to cryptoverif

cryptoverif reviews and mentions

Posts with mentions or reviews of cryptoverif. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2024-03-24.

Tinyssh
7 projects | news.ycombinator.com | 24 Mar 2024

A better question to ask would have been, why settle for just memory safety - does a formally verified sshd exist? That kind of thing seems to be implemented more in OCaml and F#, like Project Everest, which has formally verified implementations of primitives (HACL) TLS, QUIC, and Signal https://project-everest.github.io/ ... ssh is notably missing?
I had a dig and found that ssh had in fact been done 9 years ago, tho it doesn't seem to have made it to a distribution: it's an offshoot of the CryptoVerif project[1] (which is, maybe unsurprisingly, under the umbrella of the same Prosecco team at Inria who worked on Project Everest). In 2015 Bruno Blanchet and David Cadé wrote a paper "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH"[2] which describes using CryptoVerif to generate an implementation of SSH from the spec; the code is in the CryptoVerif tarball, but someone's helpfully put that up on github if you want a look https://github.com/mgrabovsky/cryptoverif/tree/master/implem...
The eye opening bits in the paper (given the claims of tinyssh to be small at < 100k words):