Re: [isabelle] Inductive Approach for Security Protocol Analysis



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


On 4 Apr 2014, at 09:43, kristof.teichel at ptb.de wrote:

> 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.