Security Engineering Research Group

Protocol Nonce Question

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 Comment to Protocol Nonce Question

1. 

   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.
recluze on August 29th, 2007

Leave a comment