Cryptanalysis with Reasoning Systems

A Full Analysis of the 2015 GCHQ Crypto Puzzle

Today I would like to start the third article in a series on reasoning systems and declarative, executable specifications.  The material I prepared for this article on the 2015 GCHQ crypto puzzle was mothballed nearly a year ago now – and surely GCHQ will host a new puzzle this year. To date, I have not examined other people’s solution strategies as this would have spoiled the fun for me. I set out to solve this problem differently. I wanted to build a general solver, one that would not rely on the hints GCHQ so generously provided in the form of pre-filled parts of the puzzle, one that would work for other puzzles and which would demonstrate how problems with significant analytical complexity can be solved using declarative, functional programming techniques.

This is part 3 of a 3 part series. Part 1 is The Anatomy of a Puzzle. Part 2 is The Reasoned Lisper.

Background

GCHQ is the modern name for the British intelligence organisation once known as Bletchley Park. Bletchley Park is famous for the code breakers of the German Enigma cipher machine. Crypto puzzles are a true tradition at GCHQ.

screen-shot-2016-12-06-at-11-18-06-pm

How does the GCHQ crypto puzzle compare to the enigma cipher machine? In terms of pure analytical complexity, the Enigma had a significant number of internal states. The number of internal states of an Enigma machine was defined as:

screen-shot-2016-12-06-at-11-07-58-pm

Below is the 2015 GCHQ crypto puzzle.

gchq-puzzle

This represents a 25×25 matrix with 22 known squares. Each square may be black or white. This gives the following number of possible states:

screen-shot-2016-12-06-at-11-13-07-pm

Compare that to a 256 bit cipher:

screen-shot-2016-12-06-at-11-14-30-pm

Compare to the Enigma again:

screen-shot-2016-12-06-at-11-07-58-pm

How long then might it take to “brute force” the GCHQ problem? Here is a back of the envelope calculation. Assuming 10 nanosecond execution on a modern CPU, per combination, divide by the number of nanoseconds in a second, seconds in an hour, hours in a day, days in a year. This gives an expected runtime of 10526422041808708672025387782067887242548062486662701420587664458880397796582719803144868211433545901289187941682650403811251017441430175819094050822206909404011115685 years. This in intractable.

screen-shot-2016-12-07-at-7-26-18-am

This will have set the scene. Our aim is to build a purely functional solver, using a self executing specification of the problem. We will use the Common Lisp Screamer framework. Screamer is a reasoning framework that embodies a nondeterministic choice-point operator, and backtracking system. In simple terms, it allows systematic and efficient exploration of problems based on combinatorics.

A naive Analysis of the Problem

We start by recognising that the 2015 GCHQ crypto puzzle is a type of Run Length Encoding.

According to Wikipedia, Runlength encoding (RLE) is “a very simple form of lossless data compression in which runs of data (that is, sequences in which the same data value occurs in many consecutive data elements) are stored as a single data value and count, rather than as the original run.

We say a type of Run Length Encoding, because only runs of black squares in the matrix are enumerated. White squares are elided. This is the missing “key” information needed to solve the puzzle. If both black and white runs were specified, there would be no puzzle.

The puzzle canvas is a square matrix, which means that the number of rows equates to the number of columns. Let’s explore our problem domain with baby steps. Firstly, the site Solutions to Ninety-Nine Lisp Problems contains an exhaustive treatment of run length encoding in Lisp. The simplest, most elegant formulation is thus:

screen-shot-2016-12-07-at-7-45-10-am

This gives us the following example usage:

screen-shot-2016-12-07-at-7-46-24-am

This is kind of what we were looking for. 3 zeroes, 4 ones. Except in the GCHQ example, zeroes are not specified. We modify thusly:

screen-shot-2016-12-07-at-7-48-16-am

This gives the following corrected output on the previous example:

screen-shot-2016-12-07-at-7-51-53-am

Let’s play with this. We will encode a simple example as a toy problem that spells out “Hi” in a simple matrix. It’s easier to think about things in the small. In the below example, X denotes a black square and the underscore symbol denotes a white square.

screen-shot-2016-12-07-at-7-56-19-am

What can we say about our simple example, that will likewise hold true for any puzzle of this type? We can say that any given valid sequence of black and white squares, say “_X_X_X_” will encode to its relevant specification. That’s the requirement really. Given that we are looking at a matrix, how might we state this?  We might say something like, the solution is such that for all rows in the matrix, their encoding corresponds to the respective row specification and  for all rows of the transpose of the matrix, their  encoding corresponds to the respective column specification. If this is warranted, then our solution is valid.

