7 ms·

Just wondering — has anyone come across a course or resource that explores how cryptographic systems are built up from smaller building blocks? Like, using som

Just wondering — has anyone come across a course or resource that explores how cryptographic systems are built up from smaller building blocks? Like, using something like SageMath for algebraic structures, a prover like Lean to verify properties — to get a feel for how things actually fit together. There's something cool about trying to reimplement known standards just to understand them better (with the usual "don’t roll your own crypto" warning, of course). By the way, it would be nice to have a kind of sandbox for the more formal path to explore how to build my own SP-network, prove that the Decisional Diffie-Hellman assumption holds or something. I've seen cryptopals and cryptohack.

moi2388 1y ago
That’d indeed be nice to do.
cmrx64 1y ago
the types of arguments and proofs used in cryptography are notoriously difficult to mechanize, a little bit of lean isn’t going to go get anywhere close to stating a security property. eg CryptHOL needs a ton of infrastructure, and in still very limited: https://eprint.iacr.org/2017/753.pdf https://eprint.iacr.org/2017/753.pdf
- nioj 1y ago
  There is also SSProve which has similar goal to CryptHOL: https://dl.acm.org/doi/full/10.1145/3594735 https://dl.acm.org/doi/full/10.1145/3594735 https://github.com/SSProve/ssprove https://github.com/SSProve/ssprove
