Email Gateway (Aug 22 2022 at 18:08): Email Gateway (Aug 22 2022 at 18:08):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Kristof, thanks for your email. I'll do my best to answer, but it's at least 15 years since I was working with this material.
The main reference connected with your question (e.g. authenticity of signed messages) is the original JCS paper:
https://www.cl.cam.ac.uk/~lp15/papers/Auth/jcs.pdf
The main examples distributed with Isabelle/HOL are OtwayRees.thy (for symmetric key protocols) and NS_Public.thy (for public key protocols). The message primitives such as synth and analz are defined in Message.thy.
All the proofs distributed here take the original approach, where little is protocol-independent other than the basic frameworks, which assume either a symmetric key or a public key environment (Public.thy). Other authors have further developed the approach to strengthen the protocol-independent side, and apparently much reducing the effort needed to verify protocols, but I'm not familiar with this work.
So with a protocol-dependent approach, it works because of the way the functions synth and analz are defined: they aren't able to generate nonces or keys, so in particular the Spy cannot do that. If you look at the proofs in NS_Public.thy, which is the famous Needham-Schroeder public key protocol, you'll see that the main tools are induction, simplification and basic automation (blast) with the theorem analz_insertI, which simply asserts Y ∈ analz H ⟹ Y ∈ analz (insert X H).
Larry Paulson
Email Gateway (Aug 22 2022 at 18:09):From: Kristof Teichel <k.teichel@gmail.com>
Hello Isabellers,
I am currently trying to finish up my dissertation project at PTB
(Germany's metrology institute) with the topic of of "design and formal
analysis of security measures for time synchronization protocols". For
this, I would really appreciate a few pointers towards authenticity proofs
with the Inductive Approach in Isabelle - and perhaps ideas on how best to
implement a few extensions that I will need.
Since 2014, I have been (on and off) tampering with the Inductive Approach
So, now for a few actual questions:
1) Where (if anywhere) in the source files can I find protocol-independent
proofs concerning authenticity of signed messages, specifically about the
impossibility of synthesis of signatures/message authentication codes
without knowledge of the proper key (or the exact, already authenticated
message itself)? Or is something like this simply not needed / not feasible
for some reason?
I ask because I have been stuck for ages whenever I attempted an
authentication goal, and I have recently discovered I was able to solve all
those problem with a simple lemma along the lines of "if attacker does not
know [key], then he cannot synthesize messages containing signature or MAC
using [key]" (with "sorry" cheat, just for proof-of-concept).
2) In general, what file might be a good starting point to import when
defining a new protocol that I want to obtain authentication proofs for?
There is lots of material, but I am somehow missing instruction on this
question.
Sorry for wall-of-text. I would be thankful for any help.
Best regards,
Kristof Teichel
P.S.: If anyone is interested and able to help, I would also like to go
more into the extensions that I need (namely, "runtime"-adjustable clocks
that let participants assign quantitative time values to events and
communicate those in messages). I am aware of the "Physical Properties"
extension attempt (https://beschmi.net/csf09.pdf), but for a few different
reasons, I do not think I will be able to use it and prefer instead to
incorporate my own extensions. This is the main reason why I like the
Inductive Approach so much: it is generic enough that I am pretty sure that
I should be able to somehow include these extras into it in a sensible way.
Email Gateway (Aug 22 2022 at 18:09):From: Kristof Teichel <k.teichel@gmail.com>
Thank you, Larry, for the info, as well as the quick and friendly response.
To give some additional context:
The JCS paper I have studied and consulted a fair amount over the years. It
has certainly been helpful.
I would say that I have a solid working knowledge (i.e. I know the
definitions and have a concept of roughly what lemmas/theorems are in
there) of the theory files up to and including Public.thy.
I have made modifications on Event.thy (and formerly Message.thy) and later
switched to extension of Event.thy, in order to account for real-time
clocks, for which I had to re-prove everything in there.
Overall, these activities have certainly given me the chance of studying
that material pretty carefully.
Recently, I have been successful using my extensions to define a few
dumbed-down protocols and proving executability and regularity goals on
those.
However, authenticity goals have been giving me headaches forever.
For some reason (probably mainly lack of skills with Isabelle syntax), I
have not been successful (before cheating with protocol-independent lemmas
as hinted at).
I guess I will go back to the Needham-Schroeder proofs and see if my
increased overall understanding since I last looked at those can give me
new input.
Let me ask a few more actual questions:
1) The protocols mostly use keyed Hash-MAC ("Hash[key] message") instead of
classical signatures for authentiction - would you suppose that had
something to do with my troubles (are these perhaps less friendly for
provability than straight-up signatures)?
2) Is there anyone still actively engaging in activities related to the
Inductive Approach who would possibly be willing to have an exchange about
the more intricate aspects of what I am trying to do? Or anyone who gives
anything tutorial-like on it?
Best regards,
Kristof
P.S.: Only recently did I discover that there were potentially valuable
extensions in the "Guard" subdirectory.
I am not yet familiar with any of the material really, but have given it a
scan. I did notice there are quite a few protocol-independent formulations
in there.
I was hoping you or Frédéric could shine some light on what these
extensions can and cannot do, specifically for authentication goals.
For some reason, I have neglected Frédéric's Paper (" An Isabelle
formalization of protocol-independent secrecy with an application to
e-commerce") on this so far, I will rectify that ASAP.
Email Gateway (Aug 22 2022 at 18:10):From: Lawrence Paulson <lp15@cam.ac.uk>
On 3 Aug 2018, at 15:24, Kristof Teichel <k.teichel@gmail.com> wrote:
1) The protocols mostly use keyed Hash-MAC ("Hash[key] message") instead of classical signatures for authentiction - would you suppose that had something to do with my troubles (are these perhaps less friendly for provability than straight-up signatures)?
The recursive authentication protocol uses the same method. It is also described in the JCS paper and formalised as Recur.thy.
2) Is there anyone still actively engaging in activities related to the Inductive Approach who would possibly be willing to have an exchange about the more intricate aspects of what I am trying to do? Or anyone who gives anything tutorial-like on it?
I see new papers appearing from time to time but I'm afraid I haven't studied any of them.
Email Gateway (Aug 22 2022 at 18:11):From: Jean Martina <jean.martina@cl.cam.ac.uk>
The issue here is that Hash-MAC are not actual signatures. They provide
a weaker form of authentication. All the authentication proofs for
digital signatures in the standard theories, will be too strong for
that. The authentication Hash-MAC provide can only be available to the
recipient of the message based on the fact that that "Hash[key] message"
was not seen before by him. It is not available to anyone else. This
makes some other proofs tricky.
If you analyse the authenticity proofs for Needham-Schroeder Shared Key
Protocol and compare them with Needham-Schroeder Public Key Protocol,
you will see that they yield different things, although both are called
authenticity. Definitely, what you need is the weaker form that is used
in NSSKP since you are using a shared key.
Regards,
Jean
signature.asc
Email Gateway (Aug 22 2022 at 18:11):From: Kristof Teichel <k.teichel@gmail.com>
Hey Jean,
nice to hear from you again.
That's a very interesting distinction you're pointing out.
I've compared the two Needham-Schroder files and also taken a look at
Recur.thy.
I will absolutely keep it mind for my formalizations and proofs.
Best regards,
Kristof
Last updated: Apr 25 2024 at 04:18 UTC