rebuilding site Wed May 14 07:15:17 CEST 2025

Author: franziskuskiefer

about/index.html

@@ -1,4 +1,10 @@
-<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Cryspen</title><link>https://cryspen.com/</link><description>Recent content on Cryspen</description><generator>Hugo</generator><language>en-us</language><lastBuildDate>Thu, 03 Apr 2025 00:00:00 +0000</lastBuildDate><atom:link href="https://cryspen.com/index.xml" rel="self" type="application/rss+xml"/><item><title>MLS Group State Forks: What, Why, How</title><link>https://cryspen.com/post/mls-fork-resolution/</link><pubDate>Thu, 03 Apr 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/mls-fork-resolution/</guid><description>&lt;p>Group state forks are faulty states that MLS groups can end up in. This article looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.&lt;/p></description></item><item><title>Cryspen @ RWC 2025</title><link>https://cryspen.com/post/rwc-2025/</link><pubDate>Thu, 27 Mar 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2025/</guid><description>&lt;p>&lt;a href="https://rwc.iacr.org/2025/">Real World Crypto 2025&lt;/a> buzzed with energy as
+<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Cryspen</title><link>https://cryspen.com/</link><description>Recent content on Cryspen</description><generator>Hugo</generator><language>en-us</language><lastBuildDate>Tue, 13 May 2025 00:00:00 +0000</lastBuildDate><atom:link href="https://cryspen.com/index.xml" rel="self" type="application/rss+xml"/><item><title>Cryspen Welcomes Clement</title><link>https://cryspen.com/post/welcome_clement/</link><pubDate>Tue, 13 May 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_clement/</guid><description>&lt;p>The team here at Cryspen is thrilled to welcome to our newest member, Clement!&lt;/p>
+&lt;p>&lt;a href="https://clement.blaudeau.net/">Clement&lt;/a> joins us fresh from his impressive
+journey as a PhD student at Inria Paris, where he was part of the &lt;a href="https://cambium.inria.fr/">Cambium
+team&lt;/a>. His doctoral work focused on the
+formalization of the powerful but intricate typing system of OCaml modules.
+Under the supervision of Didier Rémy and Gabriel Radanne, Clement delved deep
+into the theoretical underpinnings of this masterpiece of language design.&lt;/p></description></item><item><title>MLS Group State Forks: What, Why, How</title><link>https://cryspen.com/post/mls-fork-resolution/</link><pubDate>Thu, 03 Apr 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/mls-fork-resolution/</guid><description>&lt;p>Group state forks are faulty states that MLS groups can end up in. This article looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.&lt;/p></description></item><item><title>Cryspen @ RWC 2025</title><link>https://cryspen.com/post/rwc-2025/</link><pubDate>Thu, 27 Mar 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2025/</guid><description>&lt;p>&lt;a href="https://rwc.iacr.org/2025/">Real World Crypto 2025&lt;/a> buzzed with energy as
 the cutting edge of cryptography was presented to and discussed among an audience of leading
 researchers and developers from academia and industry. Today, on the second day of the conference,
 Cryspen teamed up with Google to showcase practical, scalable, verified solutions
@@ -123,10 +129,9 @@ We provide instantiations of the scheme using widely used and efficient primitiv
  data-mount-in="#join-widget"
  src="https://join.com/api/widget/bundle/eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJzZXR0aW5ncyI6eyJzaG93Q2F0ZWdvcnlGaWx0ZXIiOnRydWUsInNob3dMb2NhdGlvbkZpbHRlciI6dHJ1ZSwic2hvd0VtcGxveW1lbnRUeXBlRmlsdGVyIjp0cnVlLCJsYW5ndWFnZSI6ImVuIiwiam9ic1BlclBhZ2UiOjI1fSwiam9icyI6e30sImRlc2lnbiI6eyJzaG93TG9nbyI6dHJ1ZSwic2hvd0xvY2F0aW9uIjp0cnVlLCJzaG93RW1wbG95bWVudFR5cGUiOnRydWUsInNob3dDYXRlZ29yeSI6dHJ1ZSwiY29sb3JzIjp7IndpZGdldCI6eyJiYWNrZ3JvdW5kIjoiI0ZGRkZGRiIsImZpbHRlckJvcmRlciI6IiNENEQ0RDgiLCJwYWdpbmF0aW9uIjoiIzk5MDAwMCJ9LCJqb2JDYXJkIjp7InNoYWRvdyI6IiNGRkRCREIiLCJiYWNrZ3JvdW5kIjoiI0ZGRkZGRiIsInByaW1hcnlUZXh0IjoiIzNGM0Y0NiIsInNlY29uZGFyeVRleHQiOiIjNTI1MjVCIn19fSwidmVyc2lvbiI6MiwiY29tcGFueVB1YmxpY0lkIjoiNzUyMjA2YjVmYmM2ZmI5ZjA2YmM3NDEzM2JhMjdmYzciLCJpYXQiOjE2NzYxOTc0NTYsImp0aSI6ImVjZDJjYzA0LWEzYWUtNGI2ZC04ZWNlLTRiOTRjODhkYzlmOSJ9.x-Zdbbs8_ht6hYNS3DQs6UcLlN2mVps_eFaPGJU4vwU"
  >&lt;/script>
