[isabelle] Inductive Approach for Security Protocol Analysis
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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and