If we want to entertain this route, we will need some utility functions. Firstly, the transpose of a matrix:

screen-shot-2016-12-07-at-8-05-11-am

Secondly we will want to visualise solutions in the REPL. So we will want something to render a matrix. We will let zero represent whitespace, one represent a black square and ? represent an unknown value as a sentinel represented as the digit 9. The Lisp “format” function is analogous to printf in C and C++. This will be, by necessity, a side-effecting function as it alters the state of the terminal. It will principally be our only function with side effects.

screen-shot-2016-12-07-at-8-08-32-am

We are not going to re-introduce Screamer. We already presented Screamer in an earlier article of this series: The Anatomy of a Puzzle. Instead we will go straight to the self execution specification of our toy problem.

screen-shot-2016-12-07-at-8-14-47-am

Let’s “talk this through.” We have defined ?x as a non-deterministic variable through macro expansion that will be some value between 0 and 1 ( white space or black square ). Then we said that a valid value for a matrix m ( one-value ) is one whereby m comprises a list of lists of ?x, whereby n is the transpose of m and we assert that each row in m must encode to its relevant specification and that each row in n must encode to its relevant specification.

Interesting is that we might just as well have defined a function, like so…

screen-shot-2016-12-09-at-3-32-06-pm

The nice thing about Lisp is that the syntax used in macros (meta programming) allows everything that regular functions allow. This gives us the choice of running arbitrary logic knowable at compile time within the compiler and deferring only runtime aspects to actual runtime – a very powerful language feature.

Note that ultimately the evaluation of our (one-value…) specification amounts to a decision tree. When a sub-branch fails, we backtrack and try another without exhausting possible choices in the failed branch — the essence of combinatorics. Here Screamer will do this for us.  That means we have no variables or mutable state in our solution. Or rather, what is variable is expressed as a valid range of “edge cases,” here ?x.  If this construct looks a lot like a unit test in an imperative language, then that is because it is as much test as it is implementation. I like to refer to this construct as “a self executing specification.”

How does Screamer build this “decision tree?” By deconstructing the entire expression between (one-value … the the closing parenthesis  ). This is owing to macros (meta programming) and the homoiconic nature of Lisp. Code I write here can be deemed data just the same by Screamer and thus be de-constructed as needed.

I would postulate that this is the differentiating factor between our solution to this problem and an imperative solution in a language such as C++ or Java or Python: The “code as data paradigm” gives rise to  logic interpreting logic within the same expression. Logic being an argument to logic is also referred to as higher order logic. Imperative programming languages, by contrast, tend to centre upon a clear delineation of code and data. Hence, in imperative programming, logic chiefly tends to interpret data. Yet it is the higher order logic that allows us to abstract away the combinatorics of the problem and just write out the specification logic.

Let’s execute our specification then…

screen-shot-2016-12-07-at-8-25-18-am

Success! Our toy example executed itself correctly.

We might go one step further and change one-value to all-values and count them (length).

screen-shot-2016-12-07-at-8-50-06-am

The answer is one. What this tells us is that our problem specification is unambiguous and our solution is total. Nothing has been missed. If you ever had to wonder in C++ if your unit test captured all possible edge cases, you will appreciate the simplicity of this. One key word changed and one key word added. Certainty attained.

While the example is simple and the analytic complexity is small, we will not depart from the spirit of what we have done here for larger examples. No classes, no state, no variables. In our treatment of NP-Hard problems and combinatorics in The Anatomy of a Puzzle we introduced how to use “generators” to compress the state space of the combinatorics of a problem. We will do the same here.

Getting Serious about Analytic Complexity 

Our aim is to reduce the analytic complexity of the problem. 

We will do this by defining a “generator” not for individual cells of the matrix — we previously had (an-integer-between 0 1) — but for entire rows ( there are only 25 ) and by providing our generator with the ability to filter based on known plaintext information. A known plaintext attack is an approach utilised in cryptanalysis that seeks to gain an advantage based on a priori knowledge of the solution.  Let’s define our new generator now so that we know what we are building up to.

screen-shot-2016-12-07-at-5-09-02-pm

The above states that a valid row in our matrix for a given row specification (optionally including a filter definition) must be a member of the set of valid rows that can be constructed for that row specification.

We note that what we have done here is to write down the requirements for a valid row — in code.