oleganza 1y ago
When I learned crypto 5-10 years ago, it turned out that a lot of "building blocks" are mostly hacks. Looking back from 2020s we see that some of the standards that we use for the last 20-30 years can in principle be thrown out of the window (they can't for compatibility reasons, though) and replaced with much cleaner and more universal replacements. If we do not talk about modern exotic stuff (post-quantum crypto, zkSNARKS, homomorphic encryption), the 99% of everyday cryptography is based on two building blocks: 1. Symmetric crypto for ciphers and hash functions. 2. Algebraic group with "hard discrete log problem" for key exchange, signatures, asymmetric encryption and simple zero-knowledge proofs. Historically, these two categories are filled with a zoo of protocols. E.g. AES is a block cipher, but SHA(1,2) is a hash function. Today, you can roughly achieve everything of the above with two universal building blocks: - Keccak for all of symmetric crypto: it is suited both for encryption, hashing, duplex transcripts for ZK protocols etc. - Ristretto255 group based on Curve 25519: for diffie-hellman, signatures, key derivation, threshold schemes, encryption and more. The problem is that none of the described features is implemented in a turnkey standard, and we are still stuck using older crypto. Heck, even Git is using SHA-1 still. Then, after you have your building blocks, there are more hairy stuff such as application-specific protocols: TLS, Signal, PAKE/OPAQUE, proprietary hardware security schemes for full disk encryption and access controls etc.
- eXpl0it3r 1y ago
  I'm absolutely clueless about crypto, isn't there also a trade-off between being mathematically superior and well optimized in software/hardware implementation?
  - deleted 1y ago
    [deleted]
  - oleganza 1y ago
    The tradeoff is not that simple (I wish it was :-). Usually it goes like that: someone made something useful optimised for a specific use-case with certain time (or competence) constraints, within a total lack of decent alternatives. Then people adopt and use it, it becomes the standard. Then people want to do more things with it, and try to build around that thing, or on top of that thing and Frankenstein monsters get born and also become standard. If you start from scratch you can do a crypto protocol that is both better designed (causes less UX pain and critical bugs) AND performs better on relevant hardware. Also do not forget that performance is easily solved by hardware: Moore's law and then custom hardware extensions are a thing. Example: Keccak is so much better from the composition perspective, that when used ubiquitously you'd definitely have ubiquitous hardware support. But if everyone continues to use a mishmash of AES and SHA constructions on the pretext of "Keccak" is not as fast, then we'd never move forward. People would continue building over-complicated protocols, bearing subpar performance and keeping the reputation of dark wizardry inaccessible for mere mortals.
    - eXpl0it3r 1y ago
      > Also do not forget that performance is easily solved by hardware: Moore's law "Just write slow algorithms, hardware will eventually get faster" doesn't really work when talking about performance implications now. If the hash algorithm used million of times doesn't perform on current user hardware, then the algorithm is simply not a good fit. > and then custom hardware extensions are a thing. That's the kind of trade-off I eluded to as well. As a developer of a tool (e.g. git), I'd pick hash algorithms that do have hardware extensions on the most common hardware and not use something, that may eventually get hardware extensions. I guess developing such protocols right now for the future might still be advisable, but it seems odd to critic software that use well-optimized algorithms and fulfill the requirements.
k__ 1y ago
Not really, but I liked this one. https://github.com/nakov/practical-cryptography-for-developers-book https://github.com/nakov/practical-cryptography-for-develope...
cvwright 1y ago
There are no proofs of the hardness of DDH or RSA etc. That’s why they’re called assumptions. OTOH if you want to win a Turing Award…
- AnotherGoodName 1y ago
  Just to add to the above for clarity a proof that key based encryption isn't reversible requires a proof of P!=NP which hasn't been done. That may surprise people but we have no proof of the robustness of the encryption we use. In fact it might not work! Consider a one time pad for really extreme security needs. One time pads do have a proof (see the work of Shannon).
  - gary_0 1y ago
    Shor's algorithm suggests that a lot of encryption doesn't actually work, but of course it requires a quantum computer that hasn't yet been built, and may not be practical to build, so fingers crossed. At least there are quantum-resistant encryption algorithms, and OTPs are still provably secure like you say.
    - Tadpole9181 1y ago
      On "finger's crossed" - I think it's important to say that the majority of web traffic has switched over to PQC algorithms for key exchange that are not susceptible (thanks Cloudflare). We're not close to building a machine suitable for running Shor's in a practical sense, so even potential "store now, break later" attacks are now kinda pointless. Things like SSH keys are trivially revokable and often have enforced expirations, so they're not really a viable attack vector anyway. The symmetric encryption used for the vast majority of actual encryption has always been safe. Grover's algorithm does not scale appropriately (exponential on key length) unlike Shor's and cannot be parallelized. Worst case, AES-128 becomes as week as AES-64. So we bump it to AES-256 and we're back at the same difficulty as before (impossible). There's a degree of confidence this will always hold true.
- vendiddy 1y ago
  Can't someone learn this stuff with the assumption that certain functions are hard to invert? Like assuming f(x) is hard, let us try to prove these other properties of security.

moi2388 1y ago

That’d indeed be nice to do.

cmrx64 1y ago

the types of arguments and proofs used in cryptography are notoriously difficult to mechanize, a little bit of lean isn’t going to go get anywhere close to stating a security property. eg CryptHOL needs a ton of infrastructure, and in still very limited: https://eprint.iacr.org/2017/753.pdf https://eprint.iacr.org/2017/753.pdf

nioj 1y ago
There is also SSProve which has similar goal to CryptHOL: https://dl.acm.org/doi/full/10.1145/3594735 https://dl.acm.org/doi/full/10.1145/3594735 https://github.com/SSProve/ssprove https://github.com/SSProve/ssprove

oleganza 1y ago

When I learned crypto 5-10 years ago, it turned out that a lot of "building blocks" are mostly hacks. Looking back from 2020s we see that some of the standards that we use for the last 20-30 years can in principle be thrown out of the window (they can't for compatibility reasons, though) and replaced with much cleaner and more universal replacements. If we do not talk about modern exotic stuff (post-quantum crypto, zkSNARKS, homomorphic encryption), the 99% of everyday cryptography is based on two building blocks: 1. Symmetric crypto for ciphers and hash functions. 2. Algebraic group with "hard discrete log problem" for key exchange, signatures, asymmetric encryption and simple zero-knowledge proofs. Historically, these two categories are filled with a zoo of protocols. E.g. AES is a block cipher, but SHA(1,2) is a hash function. Today, you can roughly achieve everything of the above with two universal building blocks: - Keccak for all of symmetric crypto: it is suited both for encryption, hashing, duplex transcripts for ZK protocols etc. - Ristretto255 group based on Curve 25519: for diffie-hellman, signatures, key derivation, threshold schemes, encryption and more. The problem is that none of the described features is implemented in a turnkey standard, and we are still stuck using older crypto. Heck, even Git is using SHA-1 still. Then, after you have your building blocks, there are more hairy stuff such as application-specific protocols: TLS, Signal, PAKE/OPAQUE, proprietary hardware security schemes for full disk encryption and access controls etc.

eXpl0it3r 1y ago
I'm absolutely clueless about crypto, isn't there also a trade-off between being mathematically superior and well optimized in software/hardware implementation?
- deleted 1y ago
  [deleted]
- oleganza 1y ago
  The tradeoff is not that simple (I wish it was :-). Usually it goes like that: someone made something useful optimised for a specific use-case with certain time (or competence) constraints, within a total lack of decent alternatives. Then people adopt and use it, it becomes the standard. Then people want to do more things with it, and try to build around that thing, or on top of that thing and Frankenstein monsters get born and also become standard. If you start from scratch you can do a crypto protocol that is both better designed (causes less UX pain and critical bugs) AND performs better on relevant hardware. Also do not forget that performance is easily solved by hardware: Moore's law and then custom hardware extensions are a thing. Example: Keccak is so much better from the composition perspective, that when used ubiquitously you'd definitely have ubiquitous hardware support. But if everyone continues to use a mishmash of AES and SHA constructions on the pretext of "Keccak" is not as fast, then we'd never move forward. People would continue building over-complicated protocols, bearing subpar performance and keeping the reputation of dark wizardry inaccessible for mere mortals.
  - eXpl0it3r 1y ago
    > Also do not forget that performance is easily solved by hardware: Moore's law "Just write slow algorithms, hardware will eventually get faster" doesn't really work when talking about performance implications now. If the hash algorithm used million of times doesn't perform on current user hardware, then the algorithm is simply not a good fit. > and then custom hardware extensions are a thing. That's the kind of trade-off I eluded to as well. As a developer of a tool (e.g. git), I'd pick hash algorithms that do have hardware extensions on the most common hardware and not use something, that may eventually get hardware extensions. I guess developing such protocols right now for the future might still be advisable, but it seems odd to critic software that use well-optimized algorithms and fulfill the requirements.

k__ 1y ago

Not really, but I liked this one. https://github.com/nakov/practical-cryptography-for-developers-book https://github.com/nakov/practical-cryptography-for-develope...

cvwright 1y ago

There are no proofs of the hardness of DDH or RSA etc. That’s why they’re called assumptions. OTOH if you want to win a Turing Award…

AnotherGoodName 1y ago
Just to add to the above for clarity a proof that key based encryption isn't reversible requires a proof of P!=NP which hasn't been done. That may surprise people but we have no proof of the robustness of the encryption we use. In fact it might not work! Consider a one time pad for really extreme security needs. One time pads do have a proof (see the work of Shannon).
- gary_0 1y ago
  Shor's algorithm suggests that a lot of encryption doesn't actually work, but of course it requires a quantum computer that hasn't yet been built, and may not be practical to build, so fingers crossed. At least there are quantum-resistant encryption algorithms, and OTPs are still provably secure like you say.
  - Tadpole9181 1y ago
    On "finger's crossed" - I think it's important to say that the majority of web traffic has switched over to PQC algorithms for key exchange that are not susceptible (thanks Cloudflare). We're not close to building a machine suitable for running Shor's in a practical sense, so even potential "store now, break later" attacks are now kinda pointless. Things like SSH keys are trivially revokable and often have enforced expirations, so they're not really a viable attack vector anyway. The symmetric encryption used for the vast majority of actual encryption has always been safe. Grover's algorithm does not scale appropriately (exponential on key length) unlike Shor's and cannot be parallelized. Worst case, AES-128 becomes as week as AES-64. So we bump it to AES-256 and we're back at the same difficulty as before (impossible). There's a degree of confidence this will always hold true.
vendiddy 1y ago
Can't someone learn this stuff with the assumption that certain functions are hard to invert? Like assuming f(x) is hard, let us try to prove these other properties of security.