rebuilding site Mon Nov 25 11:22:11 CET 2024

index.xml

@@ -27,7 +27,7 @@ implementation of ML-KEM in Rust, and talked about how our
 high-assurance development methodology helped us find a <a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">new timing
 bug</a>
 in various other Kyber implementations.&lt;/p></description></item><item><title>Verified ML-KEM (Kyber) in Rust</title><link>https://cryspen.com/post/ml-kem-implementation/</link><pubDate>Tue, 16 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/ml-kem-implementation/</guid><description>&lt;p>ML-KEM, previously known as &lt;a href="https://pq-crystals.org/kyber/">Kyber&lt;/a>, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in &lt;a href="https://csrc.nist.gov/pubs/fips/203/ipd">FIPS 203&lt;/a>.&lt;/p>
-&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/src/kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Welcome Jan &amp; Lucas</title><link>https://cryspen.com/post/welcome_jan_lucas/</link><pubDate>Mon, 08 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_jan_lucas/</guid><description>&lt;p>📢 Exciting News! Cryspen is thrilled to announce the addition of two exceptional minds to our team: &lt;a href="https://lucas.franceschino.fr/">Dr. Lucas Franceschino&lt;/a> and &lt;a href="https://github.com/keks">Jan Winkelmann&lt;/a>.&lt;/p></description></item><item><title>An Analysis of Signal's PQXDH</title><link>https://cryspen.com/post/pqxdh/</link><pubDate>Fri, 20 Oct 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/pqxdh/</guid><description>&lt;!-- _Karthikeyan Bhargavan ([Cryspen]), Charlie Jacomme ([Inria Paris](https://www.inria.fr/en/inria-paris-centre)), Franziskus Kiefer ([Cryspen]) and Rolfe Schmidt ([Signal](https://signal.org/))_ -->
+&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/libcrux-kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Welcome Jan &amp; Lucas</title><link>https://cryspen.com/post/welcome_jan_lucas/</link><pubDate>Mon, 08 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_jan_lucas/</guid><description>&lt;p>📢 Exciting News! Cryspen is thrilled to announce the addition of two exceptional minds to our team: &lt;a href="https://lucas.franceschino.fr/">Dr. Lucas Franceschino&lt;/a> and &lt;a href="https://github.com/keks">Jan Winkelmann&lt;/a>.&lt;/p></description></item><item><title>An Analysis of Signal's PQXDH</title><link>https://cryspen.com/post/pqxdh/</link><pubDate>Fri, 20 Oct 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/pqxdh/</guid><description>&lt;!-- _Karthikeyan Bhargavan ([Cryspen]), Charlie Jacomme ([Inria Paris](https://www.inria.fr/en/inria-paris-centre)), Franziskus Kiefer ([Cryspen]) and Rolfe Schmidt ([Signal](https://signal.org/))_ -->
 &lt;p>Signal recently &lt;a href="https://signal.org/docs/specifications/pqxdh/">published&lt;/a> a new, post-quantum secure, version of their &lt;a href="https://signal.org/docs/specifications/x3dh/">X3DH&lt;/a> protocol called &lt;a href="https://signal.org/docs/specifications/pqxdh/">PQXDH&lt;/a>. As with any new cryptographic protocol, it is important to precisely analyse its security properties, especially for something as important as Signal.&lt;/p></description></item><item><title>Announcing Campus Cyber Circus Project</title><link>https://cryspen.com/post/cyber-campus-hax/</link><pubDate>Wed, 20 Sep 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/cyber-campus-hax/</guid><description>&lt;p>🎉 We&amp;rsquo;re excited to announce that Cryspen &lt;a href="https://ptcc.fr/projets/circus-2/">partnered&lt;/a> with &lt;a href="https://www.inria.fr/fr">Inria&lt;/a> on a transfer project to build a new integrated development and verification environment (IDVE). The project is part of the transfer program at &lt;a href="https://campuscyber.fr/">Campus Cyber&lt;/a>, which brings together France&amp;rsquo;s top cybersecurity experts.&lt;/p></description></item><item><title>Specifying Oblivious Pseudonymization</title><link>https://cryspen.com/post/scrambledb/</link><pubDate>Mon, 18 Sep 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/scrambledb/</guid><description>&lt;p>In this blog post we announce an executable specification in the
 &lt;code>hacspec&lt;/code> specification language for the &lt;code>ScrambleDB&lt;/code> pseudonymization
 system, developed by Cryspen as part of the &lt;a href="https://www.forschung-it-sicherheit-kommunikationssysteme.de/projekte/atlas">BMBF ATLAS project&lt;/a>.&lt;/p></description></item><item><title>Internet Defense Prize 2023</title><link>https://cryspen.com/post/internet-defense-prize-2023/</link><pubDate>Mon, 14 Aug 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/internet-defense-prize-2023/</guid><description>&lt;p>At the &lt;a href="https://www.usenix.org/conference/usenixsecurity23">32nd Usenix Security Symposium&lt;/a> in Anaheim CA, a paper on the &lt;a href="https://cryspen.com/post/mls-introduction/">Messaging Layer Security Protocol&lt;/a>, co-authored by our founders Jonathan Protzenko and Karthikeyan Bhargavan, was awarded both the Distinguished Paper Award and the prestigious &lt;a href="https://www.usenix.org/blog/usenix-announces-winners-2023-internet-defense-prize">Internet Defense Prize&lt;/a>.&lt;/p></description></item><item><title>Prairie and Atlas</title><link>https://cryspen.com/post/prarie-and-atlas/</link><pubDate>Wed, 09 Aug 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/prarie-and-atlas/</guid><description>&lt;p>With the widespread adoption and deployment of machine learning across enterprises,