How then do we get to the set of valid rows?  Let’s think about this. Say we have a single row of length 5 and a row specification of ‘(3). What can we say about it? A little sketch might help here. As we have 5 spaces but only one block of 3 black squares with a consequent “2 degrees of freedom,” there are but three ways to arrange the existing free space.  One conclusion that arises is that the 3rd square must necessarily be black.

__img_20161207_16582102

We can generalise this. Given a row specification ‘(1 2 3) and a row length of 10, we can say that the distributable free space is the row length minus the sum of black squares: 1+2+3. We have white spaces 4 spaces to distribute  in such a way as to create between 2 and 5 gaps. We may have as few as two gaps between 3 blocks or if there are leading and trailing spaces there may be as many as 5 gaps.

This is simply a variation of the  Bin Packing Problem in Mathematics.

We formulate thusly.

screen-shot-2016-12-07-at-5-33-53-pm

This creates the definition of valid gaps.

screen-shot-2016-12-07-at-5-35-28-pm

And finally our definition for valid rows. This is what we sought for our generator.

screen-shot-2016-12-07-at-5-37-05-pm

There is but one piece missing. Our filter predicate as a lambda closure constructor.

screen-shot-2016-12-07-at-5-38-44-pm

Armed with the above, we can actually do some damage on the puzzle already.

Let’s go digging. 7th row of the puzzle.

screen-shot-2016-12-07-at-5-40-50-pm

It’s fully specified. There is but one solution. This row is done. How nice is that?

Anyone sitting in the 23rd row?

screen-shot-2016-12-07-at-5-43-46-pm

Again, this row is done. Let’s time this…

screen-shot-2016-12-07-at-5-44-47-pm

It was nearly too short to measure. 100 microseconds of CPU time and exactly 15368 CPU instructions running in the REPL – interpreted, not compiled.

How did I find which rows only had one solution? I did “cheat” a bit. I had a function that created a view on the analytical complexity of the matrix. Let’s build that. Firstly, let us define our initial plaintext matrix. If you recall, GCQH pre-filled some squares. We said “?” means unknown. “0″ means white and “1” means black.

screen-shot-2016-12-08-at-7-30-27-am

We also define the row specifications from the GCHQ picture of the puzzle. Effectively, we just write down the numbers as they are.

screen-shot-2016-12-08-at-7-45-03-am

Likewise for the columns:

screen-shot-2016-12-08-at-7-47-42-am

Now that we have the initial plaintext matrix, we can build our attack vector. We formulate thusly.

screen-shot-2016-12-08-at-7-40-47-am

This avails itself of two helpers (tomust1) and (tomust0). These are convenience functions that will take a sequence like “???11” or “0???” and produce “45” and “1” respectively. The assumption is plaintext sparseness and this makes it easer for the filter predicates to onboard terse values.

screen-shot-2016-12-08-at-7-56-02-am

We might refactor these into one since the logic is identical. It should be a macro since it is knowable at compile time and nothing that is knowable at compile time ought to be deferred to runtime. Doing this is left as an exercise to the reader.

At this point, we are free to build our complexity function. We formulate thusly:

screen-shot-2016-12-08-at-8-00-47-am

Let’s run it.

screen-shot-2016-12-08-at-8-03-09-am

And there we have it. The 7th row has an analytical complexity of 1. As does the 23rd row. We are still not in a very good shape. What is our overall analytical complexity?

screen-shot-2016-12-08-at-8-04-57-am

screen-shot-2016-12-08-at-8-05-49-am

We have come in below the analytical complexity of a 256 cipher.

screen-shot-2016-12-06-at-11-14-30-pm

But we are still far off the analytical complexity of a 128 bit cipher.

screen-shot-2016-12-08-at-8-07-38-am

Not good enough. My Macbook Air won’t crack the equivalent complexity of a 128 bit cipher in the expected lifetime of the device. How about our columns then? All we have to do is transpose our initial plaintext matrix. Rinse. Repeat.

screen-shot-2016-12-08-at-8-09-45-am

We have learned something interesting just now. There are exactly three columns that have an analytical complexity of 1. There is only one solution for them. We already know how to extract them – using the (valid-rows) function. Let’s feed the 3rd column specification to that function.

screen-shot-2016-12-08-at-8-16-20-am

If we continue to probe with our new toolset, we get many more pre-filled squares. Lather. Rinse. Repeat. Our new plain text matrix ends up looking something like this:

____foo

The Home Run

There is one thing we have not yet considered. Row constraints informing column constraints and column constraints informing row constraints in turn. Returning to our trivial example…

 

__img_20161207_16582102

