Cryptography and Formal Methods
Research by
part of the EPSRC Research Network
CryptoForma (also
Facebook group
as informal home),
and also including external collaboration with
John Derrick
(Sheffield).
Summary
To investigate the application of formal methods to modern
cryptographic protocols.
Best recent paper
Two
published results however are the first paper on Approximate Refinement:
and
Issues
A modern cryptographic protocol may have the following properties:
- although its functionality is clear, its full set of desirable security properties may not be known yet;
- it contains probabilistic elements explicitly;
- its notion of security (correctness) is not an absolute one but
approximate;
- moreover, this approximate correctness is relative to the
computational resources of an attack against it (which tends to imply
an implicit probabilistic aspect);
- its security is not proved in an absolute sense but relative to
the hardness of some computational problem;
- it uses primitives in a way which does not guarantee
compositionality of the primitives' properties.
All this means that the standard techniques and good intentions from
formal methods don't work straight out of the box - all that is
needed really is a good timed probabilistic complexity-theoretic CSP
with fast converging approximate action refinement and a very rich set
of compositional algebraic properties.
Work and publications so far
- Originally more as an alternative to retrenchment, Eerke and John defined
Approximate Refinement, which is really refinement with clearly
demarcated compromise steps. See:
Research on this is ongoing, several draft papers exist and may appear
here
later.
- Dan's Phd work focused on a complete reconstruction of a complex
but basic proof concerning one-way functions: the theories required and
assumptions involved, and how this could be made more calculational.
The thesis is now (July 2010) even cited in the
wikipedia entry
for Las Vegas algorithms, which suggests that clear explanations may
indeed be thin on the ground in this research area.
- Eerke and Dan looked at how to make the theory of approximations
and limits more calculational.
- Dan and Eerke looked at the relation between refinement and
(complexity theoretic) reduction, leading to the generalised notion of
"refinement with contexts".
- Eerke looked at the cryptographic primitive of "commitment",
which turned out to be a pocket-sized case study of why formal methods
really needs to deal with all the "weird stuff" that cryptography tends
to come with.
- From ABZ to Cryptography is a short
pamphlet discussing the gap between state-based refinement methods and
what is necessary and possible in the cryptography area.
- Research proposals in other areas are in preparation.
Related projects