-
Notifications
You must be signed in to change notification settings - Fork 53
Home
Welcome to the jasmin wiki!
- About Jasmin
- Installation instructions
- Compilation to assembly
- Get support
- Pretty printing (export to LaTeX)
- Safety checker
- Extraction to EasyCrypt
- Constant-time verification
- Reference interpreter (a.k.a. executable formal semantics)
-
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub, "The Last Mile: High-Assurance and High-Speed Cryptographic Implementations," 2020 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2020, pp. 965-982, doi: 10.1109/SP40000.2020.00028.
-
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub. 2019. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS '19). Association for Computing Machinery, New York, NY, USA, 1607–1622. DOI:10.1145/3319535.3363211
-
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17). Association for Computing Machinery, New York, NY, USA, 1807–1823. DOI:10.1145/3133956.3134078