MC's Journal

32th Chaos Communication Congress, part 4

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:

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

Signature hashes

Lamport suggested one-time signatures in 79, Merkle extends to more signatures.

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:

Cons:

Solution to statefulness: eliminate the state! Build a big tree of certificate authorities:

Signature sizes:

Code-based encryption

Based on coding theory. Examples of coding theory are parity checks, the ISBN control number or Hamming code.

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

Many more post-quantum suggestions

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