# orderedItems[].object.content
https://web.archive.org/web/2023091009 1944/https://csrc.nist.gov/CSRC/media/Events/ISPAB-MARCH-2014-MEETING/documents/a_quantum_world_v1_ispab_march_2014.pdf says author is "Post Quantum Cryptography Team, National Institute of Standards and Technology (NIST), pqc@nist.gov". FOIA results have revealed secret pqc@nist.gov team members in early Sep 2016, after draft NISTPQC call: more NSA people than NIST people.

# orderedItems[].object.contentMap.en
https://web.archive.org/web/2023091009 1944/https://csrc.nist.gov/CSRC/media/Events/ISPAB-MARCH-2014-MEETING/documents/a_quantum_world_v1_ispab_march_2014.pdf says author is "Post Quantum Cryptography Team, National Institute of Standards and Technology (NIST), pqc@nist.gov". FOIA results have revealed secret pqc@nist.gov team members in early Sep 2016, after draft NISTPQC call: more NSA people than NIST people.

# orderedItems[].object.content
@Elliptickiwi
Obviously in the broader mathematical literature there are many examples of wrong proofs, sometimes wrong theorems, that got all the way through refereeing and publication. Readers using theorems have no real evidence that referees were thorough, and often spend a ton of time re-checking proofs.

# orderedItems[].object.contentMap.en
@Elliptickiwi
Obviously in the broader mathematical literature there are many examples of wrong proofs, sometimes wrong theorems, that got all the way through refereeing and publication. Readers using theorems have no real evidence that referees were thorough, and often spend a ton of time re-checking proofs.

# orderedItems[].object.content
@Elliptickiwi Section 3.4 talks about a mistake in one preprint. The preprint is mostly a survey but has a (maybe-)new theorem where my first "proof" was simply wrong. That mistake was caught last year, before this year's computer-checking process for the preprint, but it would have been better for me to do the computer-checking before putting out the preprint in the first place. I'm now thinking about submission, and I'm sure the referees will be happy to hear about the computer-checked proofs.

# orderedItems[].object.contentMap.en
@Elliptickiwi Section 3.4 talks about a mistake in one preprint. The preprint is mostly a survey but has a (maybe-)new theorem where my first "proof" was simply wrong. That mistake was caught last year, before this year's computer-checking process for the preprint, but it would have been better for me to do the computer-checking before putting out the preprint in the first place. I'm now thinking about submission, and I'm sure the referees will be happy to hear about the computer-checked proofs.

# orderedItems[].object.content
My new report "Papers with computer-checked proofs" gives "case studies supporting the hypothesis that it is often affordable for a paper presenting theorems to also include proofs that have been checked with today's proof-checking software": https://cr.yp.to/papers.html#pwccp

# orderedItems[].object.contentMap.en
My new report "Papers with computer-checked proofs" gives "case studies supporting the hypothesis that it is often affordable for a paper presenting theorems to also include proofs that have been checked with today's proof-checking software": https://cr.yp.to/papers.html#pwccp

# orderedItems[].object.content
Just uploaded new version of my paper "Understanding binary-Goppa decoding": https://cr.yp.to/papers.html#goppadeco ding Includes detailed comparisons of all ten theorems to formalizations of the theorems in HOL Light and in Lean. Also explains how to run HOL Light and Lean to verify the proofs.

# orderedItems[].object.contentMap.en
Just uploaded new version of my paper "Understanding binary-Goppa decoding": https://cr.yp.to/papers.html#goppadeco ding Includes detailed comparisons of all ten theorems to formalizations of the theorems in HOL Light and in Lean. Also explains how to run HOL Light and Lean to verify the proofs.

# orderedItems[].object.content
Now posted HOL Light formalizations of the same theorems about decoding Goppa codes: https://cr.yp.to/2023/lightgoppa-20230 811-verify.html (https://cr-yp-to.viacache.net/2023/lig htgoppa-20230811-verify.html via Cloudflare). More verbose than the Lean versions, but took me less time to write. Which will be a better foundation for software verification?

# orderedItems[].object.contentMap.en
Now posted HOL Light formalizations of the same theorems about decoding Goppa codes: https://cr.yp.to/2023/lightgoppa-20230 811-verify.html (https://cr-yp-to.viacache.net/2023/lig htgoppa-20230811-verify.html via Cloudflare). More verbose than the Lean versions, but took me less time to write. Which will be a better foundation for software verification?

# orderedItems[].object.content
Formally verified theorems about decoding Goppa codes: https://cr.yp.to/2023/leangoppa-202307 26-verify.html This is using the Lean theorem prover; I'll try formalizing the same theorems in HOL Light for comparison. This is a step towards full verification of fast software for the McEliece cryptosystem.