post/index.xml

@@ -27,7 +27,7 @@ implementation of ML-KEM in Rust, and talked about how our
 high-assurance development methodology helped us find a <a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">new timing
 bug</a>
 in various other Kyber implementations.&lt;/p></description></item><item><title>Verified ML-KEM (Kyber) in Rust</title><link>https://cryspen.com/post/ml-kem-implementation/</link><pubDate>Tue, 16 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/ml-kem-implementation/</guid><description>&lt;p>ML-KEM, previously known as &lt;a href="https://pq-crystals.org/kyber/">Kyber&lt;/a>, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in &lt;a href="https://csrc.nist.gov/pubs/fips/203/ipd">FIPS 203&lt;/a>.&lt;/p>
-&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/src/kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Welcome Jan &amp; Lucas</title><link>https://cryspen.com/post/welcome_jan_lucas/</link><pubDate>Mon, 08 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_jan_lucas/</guid><description>&lt;p>📢 Exciting News! Cryspen is thrilled to announce the addition of two exceptional minds to our team: &lt;a href="https://lucas.franceschino.fr/">Dr. Lucas Franceschino&lt;/a> and &lt;a href="https://github.com/keks">Jan Winkelmann&lt;/a>.&lt;/p></description></item><item><title>An Analysis of Signal's PQXDH</title><link>https://cryspen.com/post/pqxdh/</link><pubDate>Fri, 20 Oct 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/pqxdh/</guid><description>&lt;!-- _Karthikeyan Bhargavan ([Cryspen]), Charlie Jacomme ([Inria Paris](https://www.inria.fr/en/inria-paris-centre)), Franziskus Kiefer ([Cryspen]) and Rolfe Schmidt ([Signal](https://signal.org/))_ -->
+&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/libcrux-kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Welcome Jan &amp; Lucas</title><link>https://cryspen.com/post/welcome_jan_lucas/</link><pubDate>Mon, 08 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_jan_lucas/</guid><description>&lt;p>📢 Exciting News! Cryspen is thrilled to announce the addition of two exceptional minds to our team: &lt;a href="https://lucas.franceschino.fr/">Dr. Lucas Franceschino&lt;/a> and &lt;a href="https://github.com/keks">Jan Winkelmann&lt;/a>.&lt;/p></description></item><item><title>An Analysis of Signal's PQXDH</title><link>https://cryspen.com/post/pqxdh/</link><pubDate>Fri, 20 Oct 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/pqxdh/</guid><description>&lt;!-- _Karthikeyan Bhargavan ([Cryspen]), Charlie Jacomme ([Inria Paris](https://www.inria.fr/en/inria-paris-centre)), Franziskus Kiefer ([Cryspen]) and Rolfe Schmidt ([Signal](https://signal.org/))_ -->
 &lt;p>Signal recently &lt;a href="https://signal.org/docs/specifications/pqxdh/">published&lt;/a> a new, post-quantum secure, version of their &lt;a href="https://signal.org/docs/specifications/x3dh/">X3DH&lt;/a> protocol called &lt;a href="https://signal.org/docs/specifications/pqxdh/">PQXDH&lt;/a>. As with any new cryptographic protocol, it is important to precisely analyse its security properties, especially for something as important as Signal.&lt;/p></description></item><item><title>Announcing Campus Cyber Circus Project</title><link>https://cryspen.com/post/cyber-campus-hax/</link><pubDate>Wed, 20 Sep 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/cyber-campus-hax/</guid><description>&lt;p>🎉 We&amp;rsquo;re excited to announce that Cryspen &lt;a href="https://ptcc.fr/projets/circus-2/">partnered&lt;/a> with &lt;a href="https://www.inria.fr/fr">Inria&lt;/a> on a transfer project to build a new integrated development and verification environment (IDVE). The project is part of the transfer program at &lt;a href="https://campuscyber.fr/">Campus Cyber&lt;/a>, which brings together France&amp;rsquo;s top cybersecurity experts.&lt;/p></description></item><item><title>Specifying Oblivious Pseudonymization</title><link>https://cryspen.com/post/scrambledb/</link><pubDate>Mon, 18 Sep 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/scrambledb/</guid><description>&lt;p>In this blog post we announce an executable specification in the
 &lt;code>hacspec&lt;/code> specification language for the &lt;code>ScrambleDB&lt;/code> pseudonymization
 system, developed by Cryspen as part of the &lt;a href="https://www.forschung-it-sicherheit-kommunikationssysteme.de/projekte/atlas">BMBF ATLAS project&lt;/a>.&lt;/p></description></item><item><title>Internet Defense Prize 2023</title><link>https://cryspen.com/post/internet-defense-prize-2023/</link><pubDate>Mon, 14 Aug 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/internet-defense-prize-2023/</guid><description>&lt;p>At the &lt;a href="https://www.usenix.org/conference/usenixsecurity23">32nd Usenix Security Symposium&lt;/a> in Anaheim CA, a paper on the &lt;a href="https://cryspen.com/post/mls-introduction/">Messaging Layer Security Protocol&lt;/a>, co-authored by our founders Jonathan Protzenko and Karthikeyan Bhargavan, was awarded both the Distinguished Paper Award and the prestigious &lt;a href="https://www.usenix.org/blog/usenix-announces-winners-2023-internet-defense-prize">Internet Defense Prize&lt;/a>.&lt;/p></description></item><item><title>Prairie and Atlas</title><link>https://cryspen.com/post/prarie-and-atlas/</link><pubDate>Wed, 09 Aug 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/prarie-and-atlas/</guid><description>&lt;p>With the widespread adoption and deployment of machine learning across enterprises,