- &lt;/div></description></item><item><title>libcrux</title><link>https://cryspen.com/libcrux/</link><pubDate>Sun, 01 Jan 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/libcrux/</guid><description>&lt;p>Libcrux is a formally verified cryptographic library that brings together verified
-artifacts from different sources. It uses &lt;a href="https://cryspen.com/hacspec/">hacspec&lt;/a>
-as a common language for the specifications underlying the correctness and security
-proofs. Libcrux is written in Rust, a modern programming language that is known
+ &lt;/div></description></item><item><title>libcrux</title><link>https://cryspen.com/libcrux-library/</link><pubDate>Sun, 01 Jan 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/libcrux-library/</guid><description>&lt;p>Libcrux is a formally verified cryptographic library that brings together verified
+artifacts from different sources. It is verified using our &lt;a href="https://cryspen.com/hax-toolchain/">hax toolchain&lt;/a>.
+Libcrux is written in Rust, a modern programming language that is known
 for its safety and performance. Underneath, it uses verified Rust, C, and Assembly code.&lt;/p></description></item><item><title>OpenMLS</title><link>https://cryspen.com/openmls/</link><pubDate>Sun, 01 Jan 2023 00:00:00 +0000</pubDate><guid>https://cryspen.com/openmls/</guid><description>&lt;p>Messaging Layer Security (MLS) is a security layer for end-to-end encrypting
 communication in large dynamic groups.
 It has been specified by the &lt;a href="https://datatracker.ietf.org/wg/mls/about/">IETF MLS working group&lt;/a> and designed to be efficient,

images/clement_hu_da447295a2bd189d.jpg

@@ -78,7 +78,7 @@
 and how we can use them to increase confidence in important
 protocols like <a href=https://cryspen.com/post/pqxdh/>PQXDH</a>, <a href=https://cryspen.com/post/pq-bertie/>TLS</a>, and <a href=https://cryspen.com/post/pq-openmls/>MLS</a>.
 He also spoke about how we at Cryspen use <a href=https://cryspen.com/hax/>hax</a> to build verified post-quantum cryptographic libraries like
-<a href=https://cryspen.com/libcrux/>libcrux</a>.</p><p>The slides for Karthik&rsquo;s invited talk are available <a href=./Crypto24Slides.pdf>here</a>.</p><p>As Karthik says, if current trends hold, then in a few years, we can
+<a href=https://cryspen.com/libcrux-library/>libcrux</a>.</p><p>The slides for Karthik&rsquo;s invited talk are available <a href=./Crypto24Slides.pdf>here</a>.</p><p>As Karthik says, if current trends hold, then in a few years, we can
 expect that all new protocols and cryptographic libraries will need
 to have machine-checked proofs by default. The time to adopt formal
 verification is now!</p><p>If you have any questions about formal methods, and on how they can help you

images/mountain-team.jpeg

