Introduction

More notes from my visit to 32C3. Part 1. Part 2. Part 3.

PQCHacks: A gentle introduction to post-quantum cryptography

Fahrplan link.

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.

Signature hashes

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.

Pros:

  • post-quantum secure!
  • need secure hash function, nothing else. for instance SHA-3.
  • small public key.
  • security well understood
  • fast
  • proposed as an IETF standard.

Cons:

  • 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.

Signature sizes:

  • 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/

Code-based encryption

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.

https://binary.cr.yp.to/mcbits.html/

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.

More

http://pqcrypto.org/

http://pqcrypto.eu.org/

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

Fahrplan link.

Cornelius Diekmann.

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.

Executable code

Specifications is done in Isabell, then exported to executable code. A selection of a languages: Haskell, for instance.

More

https://github.com/diekmann/Iptables_Semantics