# orderedItems[].object.contentMap.en
Formally verified theorems about decoding Goppa codes: https://cr.yp.to/2023/leangoppa-202307 26-verify.html This is using the Lean theorem prover; I'll try formalizing the same theorems in HOL Light for comparison. This is a step towards full verification of fast software for the McEliece cryptosystem.

# orderedItems[].object.content
lib25519-20230630 with new code from Kaushik Nath for batch nP (e.g., Tiger Lake: 22 kcycles!) and multi-scalar mult: https://lib25519.cr.yp.to https://lib25519-cr-yp-to.viacache.net Also CLI, infrastructure improvements, Alpine/musl support. Still needs more auditing and formal verification.

# orderedItems[].object.contentMap.en
lib25519-20230630 with new code from Kaushik Nath for batch nP (e.g., Tiger Lake: 22 kcycles!) and multi-scalar mult: https://lib25519.cr.yp.to https://lib25519-cr-yp-to.viacache.net Also CLI, infrastructure improvements, Alpine/musl support. Still needs more auditing and formal verification.

# orderedItems[].object.content
"We operate transparently." FOIA lawsuit docs so far: first evasion (copies of public docs), then much more interesting secret slides, and now a month of secret email, including scheduling 12 Jan 2016 meeting with NSA, 26 Jan 2016 meeting with NSA, 2 Feb 2016 meeting with GCHQ.

# orderedItems[].object.contentMap.en
"We operate transparently." FOIA lawsuit docs so far: first evasion (copies of public docs), then much more interesting secret slides, and now a month of secret email, including scheduling 12 Jan 2016 meeting with NSA, 26 Jan 2016 meeting with NSA, 2 Feb 2016 meeting with GCHQ.

# orderedItems[].object.content
Here's a cryptosystem as an attack challenge: implementable PQ ECDH NIKE! Use n = 2^32-5; Koblitz curve over F_{2^n}; type-2 ONB; T = Frob; secret exponent (1+T^r1)...(1+T^r64)T^r0+T^r65+...+T^r96. Basic Shor is too slow even for 2^r1+...+2^r64, group F_{2^n}^*. Note 2n+1 factor.

# orderedItems[].object.contentMap.en
Here's a cryptosystem as an attack challenge: implementable PQ ECDH NIKE! Use n = 2^32-5; Koblitz curve over F_{2^n}; type-2 ONB; T = Frob; secret exponent (1+T^r1)...(1+T^r64)T^r0+T^r65+...+T^r96. Basic Shor is too slow even for 2^r1+...+2^r64, group F_{2^n}^*. Note 2n+1 factor.

# orderedItems[].object.content
Wow, finally an honest version of FrodoKEM! New paper https://eprint.iacr.org/2023/947 from Joel Gärtner proves that 2^128 QROM IND-CCA2 security for dimension 79510 with 37-bit modulus follows from a reasonably conjectured quantitative hardness assumption for worst-case approximate SIVP.

# orderedItems[].object.contentMap.en
Wow, finally an honest version of FrodoKEM! New paper https://eprint.iacr.org/2023/947 from Joel Gärtner proves that 2^128 QROM IND-CCA2 security for dimension 79510 with 37-bit modulus follows from a reasonably conjectured quantitative hardness assumption for worst-case approximate SIVP.

# orderedItems[].object.content
https://viacache.net now redistributes the cr.yp.to web pages via Cloudflare. For example, latest NSA/NIST FOIA results: https://nist-pqcrypto-org.viacache.net/foia/index.html libmceliece: https://lib-mceliece-org.viacache.net "Turbo Boost: How to perpetuate security problems": https://blog-cr-yp-to.viacache.net/202 30609-turboboost.html

# orderedItems[].object.contentMap.en
https://viacache.net now redistributes the cr.yp.to web pages via Cloudflare. For example, latest NSA/NIST FOIA results: https://nist-pqcrypto-org.viacache.net/foia/index.html libmceliece: https://lib-mceliece-org.viacache.net "Turbo Boost: How to perpetuate security problems": https://blog-cr-yp-to.viacache.net/202 30609-turboboost.html

# orderedItems[].object.content
Given yesterday's 18-hour DoS attack against the cr.yp.to network, I'm reposting recent links. Latest NSA/NIST FOIA results: https://nist.pqcrypto.org/foia/index.h tml libmceliece: https://lib.mceliece.org "Turbo Boost: How to perpetuate security problems": https://blog.cr.yp.to/20230609-turbobo ost.html

