SIP NOTES AND PROBLEMS
   These notes and problems are referred to by pointers in the Promela
   models.

NOTES

1  [RFC 3261, Section 15]
". . . the callee's UA MUST NOT send a BYE on a confirmed dialog until it
has received an ACK for its 2xx response or until the server transaction
times out."

2
A re-invite can be sent without an offer, which solicits an offer in the
successful response.  This capability is important for third-party call
control.
   RFC 3311 recommends using re-invites instead of updates in confirmed
dialogs, explaining the recommendation as follows: "This is because an
UPDATE needs to be answered immediately, ruling out the possibility of
user approval.  Such approval will frequently be needed, and is possible
with a re-INVITE."  The ability to solicit an offer, which also cannot be
done with an update, is another reason to use re-invite.

3
If a UA has received a re-invite with an offer, then replied to it with an
answer, the transaction is "terminated" [RFC 3261 terminology] and the UA
need not wait for the ack to send its own re-invite.  Thus the extra
precondition "ackDiff == 0" is not necessary.

4
As stated in Section 2 of "Understanding SIP Through Model-Checking", this
model is not intended to deal with network unreliability.  In addition to
the exclusions in that section, failure responses such as 481 and 408 that
indicate some kind of reliability problem are not included in this model.
As a consequence, in this model, the only responses to prack, cancel, info,
and bye requests are 200(OK) messages.

5 [RFC 3261, Section 15]
"The caller's UA MAY send a BYE for either confirmed or early dialogs, and
the callee's UA MAY send a BYE on confirmed dialogs, but MUST NOT send a
BYE on early dialogs."


PROBLEMS

1
An invite dialog is established by the first provisional or final success
response to the invite [RFC 3261, Section 12.1].  There is an implicit
assumption that if a message is part of a dialog, and the message does
not establish the dialog, then the message is received after the dialog
is established. 
   This info request was sent by the UAS after it sent a response to
establish the dialog, but it was received first by the UAC because the
messages were re-ordered in transit.  At this point the assemption about
messages in dialogs is violated.

2
RFC 3261, Section 9.2, is ambiguous on this behavior.  Its fourth paragraph
implies that a cancel request can get a 200(OK) response even if a final
response to the invite has already been sent.  But this violates the 
established definition that the invite transaction terminates in the UAS
when a successful response has been sent, so that 481 would be the correct
response. 
   As stated in Note 4, 481 responses are not included in this model.  This
model always sends a success response to the cancel.

3
A user agent might send ack,answer as part of a re-invite transaction, then
send invite,offer to begin a new re-invite transaction.  These messages
could arrive in the opposite order.  This scenario is not covered by the
RFCs, and it violates the clear intentions that offer/answer exchanges are
sequential, and that a re-invite can be processed as soon as it is 
received.
   The work-around used here is to buffer the second re-invite until the
answer arrives and is processed, then handle the new re-invite.
   The problem is in fact more general, because the "late" message carrying
an answer could also be a prackRsp, updSucc, or updFail.  For further 
information, see Section 4.5.2 of "Understanding SIP Through 
Model-Checking".

4
A relProv, offer has arrived, but it cannot be processed because there is
an unfinished offer/answer exchange begun by an update,offer or prack,offer
from the UAC.
   This problem is very similar to Problem 3.  It has the same cause 
(re-ordering of messages in transmission), is also not covered by RFCs, and
the same work-around (buffering).  For further information, see Section 
4.5.3 of "Understanding SIP Through Model-Checking".
   This problem is arguably more serious than Problem 3, because buffering
a relProv is less desirable than buffering a re-invite.  A user agent is
supposed to respond to a relProv message immediately, while it is allowed
to delay its response to a re-invite.

5
It is possible to have a race condition between an update from the UAC and
a re-invite from the UAS.  This possibility is not mentioned in the RFCs.
For further details on how the race occurs, see Section 4.5.4 of 
"Understanding SIP Through Model-Checking".
   The same work-around used for Problem 3, buffering the re-invite, also
solves this problem.

6
In an unconfirmed dialog, there can be a race condition between a 
relProv,offer message from the UAS, and an update message from the UAC.  
The resolution of this race condition is not standardized.
   There is a usual way of resolving race conditions in SIP.  In both 
re-invite/re-invite races and update/update races, both sides receive an 
invFail (4xx) response, then are allowed to retry with differing timing 
constraints.  This usual approach does not seem to be available in the case
of a relProv/update race, because a relProv is not a request, and there is
no failure response it.
   In the model, the work-around is that the relProv message always wins 
the race.  In the UAS, the update fails and an updFail response is sent. 
In the UAC, the relProv is buffered until updFail is received, after which
the relProv is handled normally.