Protocol Nonce Question
August 28th, 2007 By recluze

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.

1 Responses to " Protocol Nonce Question "
 
recluze
August 29th, 2007

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.

Leave a Reply


(Required)

(Required)