Subject: [Sip] INVITE dialogs

From: "Pamela Zave" <[email-masked]>
Date: Tue, 30 Sep 2008 15:09:28 -0400

I have created a formal model of invite dialogs in SIP.  The primary
purpose of this model is to bring together information from multiple
RFCs in a document that is centralized, unambiguous, and analyzable.

The formal language, Promela, is the input language for the model-checker
Spin.  The UAC and UAS are two finite-state machines sending messages to
each other through queues.  Promela is used in a straightforward style
that is easy to understand.

http://www.research.att.com/~pamela/sip.html contains three versions of
the model and a paper "Understanding SIP through model-checking" that
explains the work in detail.  The page also contains the results of
analysis.  The accompanying notes explain 6 small problems in the RFCs
and the workarounds I have used.

This material is made freely available for the benefit of the SIP
community.  Questions, comments, corrections and other feedback are
welcomed.

Pamela Zave
_______________________________________________
Sip mailing list  https://www.ietf.org/mailman/listinfo/sip
This list is for NEW development of the core SIP Protocol
Use [email-masked] for questions on current sip
Use [email-masked] for new developments on the application of sip

---

From: Paul Kyzivat <[email-masked]>
Date: Tue, 30 Sep 2008 16:35:46 -0400

Pamela,

This sounds interesting. I just skimmed the referenced web pages, and 
didn't take time to understand the details of the formalism, so I 
apologize if I have drawn the wrong conclusions.

I don't understand if the intent of this work is theoretical, or if it 
is intended as basis for a real implementation. If the latter, then some 
of the simplifying assumptions of your models probably need to be removed.

Of note, in many cases 3261 is less than clear, and some after the fact 
interpretation of the intent has had to be done. (You may consider this 
either discerning the intent of the Founders, or Judicial Activism, as 
you prefer.) One area where this has been done is around dialogs. It 
isn't entirely obvious, but is implicit in 3261+3265+3515 that you can 
have both an invite + a subscription, or multiple subscriptions sharing 
a dialog. RFC 5057 discusses this. In retrospect many people think it 
was a mistake to allow this, but it *is* used, in some limited ways, and 
probably cannot be removed. So in general you must be prepared to handle 
this. (Though you might be able to avoid it in some limited scope 
servers.) My fundamental is the introduction of the term "dialog usage" 
and its refinements: "invite dialog usage" and "subscribe dialog usage", 
and the partitioning of these from the notion of "dialog" which they 
share. I would think you should have the same partitioning in your models.

I then looked at your notes. I found it very interesting that through 
formal means you have identified a number of race conditions. I gather 
you are not aware of:

http://www.ietf.org/internet-drafts/draft-ietf-sipping-race-examples-06.txt

That document has been done without benefit of formal models. But it 
appears that there is substantial agreement about the set of race 
conditions. (I wish you had been around when we did that work.) That 
document is largely done, so it is likely impractical to get your input 
into it. But take a look. It has resolutions to most of the races. If 
you find any errors, please speak up.

	Thanks,
	Paul

Pamela Zave wrote:
> ------------------------------------------------------------------------
>