PQCHacks: A gentle introduction to post-quantum cryptography
Daniel “djb” Bernstein & Tanja Lange.
Tanja and djb first had some soothing words: The D-wave quantum computer isn't universal:
- can't store stable qubits.
- can't perform basic qubit operations.
- can't do shor's algoritm.
...but universal quantum computers are coming and are very scary. They break all public-key crypto! AES-256 still hard, though.
Post-quantum crypto: the adversary has a quantum computer but we have ordinary computers.
PQcrypto conference 2006–2017.
There might be an entity (Ahem... NSA) that records all your communication. In 10 or 15 years you might be a Person of Interest. Then they break your RSA with their new quantum computer and read all your old correspondence.
Initial recommendations of long-term secure post-quantum systems
- symmetric - at least AES-256, Salsa20 with 256 bits.
- symmetric authentication, GSM, Poly1305.
- Public-key encryption, McEliece with binary goppa codes.
- Public-key signatures, hash-based signatures.
Lamport suggested one-time signatures in 79, Merkle extends to more signatures.
- a signature scheme for empty messages: key generation.
- a message that signs a panic button. a panic message.
For instance, use SHA3-256...
Can only send a single message. The message reveals the private key. And its hash is the public key.
A signature scheme for 1 bit messages: two private keys.
For 4 bits: 4 key pairs! Concatenate the public keys to create a new public key for the message.
Don't use the same secret key to sign two messages. Obviously, since we're revealing the private key when sending.
Lamports 1-time signature messages.
Merkle's 8-time signature system. Make 8 Lamport keys! And concate them and hash them. One hash is a public key, but many private keys.
- post-quantum secure!
- need secure hash function, nothing else. for instance SHA-3.
- small public key.
- security well understood
- proposed as an IETF standard.
- big signature
- stateful. You need to remember what private keys have been used. Imagine what happens if we restore from backup.
Solution to statefulness: eliminate the state! Build a big tree of certificate authorities:
- signature inclues cert chain
- each ca is a hash of master secret and tree position. deterministic so
don't need to store results
- random bottom-level ca signs message. many bottom-level cas, so one-time signature is safe.
- 0.6 MiB for a signature: Goldreich signature with good 1 time signature scheme.
- 0.041 MiB, 41 K! SPHINCS signature. https://sphincs.cr.yp.to/
Based on coding theory. Examples of coding theory are parity checks, the ISBN control number or Hamming code.
- -71 Goppa: Fast decoders for many matrices H.
- -78 McEliece Use Goppa codes for public-key cryptography.
- -86 Niederreiter: Simplified and smaller version of McEliece. public key: H with 1s on the diagonal secret key: fast goppa decoder encryption: randomly generate e with t bits set, send H # e.
Many more post-quantum suggestions
- qc-mdpc: smaller keys but is it secure?
- lattice based systems. some broken, some not.
- multivariate-quadratic systems. some broken, some not. highlight: very small signatures.
- isogeny-based crypto, ECC-like, supports DH.
Coming 2017 summer school and workshops.
@pqc_eu on Twitter.
Verified Firewall Ruleset Verification: Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL
Cornelius told us about mathematical machine proofs for firewall rules. He cited previous works and said “tools do not understand real-world firewall rules”.
Needs to specify "what is a firewall?" a model of the semantics of Linux iptables.
Using a theorem prover, Isabelle.
Builds a model of the firewall, the filtering behavior. Only 11 filter behaviours defined in the complete semantics.
This is a mathematical specification - not an implementation. It describes what a firewall does. The specification for CallReturn, for instance, didn't use a call stack but had a description of calls to new iptables call chains.
Why do this?
You can use it to prove “semantics-preserving simplification”, for instance prove that the firewall filtering behaviour stays the same after optimization or after having removed logging.
Specifications is done in Isabell, then exported to executable code. A selection of a languages: Haskell, for instance.