# orderedItems[].object.contentMap.en
Given yesterday's 18-hour DoS attack against the cr.yp.to network, I'm reposting recent links. Latest NSA/NIST FOIA results: https://nist.pqcrypto.org/foia/index.h tml libmceliece: https://lib.mceliece.org "Turbo Boost: How to perpetuate security problems": https://blog.cr.yp.to/20230609-turbobo ost.html

# orderedItems[].object.content
Pleased to announce CryptAttackTester, a framework to systematically catch bugs in cryptanalysis. CAT tests analyses of completely specified algorithms in a simple, fully defined cost metric. Includes many ISD attacks + AES-128. Joint work with @TungChou1. https://cat.cr.yp.to

# orderedItems[].object.contentMap.en
Pleased to announce CryptAttackTester, a framework to systematically catch bugs in cryptanalysis. CAT tests analyses of completely specified algorithms in a simple, fully defined cost metric. Includes many ISD attacks + AES-128. Joint work with @TungChou1. https://cat.cr.yp.to

# orderedItems[].object.content
@bartavi Updated, thanks.

# orderedItems[].object.contentMap.en
@bartavi Updated, thanks.

# orderedItems[].object.content
@briansmith Examples of statements from Intel in the cited sources: "we demonstrate how such power management-based frequency throttling activity forms a source of timing side-channel information leakage, which can be exploited by an attacker to infer secret data even from a constant-cycle victim workload"; "options that fully resolve the security issue (e.g., #2 and #6) bring high performance or functional impact".

# orderedItems[].object.contentMap.en
@briansmith Examples of statements from Intel in the cited sources: "we demonstrate how such power management-based frequency throttling activity forms a source of timing side-channel information leakage, which can be exploited by an attacker to infer secret data even from a constant-cycle victim workload"; "options that fully resolve the security issue (e.g., #2 and #6) bring high performance or functional impact".

# orderedItems[].object.content
@briansmith "Stops attacks" is referring to the class of attacks at hand. It doesn't mean "stops all implementation attacks" or even "stops all timing attacks"; see, e.g., the comment on crystal variability. For the class of attacks at hand, everyone agrees that the root cause is DVFS; Intel's documentation says how to turn that off; various tests comparing rdpmc, rdtsc, and NTP haven't falsified this. Recommendations against this defense instead come from performance hype.

# orderedItems[].object.contentMap.en
@briansmith "Stops attacks" is referring to the class of attacks at hand. It doesn't mean "stops all implementation attacks" or even "stops all timing attacks"; see, e.g., the comment on crystal variability. For the class of attacks at hand, everyone agrees that the root cause is DVFS; Intel's documentation says how to turn that off; various tests comparing rdpmc, rdtsc, and NTP haven't falsified this. Recommendations against this defense instead come from performance hype.

# orderedItems[].object.content
libmceliece now available from https://lib.mceliece.org for post-quantum encryption with Classic McEliece, wrapping fast code from @tungchou1 + me. Simple stateless wire-format API and CLI. Automatic run-time selection of implementations: unified binary works with or without AVX2.

# orderedItems[].object.contentMap.en
libmceliece now available from https://lib.mceliece.org for post-quantum encryption with Classic McEliece, wrapping fast code from @tungchou1 + me. Simple stateless wire-format API and CLI. Automatic run-time selection of implementations: unified binary works with or without AVX2.

# orderedItems[].object.content
New blog post "Turbo Boost: How to perpetuate security problems." https://blog.cr.yp.to/20230609-turbobo ost.html with special guest appearances from Shark, Fluffy, and Turbo Boost Max Ultra Hyper Performance Extreme. #overclocking #performancehype #power #timing #hertzbleed #riskmanagement #environment

# orderedItems[].object.contentMap.en
New blog post "Turbo Boost: How to perpetuate security problems." https://blog.cr.yp.to/20230609-turbobo ost.html with special guest appearances from Shark, Fluffy, and Turbo Boost Max Ultra Hyper Performance Extreme. #overclocking #performancehype #power #timing #hertzbleed #riskmanagement #environment

# orderedItems[].object.content
Exercise in systems engineering: What's the best fix for https://github.com/cloudflare/circl/se curity/advisories/GHSA-2q89-485c-9j2x? Change the Kyber and FrodoKEM software? Change the RNG to a simpler randombytes() API that guarantees callers won't see this failure case? Crypto students aren't taught how to think this through.

# orderedItems[].object.contentMap.en
Exercise in systems engineering: What's the best fix for https://github.com/cloudflare/circl/se curity/advisories/GHSA-2q89-485c-9j2x? Change the Kyber and FrodoKEM software? Change the RNG to a simpler randombytes() API that guarantees callers won't see this failure case? Crypto students aren't taught how to think this through.