I have a question and I was wondering if one of you security gurus can answer it.

There’s a lemma in the “Message” theory in Isabelle. It says, “In any message, there is an upper bound N on its greatest Nonce”.

In Isabelle:

lemma “Ex N. !!n. N <=n –> Nonce n ~: parts {msg}”

The lemma, translated to English says, “There exists an N such that for all Nonces, if N is less than the nonce, this greater Nonce is not in the message” or “there is a Nonce of number n which is not in the message”.

Can somebody shed some light on why this might be so? Or why we’re bothering with proving this?

Note: Isabelle protocol verification theory does not give any motivation for the lemmas it’s proving. It’s just going about merrily proving all sort of seemingly repetitive theorems.

Here’s a response I got from Larry Paulson regarding this post:

—

[snip]

Incidentally, I noticed the “Protocol Nonce Question” at <http://

securityengineering.wordpress.com/>. This lemma states that every

message contains at most finitely many nonces. It holds because

messages are finite. It’s only used to prove “possibility

properties”, which in turn merely show that a protocol execution can

occur.

Larry Paulson

—

I think the most important point to note here is that with a simple lemma, we’re proving an important property. That’s the way we need to convert all our property requirements to lemmas and break them down to simpler ones.

Hopefully, I’ll add more in this direction later.