Email Gateway (Aug 19 2022 at 14:08): Email Gateway (Aug 19 2022 at 14:08):From: kristof.teichel@ptb.de
Hello Isabellers,
I am part of a team seeking to develop a protocol with a lot of security
aspects. I have taken on the responsibility of performing a formal
verification of the security aspects. One of the methods I would really
like to employ is Larry Paulson's 'Inductive Approach' via Isabelle.
In parallel with the development, I have begun with modelling parts of the
protocol and proving some basic properties, mostly to get a feel for it.
Since I am new to most aspects of all this, it would be great if someone
was able and willing to help me out every now and again with some
beginner's aid.
My first concrete questions are these:
1) We are using keyed Hash signatures for authenticity. Is there already a
Theory treating authenticity goals via Hash signatures? If so, could
someone please point me to it?
I believe I have succeeded with proving the authenticity goal I had in
mind, but I had to start with the very basic facts like that no Hash value
is in the "initState" knowledge of any participant; I was feeling like
this had probably been treated somewhere before and I just couldn't find
it.
2) What would be a good way to model a (secret) random seed for each
agent? This seed shall be used to deterministically generate secrets in
the course of the protocol.
2a) Until I figure out a good answer to 2): If I do not wish to use the
"shrK" shared key that every agent possesses for its original purpose,
would it make sense to just divert this from its intended use and model
the seed(s) with it? The property that the "Server" entity (which will be
used by me to represent a Certificate Authority) then knows all the seeds
does not benefit me, nor does it mirror the true behaviour of the
participants. I suppose it won't hurt, but does anyone here think it is
a really bad idea anyway?
That's it for now. I would be thankful for any help, even just little
hints.
Regards
Kristof
Email Gateway (Aug 19 2022 at 14:09):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for your enquiry. The first thing to say is that I’m not sure that this old work is still the best way to prove protocols. I have seen more modern methods that seem to lead to simpler proofs, described for example in the following paper:
http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5552641&tag=1
On the other hand, I haven’t studied that work in detail and am not certain what it can and cannot do. The main advantage of the inductive method today is that, being based on little more than pure logic, you can adapt it to almost anything. The highly refined and effective verification methods that many people are using now may turn out to be too specialised to cope with a sort of protocol that hasn’t been seen before.
As regards the inductive method, proving authenticity properties isn’t that difficult compared with the effort of getting to grips with a typical protocol specification consisting of hundreds of pages of text. Secrecy properties tend to be much trickier, requiring very subtle invariants.
Turning to your questions:
1: I assume that by a keyed hash signature you mean hashing the plaintext, then encrypting it with a private key. Quite a few examples exist in the Isabelle distribution, above all in HOL/SET_Protocol. Papers about this work can be downloaded from http://www.cl.cam.ac.uk/~lp15/papers/Auth/
2: if the random seed in question is assumed to be an unguessable long-term secret, then you could represent it in exactly the same way as shrK. Probably you could use shrK itself, for example, if other secrets are generated by a hash chain starting from this. It isn’t strictly correct to say that the Server “knows” anything, in the sense that it cannot do anything with its “knowledge” other than to execute the protocol lawfully. Only the knowledge of the Spy is critical.
I hope you find all this useful.
Larry Paulson
Last updated: Apr 24 2024 at 20:16 UTC