How would our view on possible solutions be affected if separately a column specification fixed the last square to be black?  In other words if our “must1” specification said 4 ( zero based ), then only possibility 3 would be valid for this row. Only one solution would be possible. Even if we had but reduced the number of possibilities at all, we would still be ahead. Say we start with a “must0” specification of 0. That would rule out possibility 1 but leave possibilities 2 and 3. It is easy to imagine a situation where  our renewed understanding of the possible solutions for a row, further informs other columns. These columns inform other rows.

If we can formulate this as a function, we arrive at the mathematical concept of fixed point functions.

screen-shot-2016-12-08-at-8-35-52-am

We will write a function that takes on known plaintext and derives known plaintext. The function converges on a solution when it reaches its fixed point. Functional recursion is a natural fit here.

screen-shot-2016-12-08-at-8-41-17-am

We will use this function to build our new attack vector…

screen-shot-2016-12-08-at-8-44-34-am

The Solution… (break-puzzle)

The definition of the (break-puzzle) function is given below. At the top of the function we have our non-deterministic generator (a-valid-row-for) applied to each row using the attack vector we have constructed in our treatment of analytic complexity. This creates a non-deterministic matrix of rows, called m. n is its transpose.  We assert that each row of n, encodes to the correct specification. The overall structure has been preserved to show correspondence to our trivial example. Both encode the requirements in an executable specification. As before, no mutable state, no classes, no variables. Yet I ought to clean this up – at the very least roll-up the repetition. Apologies.

screen-shot-2016-12-08-at-9-22-57-am

screen-shot-2016-12-08-at-9-23-09-am

Let’s run our solver…

screen-shot-2016-12-08-at-9-29-14-am

Bingo !

Now the timed execution..

screen-shot-2016-12-08-at-9-31-21-am

What would have been a 10526422041808708672025387782067887242548062486662701420587664458880397796582719803144868211433545901289187941682650403811251017441430175819094050822206909404011115685 year problem, if brute-forced as a naive solution, has been reduced to  2.9 seconds.

There are also some spin-off benefits. The wording of the specification leans on what is termed universal quantification.

screen-shot-2016-12-08-at-6-18-17-pm

Quoting Wikipedia, “In predicate logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as “given any” or “for all”. It expresses that a propositional function can be satisfied by every member of a domain of discourse.

In other words we have said what must hold true for all matrices m, with rows & columns conforming  to the puzzle specification in terms of the “domain of discourse” and we have solved for that. The fact that only one result is returned is assurance that indeed only one result exists.

This gives us powerful reasoning abilities. For example, what would happen if we started with no known plaintext at all? What if GCHQ had not given us any pre-filled squares in the puzzle. Let’s find that out.

Firstly, we will define our initial plaintext matrix to contain question marks only – no black squares. We will start with a totally clean slate. We will call this *initial-without*.

screen-shot-2016-12-08-at-6-33-38-pm

We then construct a new attack vector for *initial-without*.

screen-shot-2016-12-08-at-6-35-03-pm

Firstly we note that our (derive-known-plaintext) function still converges on a fixed point. We expect one or more solutions to our puzzle. Let’s find out how many…

screen-shot-2016-12-08-at-6-40-42-pm

If we elide the knowledge of the pre-filled squares provided by GCHQ, there are exactly four solutions to the problem, no longer one unique solution. These are left to the reader as an exercise.

What we have acquired is a powerful “what if” analysis capability that allows us to reason about edge cases and total solutions with less than a handful of lines of code. It’s almost as if we had an SQL style (declarative) query capability into our problem, e.g. “select count(*) from AllSolutions,” that facilitates ad-hoc analysis of, in this case, a highly complex domain. This would not be the case for implementations where the problem domain has been transformed to an imperative abstraction, for example an object model. Because our representation is the problem specification itself, changes made at that level of abstraction are easy and quick.

We also observe a pattern in relation to the Project Euler problems we solved using the same technique in the article  The Anatomy of a Puzzle: There is a recurring pattern on how to solve problems of this kind:

  1. Specification of the problem through existential or universal quantification using higher order logic
  2. Domain generator functions that reduce state space
  3. Domain utility functions that embody the imperative logic of the domain

I would propose this as a design pattern for functional programming. It is summarised in this article on Specification Driven Programming.

I hope you have enjoyed this small exposé on cryptanalysis with Lisp.

 

screen-shot-2017-01-10-at-7-57-09-am

screen-shot-2017-01-10-at-7-56-09-am

 

 

 

 

 

 

 

Advertisements