tags/libcrux/index.xml

@@ -13,4 +13,4 @@ implementation of ML-KEM in Rust, and talked about how our
 high-assurance development methodology helped us find a <a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">new timing
 bug</a>
 in various other Kyber implementations.&lt;/p></description></item><item><title>Verified ML-KEM (Kyber) in Rust</title><link>https://cryspen.com/post/ml-kem-implementation/</link><pubDate>Tue, 16 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/ml-kem-implementation/</guid><description>&lt;p>ML-KEM, previously known as &lt;a href="https://pq-crystals.org/kyber/">Kyber&lt;/a>, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in &lt;a href="https://csrc.nist.gov/pubs/fips/203/ipd">FIPS 203&lt;/a>.&lt;/p>
-&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/src/kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Cryspen @ RWC 2023</title><link>https://cryspen.com/post/rwc-2023/</link><pubDate>Mon, 12 Jun 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2023/</guid><description>&lt;p>At Real World Crypto 2023 in Tokyo, we gave a talk on the hacspec language, the hax tool, and the libcrux crypto library.&lt;/p></description></item></channel></rss>
+&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/libcrux-kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item><item><title>Cryspen @ RWC 2023</title><link>https://cryspen.com/post/rwc-2023/</link><pubDate>Mon, 12 Jun 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2023/</guid><description>&lt;p>At Real World Crypto 2023 in Tokyo, we gave a talk on the hacspec language, the hax tool, and the libcrux crypto library.&lt;/p></description></item></channel></rss>

tags/pqc/index.xml

@@ -3,4 +3,4 @@ implementation of ML-KEM in Rust, and talked about how our
 high-assurance development methodology helped us find a <a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">new timing
 bug</a>
 in various other Kyber implementations.&lt;/p></description></item><item><title>Verified ML-KEM (Kyber) in Rust</title><link>https://cryspen.com/post/ml-kem-implementation/</link><pubDate>Tue, 16 Jan 2024 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/ml-kem-implementation/</guid><description>&lt;p>ML-KEM, previously known as &lt;a href="https://pq-crystals.org/kyber/">Kyber&lt;/a>, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in &lt;a href="https://csrc.nist.gov/pubs/fips/203/ipd">FIPS 203&lt;/a>.&lt;/p>
-&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/src/kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item></channel></rss>
+&lt;p>Cryspen has built &lt;a href="https://github.com/cryspen/libcrux/tree/main/libcrux-kem">a new high assurance Rust implementation of ML-KEM&lt;/a>, using our verification framework &lt;a href="https://cryspen.com/hax">hax&lt;/a> and &lt;a href="https://fstar-lang.org">F*&lt;/a>. Our implementation is among the fastest portable implementations that we know of (see &lt;a href="#performance-comparison">Performance comparison&lt;/a>), and helped uncover a &lt;a href="https://github.com/pq-crystals/kyber/commit/dda29cc63af721981ee2c831cf00822e69be3220">timing bug&lt;/a> (also called &lt;a href="https://kyberslash.cr.yp.to/">KyberSlash&lt;/a>) in various Kyber implementations that would allow an attacker to &lt;a href="https://groups.google.com/a/list.nist.gov/g/pqc-forum/c/ldX0ThYJuBo/m/uIOqRF5BAwAJ">recover the private key&lt;/a>.&lt;/p></description></item></channel></rss>