[noise] Security proofs for Noise

[Paul Rösler]

Hi everybody,

as we advertised it around RWC 19, we wrote reduction-based proofs for
many Noise patterns. We (Ben, Jörg, and me) finally published a preprint
of our resulting paper on eprint [1] (which is still under submission).
The main contributions of this paper are the proofs, a generic security
model (that can be reused for future analyses of protocols), and many
discussions about the idea behind single security properties. I'll
explain below, how far our results are complementary to the great
automated analysis by Nadim et al.

An interesting observation in our work is that, for a generic treatment
of protocols similar to Noise, it is necessary that the protocol itself
indicates to the environment during execution when a specific security
goal is reached. Otherwise it would be necessary to know how exactly the
analyzed protocol looks like, before defining what security for this
protocol means (which is not scientific). We therefore assumed that
Noise patterns output with every sent and received message an integer
that refers to a specific set of security properties, reached for the
transmission of the respectively transmitted message. Even though, this
integer can be mapped back to the round-trips in the protocol, the
round-trips themselves do to suffice for this.

Actually we think that such an indication of security is not only useful
for a formal security analysis, but could be used by upper-layer
applications to decide when to send a certain message. If someone agrees
that this would be a useful extension to Noise, we would be happy to
discuss further details.

Automated verifications and reduction-based proofs both have their pros
and cons such that we see them complementary with respect to the
security statements on Noise. Automated verifications are of course less
error-prone than manual pen and paper work. However, these verifications
treat the protocols' building blocks as black boxes independent of their
inputs' and outputs' representation. Computational proofs instead reduce
the security of the protocols to some well understood security
definitions and hardness assumptions on the underlying building blocks.
But while the statement of a reduction-based proof might be more
detailed, one cannot easily scale the approach and let machines do the
work. Thus, we now have a huge list of detailed security statements for
a lot of protocols due to the automated verification and a smaller but a
little bit more detailed list of security proofs for less protocols of
Noise due to our work.

Further interesting observations in our work regarding security
definitions and modeling are maybe not too interesting for the Noise
list. So if you have any comments, questions, or whatever on something
independent of Noise, just directly write us an email. For Noise related
comments the list would be a good place, I guess.

Cheers,
Paul

[1] https://eprint.iacr.org/2019/436.pdf

-- 
M.Sc. Paul Rösler
Horst Görtz Institute for IT-Security
Chair for Network and Data Security
Ruhr University Bochum, Germany

Universitätsstr. 150, ID 2/405
D-44801 Bochum, Germany

Telefon: +49 (0) 234 / 32-26728

https://nds.rub.de