[isabelle] Inductive Approach for Security Protocol Analysis



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.