@@ -1,4 +1,10 @@
-<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Cryspen</title><link>https://cryspen.com/post/</link><description>Recent content on Cryspen</description><generator>Hugo</generator><language>en-us</language><lastBuildDate>Thu, 03 Apr 2025 00:00:00 +0000</lastBuildDate><atom:link href="https://cryspen.com/post/index.xml" rel="self" type="application/rss+xml"/><item><title>MLS Group State Forks: What, Why, How</title><link>https://cryspen.com/post/mls-fork-resolution/</link><pubDate>Thu, 03 Apr 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/mls-fork-resolution/</guid><description>&lt;p>Group state forks are faulty states that MLS groups can end up in. This article looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.&lt;/p></description></item><item><title>Cryspen @ RWC 2025</title><link>https://cryspen.com/post/rwc-2025/</link><pubDate>Thu, 27 Mar 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2025/</guid><description>&lt;p>&lt;a href="https://rwc.iacr.org/2025/">Real World Crypto 2025&lt;/a> buzzed with energy as
+<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Cryspen</title><link>https://cryspen.com/post/</link><description>Recent content on Cryspen</description><generator>Hugo</generator><language>en-us</language><lastBuildDate>Tue, 13 May 2025 00:00:00 +0000</lastBuildDate><atom:link href="https://cryspen.com/post/index.xml" rel="self" type="application/rss+xml"/><item><title>Cryspen Welcomes Clement</title><link>https://cryspen.com/post/welcome_clement/</link><pubDate>Tue, 13 May 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/welcome_clement/</guid><description>&lt;p>The team here at Cryspen is thrilled to welcome to our newest member, Clement!&lt;/p>
+&lt;p>&lt;a href="https://clement.blaudeau.net/">Clement&lt;/a> joins us fresh from his impressive
+journey as a PhD student at Inria Paris, where he was part of the &lt;a href="https://cambium.inria.fr/">Cambium
+team&lt;/a>. His doctoral work focused on the
+formalization of the powerful but intricate typing system of OCaml modules.
+Under the supervision of Didier Rémy and Gabriel Radanne, Clement delved deep
+into the theoretical underpinnings of this masterpiece of language design.&lt;/p></description></item><item><title>MLS Group State Forks: What, Why, How</title><link>https://cryspen.com/post/mls-fork-resolution/</link><pubDate>Thu, 03 Apr 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/mls-fork-resolution/</guid><description>&lt;p>Group state forks are faulty states that MLS groups can end up in. This article looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.&lt;/p></description></item><item><title>Cryspen @ RWC 2025</title><link>https://cryspen.com/post/rwc-2025/</link><pubDate>Thu, 27 Mar 2025 00:00:00 +0000</pubDate><guid>https://cryspen.com/post/rwc-2025/</guid><description>&lt;p>&lt;a href="https://rwc.iacr.org/2025/">Real World Crypto 2025&lt;/a> buzzed with energy as
 the cutting edge of cryptography was presented to and discussed among an audience of leading
 researchers and developers from academia and industry. Today, on the second day of the conference,
 Cryspen teamed up with Google to showcase practical, scalable, verified solutions

index.html

@@ -78,15 +78,15 @@
 giving impetus to new research on how to protect the confidentiality, integrity
 and privacy of all this data.</p><p>At Cryspen, we are engaged in multiple R&amp;D projects around these topics.
 We help design new encryption standards, such as <a href=https://www.rfc-editor.org/rfc/rfc9180.html>HPKE</a>, for protecting data at
-rest; we implement high-assurance cryptographic libraries, such as <a href=https://librux.org>libcrux</a>;
+rest; we implement high-assurance cryptographic libraries, such as <a href=http://librux.org>libcrux</a>;
 we design and implement new protocols, such as <a href=https://www.rfc-editor.org/rfc/rfc9420.html>MLS</a>, for communicating sensitive data between a large number of endpoints; and we investigate state-of-the-art constructions, such as multi-party computation, for privacy-preserving analysis over distributed data.</p><p>We are working with the <a href=https://sine.foundation/>SINE Foundation</a> on the <a href=https://www.forschung-it-sicherheit-kommunikationssysteme.de/projekte/atlas>Atlas</a> project,
 whose goal is to build a privacy-preserving data custodian for municipal data.
 In particular, we are helping to transition research results from the academic partners,
 <a href=https://hpi.de/lehmann/team/anja-lehmann.html>Anja Lehmann</a> at <a href=https://hpi.de/>HPI</a> and <a href=https://www.tu.berlin/en/dsi/team/florian-tschorsch>Florian Tschorsch</a> from <a href=https://www.tu.berlin/en/>TU Berlin</a>, by building
 usable specifications as well as the cryptographic components needed for the
 data custodian.
 In this project, we will use our <a href=/circus/>hax toolchain</a>, the <a href=/hacspec/>hacspec</a> language, and
-our verified crypto library <a href=https://librux.org>libcrux</a>.
+our verified crypto library <a href=http://librux.org>libcrux</a>.
 We will also help design and analyze the multi-party computation components needed in Atlas.</p><p>Cryspen is also an associated partner at <a href=https://prairie-institute.fr/>PRAIRIE</a>, the Paris
 Artificial Intelligence Research Institute. PRAIRIE aims to bring
 together academic research groups in the area of machine learning with