Internet DRAFT - draft-cuda-sipping-ua-fsm

draft-cuda-sipping-ua-fsm







Network Working Group                                            A. Cuda
Internet-Draft                                                E. Marocco
Expires: July 20, 2006                                    Telecom Italia
                                                        January 16, 2006


      A Formal Model for Media Negotiation between SIP User Agents
                    draft-cuda-sipping-ua-fsm-00.txt

Status of this Memo

   By submitting this Internet-Draft, each author represents that any
   applicable patent or other IPR claims of which he or she is aware
   have been or will be disclosed, and any of which he or she becomes
   aware will be disclosed, in accordance with Section 6 of BCP 79.

   Internet-Drafts are working documents of the Internet Engineering
   Task Force (IETF), its areas, and its working groups.  Note that
   other groups may also distribute working documents as Internet-
   Drafts.

   Internet-Drafts are draft documents valid for a maximum of six months
   and may be updated, replaced, or obsoleted by other documents at any
   time.  It is inappropriate to use Internet-Drafts as reference
   material or to cite them other than as "work in progress."

   The list of current Internet-Drafts can be accessed at
   http://www.ietf.org/ietf/1id-abstracts.txt.

   The list of Internet-Draft Shadow Directories can be accessed at
   http://www.ietf.org/shadow.html.

   This Internet-Draft will expire on July 20, 2006.

Copyright Notice

   Copyright (C) The Internet Society (2006).

Abstract

   This document provides a formal description of the interactions
   between two SIP User Agents establishing a multimedia session,
   describing the negotiation of the two parties as an exchange of
   signals between two instances of networks of Finite State Machines
   (FSMs).

   The goal is to provide a common reference model for both SIP
   extensions and User Agent implementations: two flows that can be



Cuda & Marocco            Expires July 20, 2006                 [Page 1]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   implemented by using the external interface of the FSMs are
   guaranteed not to conflict to each other.  On the other hand a
   reference model for User Agents is expected to improve
   interoperability between different implementations and help
   implementors to model their software in a way that makes SIP
   extensions conforming to this document easier to implement.


Table of Contents

   1.  Requirements notation  . . . . . . . . . . . . . . . . . . . .  3
   2.  Scope and Purposes of This Document  . . . . . . . . . . . . .  4
   3.  Naming and Conventions . . . . . . . . . . . . . . . . . . . .  5
   4.  State Machines Interfaces  . . . . . . . . . . . . . . . . . .  8
     4.1.  External Interfaces  . . . . . . . . . . . . . . . . . . .  8
       4.1.1.  Grouping Events into Interfaces  . . . . . . . . . . .  8
       4.1.2.  FSM Tasks  . . . . . . . . . . . . . . . . . . . . . .  9
       4.1.3.  The Signalling Interface (ifcS)  . . . . . . . . . . . 12
       4.1.4.  The Session Interface (ifcI) . . . . . . . . . . . . . 13
       4.1.5.  The Negotiation Interfaces (ifcN)  . . . . . . . . . . 14
       4.1.6.  Rules of Composition . . . . . . . . . . . . . . . . . 15
     4.2.  Internal Interfaces  . . . . . . . . . . . . . . . . . . . 17
       4.2.1.  Which Interactions are Needed  . . . . . . . . . . . . 17
       4.2.2.  Synchronization-Signalling Interface (ifcU)  . . . . . 17
       4.2.3.  Session-Synchronization Interface (ifcA) . . . . . . . 19
     4.3.  Session-Negotiation Interface (ifcV) . . . . . . . . . . . 19
   5.  State Machine Definition . . . . . . . . . . . . . . . . . . . 21
     5.1.  Session State Machine  . . . . . . . . . . . . . . . . . . 21
     5.2.  Negotiation State Machine  . . . . . . . . . . . . . . . . 22
     5.3.  Synchronization State Machine  . . . . . . . . . . . . . . 24
     5.4.  Signalling State Machine . . . . . . . . . . . . . . . . . 27
       5.4.1.  Overall State Machine  . . . . . . . . . . . . . . . . 27
       5.4.2.  Scope State Machine  . . . . . . . . . . . . . . . . . 30
       5.4.3.  Prop State Machine . . . . . . . . . . . . . . . . . . 37
   6.  Open Issues  . . . . . . . . . . . . . . . . . . . . . . . . . 39
   7.  Security Considerations  . . . . . . . . . . . . . . . . . . . 40
   8.  References . . . . . . . . . . . . . . . . . . . . . . . . . . 40
   Authors' Addresses . . . . . . . . . . . . . . . . . . . . . . . . 41
   Intellectual Property and Copyright Statements . . . . . . . . . . 42












Cuda & Marocco            Expires July 20, 2006                 [Page 2]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


1.  Requirements notation

   The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
   "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this
   document are to be interpreted as described in [RFC2119].














































Cuda & Marocco            Expires July 20, 2006                 [Page 3]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


2.  Scope and Purposes of This Document

   SIP [RFC3261] is a protocol that allows to establish, control and
   terminate multimedia sessions.  As such, negotiation (specified in
   [RFC3264]) is one of its most fundamental tasks, and the need to
   provide features like resource reservation or early media streaming
   makes the protocol operations quite hard to design.  For these
   purposes, a number of SIP mechanisms have been added to the baseline
   protocol, like UPDATE ([RFC3311]) and PRACK ([RFC3262]).  All these
   RFCs leave many options to implementors and, despite the effort to
   define the best current practices ([I-D.sawada-sipping-sip-
   offeranswer]) this represents a serious threat for interoperability
   and a challenge for User Agent implementors.

   The purpose of this document is to provide a formal description of
   the SIP negotiation process, which can be used as a guideline for
   both SIP extensions authors and for User Agent implementors, as well
   as a base for SIP test suites.  The formalism chosen for this
   document is a network of Finite State Machines communicating each
   other through signals: as such, it models a software layer between
   the SIP transaction layer (see [RFC3261]), and the application
   controlling the negotiation.  However, the purpose is not to specify
   a negotiation API, nor to give a formal description of the
   interactions between the Transaction User and the Transaction Layer:
   these aspects are treated just in the measure that is needed to
   define a number of signals between the State Machines and the
   Transaction Layer and between the State Machines and the Application.
   Finally, even though this document tries to keep the negotiation
   interface as SIP-unaware as possible, it is not meant to provide a
   protocol-independent negotiation mechanism.





















Cuda & Marocco            Expires July 20, 2006                 [Page 4]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


3.  Naming and Conventions

   The following paragraphs will build the State Machine network
   starting from its external interfaces and breaking the overall system
   into subsystem as new functional entities are isolated.  Subsystems
   are modeled as Finite State Machines and interactions between them
   are represented by messages received from an external interface or
   generated by a state transition and fed to another state machine or
   sent towards an external interface.  The system may therefore be
   depicted as follows:

                        | FSM Network         |
                      |||||||||||||||||||||||||||
                        |           : ifcB    |
                   ifcA |         <-:->       | ifcC
                      <-+->  FSM    :       <-+->
                        |     A     :         |
                        |           :   FSM   |
         Application    |...........:    B    |    Transaction
            Layer       |           :         |       Layer
                        |           :         |
                        |   ///     :         |
                        |           :         |
                        |           :         |
                      |||||||||||||||||||||||||||
                        |                     |

   Figure 1

   In the figure above ifcA and ifcC are external interfaces, while ifcB
   is an internal interface.  An internal interface is uniquely
   identified by the couple of FSMs it is connected to.  An external
   interface is identified by the layer (i.e. application or
   transaction) and the FSM it connects to.

   Event propagation happens atomically and transactionally through all
   the interfaces.  Suppose, for instance, that an event through ifcA
   causes a transition in FSM A and triggers an event through ifcB.  If
   that event is illegal in the current state of FSM B, the transition
   in FSM A does not take place and the event in ifcA fails too.  This
   property greately simplifies interactions between FSMs, however if a
   state transition triggers multiple events, it can be quite hard to
   keep track all the events indirectly generated and be prepared to
   roll back all of them if someone fails.  This can be a source of
   ambiguities, so it will be avoided as much as possible and introduced
   only when the very nature of SIP negotiation mandates them.  An
   explanatory note will be added whenever this happens, to describe how
   the rollback procedure should behave.



Cuda & Marocco            Expires July 20, 2006                 [Page 5]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   An event is a message sent and or received by a FSM.  It belongs to
   one and only one interface and it is identified by a string in the
   form:

                        <ifc><direction>_<name>

   where:

   o  ifc is a single letter which uniquely identifies the interface

   o  direction identifies the direction of the signal.  It can be
      either "u" (upstream), if moving from the transaction layer
      towards the application layer or "d" (downstream) if moving in the
      opposite direction.

   o  name is the name of the event

   In some cases, it is not possible to give an event a definite
   direction.  For instance if two state machines should synchronize
   each other in order to generate a composite event, they need to
   generate events that do not fall in a "downstream" nor in an
   "upstream" category.  These events' direction flag will therefore be
   "x", i.e. their label will be in the form:

                        <ifc>x_<name>

   These events have different nature than those whose direction can be
   clearly identified, so in the remainder of this document we well
   refer to them as "non-negotiation" events, in contrast to
   "negotiation" events whose direction of propagation can unambiguously
   defined to be upstream or downstream.

   Events belonging to the interface between the FSM networks and the
   transaction layer will be defined in couples sharing the same "name"
   identifier: one event moving upstream and the other moving
   downstream.  When, as a result of the interconnection of two User
   Agents, their respective FSM networks (n1 and n2) are connected to
   each other, a downstream event generated by n1 towards the
   transaction layer, will cause the transaction layer of n2 to deliver
   the upstream event to n2, and vice versa.  In the example of figure
   Figure 1, if n1 generates the event "cd_example" (belonging to
   interface ifcC), then n2 will receive an event "cu_example".

   This property can be extended to all the negotiation events, and it
   is useful as a consistency check: all the FSMs must be built in a way
   that if two networks are interconnected to each other an event "Xd_Y"
   on one network must (directly or indirectly) originate an event
   "Xu_Y" on the other network.  Note, however, that this does not hold



Cuda & Marocco            Expires July 20, 2006                 [Page 6]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   true for non-negotiation signals.

   [TODO: Explain better difference between negotiation and non-
   negotiation events]















































Cuda & Marocco            Expires July 20, 2006                 [Page 7]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


4.  State Machines Interfaces

4.1.  External Interfaces

4.1.1.  Grouping Events into Interfaces

   The first step is to identify which events are needed to interact
   with the two networks.  Events need be grouped into interfaces
   according to which FSMs they are delivered to, so choosing to group
   signals according to different arrangements leads to different FSM
   configurations.  In particular, it is important that events related
   to the same set of transactions belong to the same interface.  In
   addition, to keep state machines as simple as possible, events
   related to different sets of transactions must belong to different
   interfaces.

   Strictly speaking, this document only relates to the negotiation
   state machine, so on the application side, only events related to
   negotiation should be considered.  It is true, however, that in SIP
   negotiation and session establishement are so intimately related
   (since they are provided by the same method, i.e.  INVITE) that also
   session related events should be taken into consideration.

   The strong liaison between session negotiation and session
   establishement is however just a feature of the protocol, so while
   the two sets of events simply can't be separated on the Transaction
   Layer side, it is an useful abstraction to keep them on different
   interfaces on the Application side.  If we accept these design
   choices, a first sketch of the system is:

                        | FSM Network               |
                      ||||||||||||||||||||||||||||||||
                        |             :             |
                   ifcI |             :             | ifcS
                      <-+-> Session   :           <-+->
                        |     FSM     : Signalling  |
                        |             :     FSM     |
         Application    |.............:             |    Transaction
            Layer       |             :             |       Layer
                        | Negotiation :             |
                   ifcN |     FSM     :             |
                      <-+->           :             |
                        |             :             |
                      |||||||||||||||||||||||||||||||||
                        |                           |

   Figure 4




Cuda & Marocco            Expires July 20, 2006                 [Page 8]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   Where mutual relationships between state machines, i.e. internal
   interfaces, are deliberately left out.

4.1.2.  FSM Tasks

   It is important, at this stage, to define clearly which tasks these
   FSMs must accomplish, and which ones they must not, to avoid gaps and
   overlaps in their interfaces and behaviour.  As a general rule:

   o  The Signalling State machine must handle all the events coming
      from the Transaction Layer, translating them into events that are
      as least SIP-related as possible.  In doing this, however, it must
      not take decisions that could affect the negotiation process.  For
      instance, it must not automatically send an ACK request when
      receiving an 2xx INVITE response because the Negotiation FSM might
      need to insert a session descriptor to complete negotiation
      exchanges;

   o  The Session State Machine must translate events coming from the
      Signalling State Machine into pure session-related events (i.e.
      without any negotiation implications) and vice versa.  As such, it
      is part of its core logic processing the initial INVITE
      transaction, the BYE transaction and other session-related
      messages;

   o  The Negotiation State Machine must translate events coming from
      the Signalling State Machine into pure negotiation-related events
      (i.e. without any session-related implications) and vice versa.
      As such, it is part of its core logic processing session
      descriptors contained in re-INVITE, PRACK and UPDATE messages;

   One questionable point is whether the Session State Machine must be
   involved when processing re-INVITEs or not.  From a purely functional
   point of view, the answer should be "no", since a re-INVITE is not
   relevant for session life (e.g. if it fails, the communication is not
   torn down).  However, everything which is allowed inside of an INVITE
   request (like UPDATE, PRACK) is also allowed in re-INVITEs, so having
   the session state machine process them simplifies the state machines
   because it can avoid some redundancy by reusing part of the logic.
   This is therefore the approach we will follow in this document.

   When trying to put the three state machines together, the most
   relevant issue to solve is how to combine session and negotiation
   events into a single signalling event.  For instance, when sending
   the initial INVITE, if a session descriptor must be provided, the
   session and negotiation events must be properly coordinated in order
   to build the initial INVITE request.




Cuda & Marocco            Expires July 20, 2006                 [Page 9]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


              +-------+   +-------+               +-------+
              | ifc I |   | ifc N |               | ifc S |
              +-------+   +-------+               +-------+
                  |           |                       |
     Formulate an offer       |  ^^^^^^^^^^^^^^^^^^^. |
     ------------------------>| {  Synchronization  } |
     Place a call |           | {       Logic       } |
     ------------>|           | {                   } |
                  |           |  vvvvvvvvvvvvvvvvvvv  | INVITE + SD
                  |           |                       |-------->

   Figure 5

   The same happens on the UAS side: if an incoming INVITE is received,
   there must be a way for the application to reply 200 with a session
   descriptor:

              +-------+   +-------+               +-------+
              | ifc I |   | ifc N |               | ifc S |
              +-------+   +-------+               +-------+
                  |           |                       |
                  |           |                       |
                  |           |                       | INVITE
                  |      (Events get propagated)      |<-----------
     Incoming call|<=================================>|
     <------------|           |                       |
                  |           |                       |
     Formulate an offer       |  ^^^^^^^^^^^^^^^^^^^. |
     ------------------------>| {  Synchronization  } |
     Accept call  |           | {       Logic       } |
     ------------>|           | {                   } |
                  |           |  vvvvvvvvvvvvvvvvvvv  | 200 Ok + SD
                  |           |                       |------------>

   Figure 6

   Here the problem is even more complex, since there must be a way for
   the application to choose whether to put the session descriptor into
   the 2xx response or in some provisional response sent beforehand.
   The complexity comes from the fact that the two events from the
   Application are the same as the ones in the previous scenario.










Cuda & Marocco            Expires July 20, 2006                [Page 10]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


              +-------+   +-------+               +-------+
              | ifc I |   | ifc N |               | ifc S |
              +-------+   +-------+               +-------+
                  |           |                       |
                  |           |                       |
                  |           |                       | INVITE
                  |      (Events get propagated)      |<-----------
     Incoming call|<=================================>|
     <------------|           |                       |
                  |           |                       |
     Formulate an offer       |  ^^^^^^^^^^^^^^^^^^^. |
     ------------------------>| {  Synchronization  } | 183 + SD
     Accept call  |           | {       Logic       } |------------>
     ------------>|           | {                   } |
                  |           |  vvvvvvvvvvvvvvvvvvv  | 200 Ok + SD
                  |           |                       |------------>

   Figure 7

   A possible solution of this problem is to put the synchronization
   logic into the application, and define events into ifcI that affect
   both session and negotiation.  Another option consists in putting the
   synchronization inside of the FSM network and defining a convention
   on the order in which events are generated.

   Both solutions are viable, but they suffer from a common
   disadvantage: they inevitably put some negotiation logic into the
   session FSM and/or some session logic into the negotiation.  The
   first approach leads to a simpler interface for the application
   because there are no sequencing rules apart from those that are
   intrinsic to the negotiation process.  The other approach, on the
   other hand, requires some extra conventions on the Application side,
   however the resulting state machines are simpler and less redundant.

   Keeping state machines as simple as possible is one of the primary
   goals of this document, so the second apporach looks more promising,
   however another important goal is to avoid as much as possible the
   situation in which a task is partly performed by a state machine and
   partly in another.  To mitigate this, a new state machine whose only
   task is to synchronize and compose outbound events, as well as to
   decomponse inbound events is added.










Cuda & Marocco            Expires July 20, 2006                [Page 11]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


                   | FSM Network                         |
                 |||||||||||||||||||||||||||||||||||||||||||
                   |             :                       |
              ifcI |             :     Signalling        | ifcS
                 <-+-> Session   :       FSM           <-+->
                   |     FSM     :                       |
                   |         ...................         |
                   |         :                 :         |
                   |         : Synchronization :         |
    Application    |.........:       FSM       :         |   Transaction
       Layer       |         :                 :         |      Layer
                   |         :.................:         |
                   |             :                       |
                   | Negotiation :                       |
              ifcN |     FSM     :                       |
                 <-+->           :                       |
                   |             :                       |
                 |||||||||||||||||||||||||||||||||||||||||||
                   |                                     |

   Figure 8

   Having done this, it is important to define this "extra" protocol
   between the Application and the state machines, i.e. what's the order
   of signals applied to the ifcI and ifcN interfaces that will be
   interpreted by the FSM network as a request to send a specific event
   (e.g. issue an INVITE request with a session descriptor), or another
   (e.g. issue an INVITE request without session descriptor).  This
   can't be done at this point because events are not defined yet: it
   will be however discussed right after defining external interfaces
   (see Section 4.1.6).

4.1.3.  The Signalling Interface (ifcS)

   The ifcS interface is the easiest to define, since it is just an
   event-oriented abstraction of the interface between the Transaction
   Layer and the Transaction User Layer, which is defined in [RFC3261].

   It is not a complete mapping, of course , and most of the details are
   out of scope, so the following events suffice for our purposes:











Cuda & Marocco            Expires July 20, 2006                [Page 12]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +------------------------+-----------------+------------------------+
   | event                  | With proposal   | Without proposal       |
   +------------------------+-----------------+------------------------+
   | INVITE                 | s[du]_invite_sd | s[du]_invite           |
   |                        |                 |                        |
   | reINVITE               | s[du]_invite_sd | s[du]_invite           |
   |                        |                 |                        |
   | INVITE provisional     | s[du]_1xxi_sd   | n/a                    |
   | answer                 |                 |                        |
   |                        |                 |                        |
   | INVITE success         | s[du]_2xxi_sd   | s[du]_2xxi             |
   | response               |                 |                        |
   |                        |                 |                        |
   | INVITE failure         | n/a             | s[du]_Xxxi             |
   | response               |                 |                        |
   |                        |                 |                        |
   | ACK                    | s[du]_ack_sd    | s[du]_ack              |
   |                        |                 |                        |
   | PRACK                  | s[du]_prack_sd  | s[du]_prack            |
   |                        |                 |                        |
   | PRACK success response | s[du]_2xxp_sd   | s[du]_2xxp             |
   |                        |                 |                        |
   | PRACK failure response | n/a             | s[du]_Xxxp             |
   |                        |                 |                        |
   | UPDATE                 | s[du]_update_sd | n/a                    |
   |                        |                 |                        |
   | UPDATE success         | s[du]_2xxu_sd   | UPDATE failure         |
   | response               |                 | response               |
   |                        |                 |                        |
   | n/a                    | s[du]_Xxxu      | CANCEL                 |
   |                        |                 |                        |
   | n/a                    | s[du]_cancel    | BYE                    |
   |                        |                 |                        |
   | n/a                    | s[du]_bye       |                        |
   +------------------------+-----------------+------------------------+

   The most common form of proposal is an SDP body inside of a message
   body.  However the format needs not be SDP and some other kind of
   negotiation may be implied by future extensions of the SIP protocol
   without affecting the model.

4.1.4.  The Session Interface (ifcI)

   On the application side, events are not that straightforward to
   define, since this interface is outside the scope of the SIP core
   specification, and also the separation between the session interface
   and the negotiation interface is convenient but in some ways
   arbitrary.



Cuda & Marocco            Expires July 20, 2006                [Page 13]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   The set of events we propose for IfcI is:

                   +--------------------+--------------+
                   | Event              | Name         |
                   +--------------------+--------------+
                   | Open a new session | i[du]_create |
                   |                    |              |
                   | Close a session    | i[du]_close  |
                   |                    |              |
                   | Accept a session   | i[du]_accept |
                   +--------------------+--------------+

4.1.5.  The Negotiation Interfaces (ifcN)

   The negotiation handshake is essentially a sequence of offers and
   answers, so this interface allows to formulate offers and reply with
   answers.  Once an offer is received, the Application must react
   immediately, by rejecting it or answering with a new session
   descriptor.

   Given the flexibility in SIP negotiation, an offer and an answer can
   be urgent or not:

      An urgent offer or answer is immediately delivered to the other
      party;

      A non-urgent offer is deferred until the session is established.

   The scenario in which this distinction is most clear is when an
   INVITE request is received: if it contains a session descriptor, the
   Application might already be able to formulate an answer, but this
   does not necessarily mean that it is willing to send it immediately.
   Depending on the fact that the answer is tagged as "urgent" or not,
   the session descriptor will be encapsulated into an ad-hoc 183
   reliable response or it is deferred until the user answers (i.e. it
   will be encapsulated into the 2xx response).

   Non-urgent proposals may be updated by an urgent proposal, or by
   another non-urgent proposal.  The former event "clears" the proposal
   and forces delivery of the proposal to the other endpoint.  The
   latter does not cause a state switch but it only updates the session
   descriptor.

   Urgency of offers is a purely applicative characteristic, and cannot
   be stated independently by the Negotiation state machine, therefore
   some specific events need to be introduced:





Cuda & Marocco            Expires July 20, 2006                [Page 14]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


     +-------------------------------------------+------------------+
     | Event                                     | Name             |
     +-------------------------------------------+------------------+
     | Make an urgent offer                      | n[du]_urg_offer  |
     |                                           |                  |
     | Make an offer                             | n[du]_offer      |
     |                                           |                  |
     | Make an interactive offer                 | n[du]_int_offer  |
     |                                           |                  |
     | Accept an offer and send an urgent answer | n[du]_urg_answer |
     |                                           |                  |
     | Accept an offer and send an answer        | n[du]_answer     |
     |                                           |                  |
     | Accept an answer                          | n[du]_accept     |
     |                                           |                  |
     | Reject an offer                           | n[du]_reject     |
     +-------------------------------------------+------------------+

   The difference between an interactive offer and a non interactive
   offer is in whether the session update request must be approved by
   the other endpoint's user or not.  An interactive offer must be
   mapped into an INVITE transaction and a non-interactive proposal into
   an UPDATE transaction.  Interactive negotiations can only happen once
   the session has been fully established, and are always urgent (since
   they immediately generate a re-INVITE request).

   Accepting an answer by sending nd_accept acknowledges its reception.
   This event is needed because, in SIP, transaction related messages
   can carry session descriptors.  For instance, if a 18x INVITE
   response containing a session descriptor is received, the Signalling
   State Machine must be able to tell whether the PRACK request shall
   contain a session descriptor or not.  If, as a result of delivering
   the vu_answer event to the application, it receives a vd_offer event,
   it will encapsulate a session descriptor in the PRACK request.  If it
   receives an vd_accept event, the PRACK request won't contain any
   session descriptor.

   [TODO: Clarify with example]

4.1.6.  Rules of Composition

   As anticipated in Section 4.1.2, the interface between the FSM
   network and the external world is ambiguous unless complemented by a
   set of rules describing when and how session and negotiation events
   must be composed into a single signalling event.

   Cases that could raise ambiguities are summarized in the table below:




Cuda & Marocco            Expires July 20, 2006                [Page 15]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


              +---+-----------+-------------+--------------+
              |   | Session   | Negotiation | Signalling   |
              +---+-----------+-------------+--------------+
              | 1 | id_create | nd_offer    | sd_invite_sd |
              |   |           |             |              |
              | 2 | id_create | -           | sd_invite    |
              |   |           |             |              |
              | 3 | id_accept | nd_*        | sd_2xxi_sd   |
              |   |           |             |              |
              | 4 | -         | nd_*        | sd_1xxi_sd   |
              +---+-----------+-------------+--------------+

                                  Table 4

   Cases (1) and (2) happen when establishing an outbount call, in the
   scenario of Figure 5.  There is no such ambiguity when sending a re-
   INVITE, because it is triggered by a single event (nd_int_offer), so
   the simplest solution seems to give a meaning to the order in which
   signalling and negotiation events are generated:

                +---+---------------------+--------------+
                |   | Events              | Signalling   |
                +---+---------------------+--------------+
                | 1 | nd_offer, id_create | sd_invite_sd |
                |   |                     |              |
                | 2 | id_create           | sd_invite    |
                +---+---------------------+--------------+

   The difference between an urgent proposal and a non-urgent proposal
   is meaningless in case (1), so it seems natural to forbid urgent
   proposals at this stage.

   Cases (3) and (4), instead, can be disambiguated thanks to the
   "urgency mechanism": an urgent answer will immediately trigger a 183
   response (Figure 7, while a non urgent answer will wait for the
   id_accept event to be composed with:

                +-----+----------------------+------------+
                |     | Events               | Signalling |
                +-----+----------------------+------------+
                | 3'  | nd_offer, id_accept  | sd_2xxi_sd |
                |     |                      |            |
                | 3'' | nd_answer, id_accept | sd_2xxi_sd |
                |     |                      |            |
                | 4'  | nd_urg_offer         | sd_1xxi_sd |
                |     |                      |            |
                | 4'' | nd_urg_answer        | sd_1xxi_sd |
                +-----+----------------------+------------+



Cuda & Marocco            Expires July 20, 2006                [Page 16]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


4.2.  Internal Interfaces

4.2.1.  Which Interactions are Needed

   In the FSM network, the Synchronization State Machine plays a central
   role: it must receive events from the Session and Negotiation State
   Machines, compose them if necessarily and deliver the resulting
   events to the Signalling State Machine.  Conversely, it must receive
   composite events from the Signalling State Machine and break them
   into pure session and negotiation events.

   To accomplish these tasks, the Synchronization State Machine needs an
   interface towards each other state machine.  It seems therefore
   natural to treat this FSM as an hub, delivering all the events
   (including those that do not need composition nor descomposition)
   from one FSM to another.  Following this approach, the internal
   structure becomes:

                   | FSM Network                         |
                 |||||||||||||||||||||||||||||||||||||||||||
                   |             :                       |
              ifcI |             :     Signalling        | ifcS
                 <-+-> Session   :       FSM           <-+->
                   |     FSM     :                       |
                   |         ...................         |
                   |       <-+->               :         |
                   |    IfcA : Synchronization :         |
    Application    |.........:       FSM       : IfcU    |   Transaction
       Layer       |       <-+->             <-+->       |      Layer
                   |    IfcV :.................:         |
                   |             :                       |
                   | Negotiation :                       |
              ifcN |     FSM     :                       |
                 <-+->           :                       |
                   |             :                       |
                 |||||||||||||||||||||||||||||||||||||||||||
                   |                                     |

   Figure 9

4.2.2.  Synchronization-Signalling Interface (ifcU)

   The ifcU interface is primarly the interface that the Signalling FSM
   exposes, so the events that should be exchanged there provide the
   highest possible abstraction of SIP transactions without knowledge of
   the distinction between the session and the negotiation part.

   In the model we propose, offers and answers (collectively called



Cuda & Marocco            Expires July 20, 2006                [Page 17]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   "proposals" from now on) may be exchanged inside or outside of a
   "negotiation scope".  Negotiation scopes carry no semantic meaning:
   proposals belonging to the same scope do not need having anything in
   common, however they must complete before the scope is closed.  On
   the transaction layer interface, negotiation scopes map to INVITE and
   reINVITE transactions, while negotiations map to UPDATE and PRACK
   transactions.  This abstraction is useful to define the life of an
   instance of the Signalling state machine, which spans the life of
   negotiation scope or a single negotiation in case scopes are not
   used.  There is actually an important difference between a
   negotiation scope created by an INVITE and one created by a reINVITE,
   since the former has some additional limitations in messages that can
   be exchanged until a confirmed dialog is established.  To inform the
   Signalling State machine about this difference, specific events for
   the dialog-establishing negotiation scopes and for in-dialog
   negotiation scopes are defined.

   Given that, this is the list of events which are needed on the ifcU
   interface:

   +------------------------------------------------+------------------+
   | Event                                          | Name             |
   +------------------------------------------------+------------------+
   | Create the negotiation scope and establish     | u[du]_open       |
   | dialog                                         |                  |
   |                                                |                  |
   | Create a negotiation scope, make proposal and  | u[du]_open_pro   |
   | establish dialog                               |                  |
   |                                                |                  |
   | Create in dialog negotiation scope             | u[du]_reopen     |
   |                                                |                  |
   | Create in dialog negotiation scope and make    | u[du]_reopen_pro |
   | proposal                                       |                  |
   |                                                |                  |
   | Close a negotiation scope                      | u[du]_close      |
   |                                                |                  |
   | Close a negotiation scope and make a proposal  | u[du]_close_pro  |
   |                                                |                  |
   | Abort an outbound negotiation scope            | u[du]_cancel     |
   |                                                |                  |
   | Abort an inbound negotiation scope             | u[du]_decline    |
   |                                                |                  |
   | Send a proposal                                | u[du]_propose    |
   |                                                |                  |
   | Accept a proposal                              | u[du]_accept     |
   |                                                |                  |
   | Reject a proposal                              | u[du]_reject     |
   |                                                |                  |



Cuda & Marocco            Expires July 20, 2006                [Page 18]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   | Terminate session                              | u[du]_end_sesson |
   +------------------------------------------------+------------------+

   Accepting a proposal by sending ud_accept carries the same meaning of
   the corresponding signal in the ifcN interface.

4.2.3.  Session-Synchronization Interface (ifcA)

   The ifcA interface is the result of the decomposition of the events
   of the ifcU interface operated by the Synchronization State Machine.
   In particular, it must contain:

   +------------------------------------------------+------------------+
   | Event                                          | Name             |
   +------------------------------------------------+------------------+
   | Create a negotiation scope and establish       | a[du]_open       |
   | dialog                                         |                  |
   |                                                |                  |
   | Create an in dialog negotiation scope          | a[du]_reopen     |
   |                                                |                  |
   | Close a negotiation scope                      | a[du]_close      |
   |                                                |                  |
   | Abort an outbound negotiation scope            | a[du]_cancel     |
   |                                                |                  |
   | Abort an inbound negotiation scope             | a[du]_decline    |
   |                                                |                  |
   | Terminate session                              | a[du]_end_sesson |
   +------------------------------------------------+------------------+

   The meaning of these events is the same of the couterparts in the
   ifcU interface.

4.3.  Session-Negotiation Interface (ifcV)

   By applying the same rule, this interface can be made to comprise
   very few events.  To keep the model as simple as possible, there is
   not even a distinction between an offer and an answer: all the events
   are generic proposals.  It will be up to the negotiation state
   machine to make sure that offers are properly coupled with answers:












Cuda & Marocco            Expires July 20, 2006                [Page 19]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


        +------------------------------------+-------------------+
        | Event                              | Name              |
        +------------------------------------+-------------------+
        | Make or receive a proposal         | v[du]_propose     |
        |                                    |                   |
        | Make or receive an urgent proposal | v[du]_urg_propose |
        |                                    |                   |
        | Accept a proposal                  | v[du]_accept      |
        |                                    |                   |
        | Reject a proposal                  | v[du]_reject      |
        +------------------------------------+-------------------+

   The definition of urgent answer (and offer) also applies to
   proposals.





































Cuda & Marocco            Expires July 20, 2006                [Page 20]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


5.  State Machine Definition

5.1.  Session State Machine

   A Session State Machine is created:

   o  By the Application, when establishing an outgoing call;

   o  By the Synchronization State Machine, when an inbound call request
      is received

   In both cases, the initial state of this state machine is INIT.  When
   servicing an inbound call, the state machine enters the INBOUND
   state; when an outbound call is attempted, the state machine enters
   the OUTBOUND state instead.  Depending on the outcome of the inbound
   or outbound call, it can enter the ESTABLISHED or the TERM state.

   A graphical representation of this state machine is:

                               +---------+
                               |  INIT   |
                               +---------+
                                 |     |
                         +-------+     +-------+
                         |                     |
                         v                     v
                   +----------+           +---------+
                   | OUTBOUND |           | INBOUND |
                   +----------+           +---------+
                         |                     |
                         +-------+     +-------+
                         |       |     |       |
                         |       v     v       |
                         |   +-------------+   |
                         |   | ESTABLISHED |   |
                         |   +-------------+   |
                         |          |          |
                         |          v          |
                         |   +-------------+   |
                         +-->|    TERM     |<--+
                             +-------------+










Cuda & Marocco            Expires July 20, 2006                [Page 21]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +-----------+-------------+-------------+-------------+-------------+
   |           | INIT        | INBOUND     | OUTBOUND    | ESTAB       |
   +-----------+-------------+-------------+-------------+-------------+
   | id_create | OUTBOUND /  | - / e(500)  | - / e(500)  | - / e(500)  |
   |           | ad_open     |             |             |             |
   |           |             |             |             |             |
   | id_close  | - / e(481)  | TERM /      | TERM /      | TERM /      |
   |           |             | ad_decline  | ad_cancel   | ad_hangup   |
   |           |             |             |             |             |
   | id_accept | - / e(481)  | ESTAB /     | - / e(500)  | - / e(500)  |
   |           |             | ad_close    |             |             |
   +-----------+-------------+-------------+-------------+-------------+

            State transition table for events coming from ifcI

   +------------+--------------+-----------+--------------+------------+
   |            | INIT         | INBOUND   | OUTBOUND     | ESTAB      |
   +------------+--------------+-----------+--------------+------------+
   | au_open    | INBOUND /    | - /       | - / e(491)   | - / E      |
   |            | iu_create    | e(500)    |              |            |
   |            |              |           |              |            |
   | au_reopen  | - / E(481)   | - /       | - / e(491)   | - /        |
   |            |              | e(500)    |              | [t.b.i]    |
   |            |              |           |              |            |
   | au_close   | - / e(481)   | - / E     | ESTAB /      | - / E      |
   |            |              |           | iu_accept    |            |
   |            |              |           |              |            |
   | au_cancel  | - / e(481)   | TERM /    | - / e(481)   | - / E      |
   |            |              | iu_close  |              |            |
   |            |              |           |              |            |
   | au_decline | - / e(481)   | - /       | TERM /       | - / E      |
   |            |              | e(481)    | iu_close     |            |
   |            |              |           |              |            |
   | au_hangup  | - / e(481)   | TERM /    | TERM /       | TERM /     |
   |            |              | iu_close  | iu_close     | iu_close   |
   +------------+--------------+-----------+--------------+------------+

            State transition table for events coming from ifcA

5.2.  Negotiation State Machine

   A Session State Machine does not need to last longer than an offer,
   since its main task is to keep track of offers and couple them with
   their corresponding answers.  It is therefore created:

   o  By the Application, when formulating a new offer;





Cuda & Marocco            Expires July 20, 2006                [Page 22]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   o  By the Signalling State Machine, when an inbound offer is received

   When created, it enters the INIT state, immediately switching the the
   OFFERING or ANSWERING state depending on the direction of the offer.
   When the negotiation completes, the FSM enters the TERM state and is
   destroyed.

                               +---------+
                               |   INIT  |
                               +---------+
                                 |     |
                         +-------+     +-------+
                         |                     |
                         v                     |
                   +----------+                |
                   | OFFERING |-----+          v
                   +----------+     |    +-----------+
                      |    ^        |    | ANSWERING |
                      v    |        |    +-----------+
                   +----------+     |          |
                   | CLOSING  |     |          |
                   +----------+     |          |
                         |          |          |
                         +-------+  |  +-------+
                                 |  |  |
                                 v  v  v
                             +-------------+
                             |    TERM     |
                             +-------------+

   +--------------+-------------+----------+-------------+-------------+
   |              | INIT        | OFFERING | ANSWERING   | CLOSING     |
   +--------------+-------------+----------+-------------+-------------+
   | nd_offer     | OFFERING /  | - /      | - / e(491)  | OFFERING /  |
   |              | vd_prop     | e(500)   |             | vd_prop     |
   |              |             |          |             |             |
   | nd_answer    | - / e(481)  | - /      | TERM /      | - / e(481)  |
   |              |             | e(481)   | vd_prop     |             |
   |              |             |          |             |             |
   | nd_accept    | - / e(481)  | - /      | - / e(481)  | TERM /      |
   |              |             | e(481)   |             | vd_accept   |
   |              |             |          |             |             |
   | nd_reject    | - / e(481)  | - /      | TERM /      | - / e(481)  |
   |              |             | e(481)   | vd_reject   |             |
   |              |             |          |             |             |
   | nd_urg_offer | OFFERING /  | - /      | - / e(491)  | OFFERING /  |
   |              | vd_urg_prop | e(500)   |             | vd_urg_prop |
   |              |             |          |             |             |



Cuda & Marocco            Expires July 20, 2006                [Page 23]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   | nd_urg_answ  | - / e(481)  | - /      | TERM /      | - / e(481)  |
   |              |             | e(481)   | vd_urg_prop |             |
   +--------------+-------------+----------+-------------+-------------+

            State transition table for events coming from ifcN

   +------------+----------------+---------------+-----------+---------+
   |            | INIT           | OFFERING      | ANSWERING | CLOSING |
   +------------+----------------+---------------+-----------+---------+
   | vu_propose | ANSWERING /    | CLOSING /     | - /       | - /     |
   |            | nu_offer       | nu_answer     | e(491)    | e(500)  |
   |            |                |               |           |         |
   | vu_urg_pro | ANSWERING /    | TERM /        | - /       | - /     |
   |            | nu_offer       | nu_answer     | e(500)    | e(500)  |
   |            |                |               |           |         |
   | vu_accept  | - / -          | - / E         | - /       | - /     |
   |            |                |               | e(500)    | e(500)  |
   |            |                |               |           |         |
   | vu_reject  | - / E          | TERM /        | - /       | - /     |
   |            |                | nu_reject     | e(500)    | e(500)  |
   +------------+----------------+---------------+-----------+---------+

            State transition table for events coming from ifcV

5.3.  Synchronization State Machine

   The Synchronization State Machine is created:

   o  By the Session State Machiine when establishing an outgoing call;

   o  By the Signalling State Machine, when an inbound call request is
      received

   The only task of this state machine is to compose and decompose
   events.  Decomposing events does not imply synchronization, therefore
   it does not cause any state switch.  On the other hand, composition
   is needed only before the dialog has been completely established.
   That's why, once session is established, there is no further need for
   synchronization, and events are simply "tunnelled" from Session and
   Negotiation State Machines towards the Signalling State Machine, and
   vice versa.

   The resulting state machine is fairly simple: when created it enters
   the IDLE state.  The state machine must be prepared to receive non-
   urgent proposals before session is established.  In that case it must
   "buffer" the session descriptor, waiting for an outbound message
   which can vehicle it.  To keep track of this, the state machine
   enters the PROPOSAL state until the session is established.



Cuda & Marocco            Expires July 20, 2006                [Page 24]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   Disambiguation of cases in Table 4 is operated in the same way: cases
   (1) and (3) are seen as non-urgent proposals formulated before
   session is fully established, so they cause a switch to the PROPOSAL
   state.  The difference between the two cases only lies in the ifcI
   event that clears the state, which is an outbound call attempt for
   case (1) and an inbound call answer for case (3).

                               +---------+
                               |  IDLE   |
                               +---------+
                                 |     ^
                                 |     |
                         +-------+     +-------+
                         |                     |
                         v                     v
                   +----------+          +----------+
                   |   RELAY  |<---------| PROPOSAL |
                   +----------+          +----------+


   +------------+----------------+---------------------+---------------+
   |            | IDLE           | PROPOSAL            | RELAY         |
   +------------+----------------+---------------------+---------------+
   | ad_open    | - / ud_open    | IDLE / ud_open_pro  | - / ud_open   |
   |            |                |                     |               |
   | ad_reopen  | - / ud_reopen  | IDLE /              | - / ud_reopen |
   |            |                | ud_reopen_pro       |               |
   |            |                |                     |               |
   | ad_close   | RELAY /        | RELAY /             | - / ud_close  |
   |            | ud_close       | ud_close_pro        |               |
   |            |                |                     |               |
   | ad_cancel  | - / ud_cancel  | - / ud_cancel       | - / ud_cancel |
   |            |                |                     |               |
   | ad_decline | - / ud_decline | - / ud_decline      | - /           |
   |            |                |                     | ud_decline    |
   |            |                |                     |               |
   | ad_hangup  | - / ud_hangup  | - / ud_hangup       | - / ud_hangup |
   +------------+----------------+---------------------+---------------+

            State transition table for events coming from ifcA











Cuda & Marocco            Expires July 20, 2006                [Page 25]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +----------------+----------------+---------------+----------------+
   |                | IDLE           | PROPOSAL      | RELAY          |
   +----------------+----------------+---------------+----------------+
   | vd_propose     | PROPOSAL / -   | - / e(500)    | - / ud_propose |
   |                |                |               |                |
   | vd_urg_propose | - / ud_propose | - / e(500)    | - / ud_propose |
   |                |                |               |                |
   | vd_accept      | - / ud_accept  | - / ud_accept | - / ud_accept  |
   |                |                |               |                |
   | vd_reject      | - / ud_reject  | - / ud_reject | - / ud_reject  |
   +----------------+----------------+---------------+----------------+

            State transition table for events coming from ifcV

   +---------------+------------------+---------------+----------------+
   |               | IDLE             | PROPOSAL      | RELAY          |
   +---------------+------------------+---------------+----------------+
   | uu_open       | - / au_open      | - / au_open   | - / au_open    |
   |               |                  |               |                |
   | uu_reopen     | - / au_reopen    | - / au_reopen | - / au_reopen  |
   |               |                  |               |                |
   | uu_open_pro   | - / vu_propose,  | - /           | - /            |
   |               | au_open          | vu_propose,   | vu_propose,    |
   |               |                  | au_open       | au_open        |
   |               |                  |               |                |
   | uu_reopen_pro | - /              | - /           | - /            |
   |               | au_reopen_pro    | au_reopen_pro | au_reopen_pro  |
   |               |                  |               |                |
   | uu_close      | RELAY / au_close | - / e(491)    | - / au_close   |
   |               |                  |               |                |
   | uu_close_pro  | RELAY /          | - / e(419)    | - /            |
   |               | vu_propose,      |               | vu_propose,    |
   |               | au_close         |               | au_close       |
   |               |                  |               |                |
   | uu_cancel     | - / au_cancel    | - / au_cancel | - / au_cancel  |
   |               |                  |               |                |
   | uu_decline    | - / au_decline   | - /           | - / au_decline |
   |               |                  | au_decline    |                |
   |               |                  |               |                |
   | uu_propose    | - / vu_propose   | - /           | - / vu_propose |
   |               |                  | vu_propose    |                |
   |               |                  |               |                |
   | uu_accept     | - / vu_accept    | - / vu_accept | - / vu_accept  |
   |               |                  |               |                |
   | uu_reject     | - / vu_reject    | - / vu_reject | - / vu_reject  |
   |               |                  |               |                |
   | uu_hangup     | - / au_hangup    | - / au_hangup | - / au_hangup  |
   +---------------+------------------+---------------+----------------+



Cuda & Marocco            Expires July 20, 2006                [Page 26]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


            State transition table for events coming from ifcU

5.4.  Signalling State Machine

5.4.1.  Overall State Machine

   The Signalling State Machine is created:

   o  By the Session State Machine when establishing an outgoing call;

   o  By the Transaction Layer, when an inbound INVITE request is
      received

   If this FSM is created to exchange proposals inside of a negotiation
   scope, its life is limited to that negotiation scope.  If it is
   created to exchange proposals outside of a negotiation scope, it is
   limited to that proposal.

   Though the behaviour is essentially the same, this distinction leads
   to two different state machines, which are discussed separately for
   clarity purposes.  The overall machine can however be sketched like
   this:

                               +----------+
                               | INIITIAL |
                               +----------+
                                 |      |
                                 |      |
                         +-------+      +-------+
                         |                      |
                         v                      v
                   +===========+           +==========+
                   | SCOPE_FSM |           | PROP_FSM |
                   +===========+           +==========+

















Cuda & Marocco            Expires July 20, 2006                [Page 27]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


            +---------------+---------------------------------+
            |               | INIT                            |
            +---------------+---------------------------------+
            | ud_open       | SCOPE_FSM.INIT / sd_invite      |
            |               |                                 |
            | ud_open_pro   | SCOPE_FSM.INIT / sd_invite_sd   |
            |               |                                 |
            | ud_reopen     | SCOPE_FSM.IDLE / sd_reinvite    |
            |               |                                 |
            | ud_reopen_pro | SCOPE_FSM.IDLE / sd_reinvite_sd |
            |               |                                 |
            | ud_close      | - / e(481)                      |
            |               |                                 |
            | ud_close_pro  | - / e(481)                      |
            |               |                                 |
            | ud_cancel     | - / e(481)                      |
            |               |                                 |
            | ud_decline    | - / e(481)                      |
            |               |                                 |
            | ud_propose    | PROP_FSM.INIT / sd_update_sd    |
            |               |                                 |
            | ud_accept     | - / e(481)                      |
            |               |                                 |
            | ud_reject     | - / e (481)                     |
            |               |                                 |
            | ud_hangup     | TERM / sd_bye                   |
            +---------------+---------------------------------+

            State transition table for events coming from ifcU.

             +----------------+------------------------------+
             |                | INIT                         |
             +----------------+------------------------------+
             | su_invite_sd   | SCOPE_FSM.INIT / uu_open_pro |
             |                |                              |
             | su_invite      | SCOPE_FSM.INIT / uu_open     |
             |                |                              |
             | su_reinvite_sd | SCOPE_FSM.IDLE / uu_open_pro |
             |                |                              |
             | su_reinvite    | SCOPE_FSM.IDLE / uu_open     |
             |                |                              |
             | su_1xxi_sd     | - / e(481)                   |
             |                |                              |
             | su_1xxi        | - / e(481)                   |
             |                |                              |
             | su_1xxirel_sd  | - / e(481)                   |
             |                |                              |
             | su_1xxirel     | - / e(481)                   |



Cuda & Marocco            Expires July 20, 2006                [Page 28]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


             | su_2xxi_sd     | - / e(481)                   |
             |                |                              |
             | su_2xxi        | - / e(481)                   |
             |                |                              |
             | su_Xxxi        | - / e(481)                   |
             |                |                              |
             | su_ack_sd      | - / e(481)                   |
             |                |                              |
             | su_ack         | - / e(481)                   |
             |                |                              |
             | su_prack_sd    | - / e(481)                   |
             |                |                              |
             | su_prack       | - / e(481)                   |
             |                |                              |
             | su_2xxp_sd     | - / e(481)                   |
             |                |                              |
             | su_2xxp        | - / e(481)                   |
             |                |                              |
             | su_Xxxp        | - / e(481)                   |
             |                |                              |
             | su_update_sd   | PROP_FSM.INIT / uu_propose   |
             |                |                              |
             | su_2xxu_sd     | - / e(481)                   |
             |                |                              |
             | su_Xxxu        | - / e(481)                   |
             |                |                              |
             | su_cancel      | - / e(481)                   |
             |                |                              |
             | su_bye         | TERM / uu_hangup             |
             +----------------+------------------------------+

            State transition table for events coming from ifcS.



















Cuda & Marocco            Expires July 20, 2006                [Page 29]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


5.4.2.  Scope State Machine


                               +----------+
                               |   INIT   |--------------------------+
                               +----------+                          |
                                  |    |                             |
                        +---------+    +-------+                     |
                        |                      |                     |
                        v                      v                     |
                   +------------+        +-----------+               |
                   |  PROV_OUT  |        | PRACK_OUT |               |
                   +------------+        +-----------+               |
                         ^                     ^                     |
                         |                     |                     |
                         +-------+     +-------+                     |
                                 |     |                             |
                                 v     v                             |
      +------------+           +---------+           +------------+  |
      | UPDATE_IN  |<--------->|   IDLE  |<--------->| UPDATE_OUT |  |
      +------------+           +---------+           +------------+  |
                                 ^  |  ^  \_________________         |
                                 |  |  |                    |        |
                         +-------+  |  +-------+            |        |
                         |          |          |            |        |
                         v          |          v            |        |
                   +-----------+    |     +----------+      |        |
                   |  PROV_IN  |    |     | PRACK_IN |      |        |
                   +-----------+    |     +----------+      |        |
                                    |                       |        |
                                    v                       v        |
                               +----------+           +----------+   |
                               | ACCEPTED |---------->|   TERM   |<--+
                               +----------+           +----------+   |
                                    ^                                |
                                    |                                |
                                    +--------------------------------+














Cuda & Marocco            Expires July 20, 2006                [Page 30]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +--------------+----------------+--------------------+--------------+
   |              | INIT           | IDLE               | ACCEPTED     |
   +--------------+----------------+--------------------+--------------+
   | ud_open      | - / E          | - / E              | - / E        |
   |              |                |                    |              |
   | ud_open_pro  | - / E          | - / E              | - / E        |
   |              |                |                    |              |
   | ud_close     | ACCEPTED /     | ACCEPTED / sd_2xxi | - / E        |
   |              | sd_2xxi        |                    |              |
   |              |                |                    |              |
   | ud_close_pro | ACCEPTED /     | ACCEPTED /         | - / E        |
   |              | sd_2xxi_sd     | sd_2xxi_sd         |              |
   |              |                |                    |              |
   | ud_cancel    | - / E          | TERM / sd_cancel   | - / E        |
   |              |                |                    |              |
   | ud_decline   | - / E          | TERM / sd_Xxxi     | - / E        |
   |              |                |                    |              |
   | ud_propose   | PROV_OUT /     | UPDATE_OUT /       | TERM /       |
   |              | sd_1xx_sd      | sd_update_sd       | sd_ack_sd    |
   |              |                |                    |              |
   | ud_accept    | - / E          | - / -              | TERM /       |
   |              |                |                    | sd_ack       |
   |              |                |                    |              |
   | ud_reject    | - / E          | - / e(500)         | - / e(488)   |
   |              |                |                    |              |
   | ud_hangup    | - / E          | - / E              | TERM /       |
   |              |                |                    | sd_bye       |
   +--------------+----------------+--------------------+--------------+

         State transition table for events coming from ifcU (1/3).





















Cuda & Marocco            Expires July 20, 2006                [Page 31]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +--------------+--------------+-----------------+-------------------+
   |              | PROV_IN      | PROV_OUT        | PRACK_IN          |
   +--------------+--------------+-----------------+-------------------+
   | ud_open      | - / E        | - / E           | - / E             |
   |              |              |                 |                   |
   | ud_open_pro  | - / E        | - / E           | - / E             |
   |              |              |                 |                   |
   | ud_close     | - / E        | ACCEPTED /      | ACCEPTED /        |
   |              |              | sd_2xxi         | sd_2xxp, sd_2xxi  |
   |              |              |                 |                   |
   | ud_close_pro | - / E        | ACCEPTED /      | ACCEPTED /        |
   |              |              | sd_2xxi_sd      | sd_2xxp,          |
   |              |              |                 | sd_2xxi_sd        |
   |              |              |                 |                   |
   | ud_cancel    | TERM /       | - / E           | - / E             |
   |              | sd_cancel    |                 |                   |
   |              |              |                 |                   |
   | ud_decline   | - / E        | TERM / sd_Xxxi  | TERM / sd_Xxxi    |
   |              |              |                 |                   |
   | ud_propose   | PRACK_OUT /  | UPDATE_OUT /    | IDLE / sd_2xxp_sd |
   |              | sd_prack_sd  | sd_update_sd    |                   |
   |              |              |                 |                   |
   | ud_accept    | PRACK_OUT /  | - / E           | IDLE / sd_2xxp    |
   |              | sd_prack     |                 |                   |
   |              |              |                 |                   |
   | ud_reject    | - / e(488)   | - / E           | IDLE / sd_Xxxp    |
   |              |              |                 |                   |
   | ud_hangup    | - / e(500)   | - / E           | - / E             |
   +--------------+--------------+-----------------+-------------------+

         State transition table for events coming from ifcU (2/3).




















Cuda & Marocco            Expires July 20, 2006                [Page 32]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +--------------+----------------+---------------------+-------------+
   |              | PRACK_OUT      | UPDATE_IN           | UPDATE_OUT  |
   +--------------+----------------+---------------------+-------------+
   | ud_open      | - / E          | - / E               | - / E       |
   |              |                |                     |             |
   | ud_open_pro  | - / E          | - / E               | - / E       |
   |              |                |                     |             |
   | ud_close     | - / E          | ACCEPTED / sd_Xxxu, | ACCEPTED /  |
   |              |                | sd_2xxi             | sd_2xxi     |
   |              |                |                     |             |
   | ud_close_pro | - / E          | ACCEPTED /          | - / E       |
   |              |                | sd_2xxu_sd,         |             |
   |              |                | sd_2xxi,            |             |
   |              |                |                     |             |
   | ud_cancel    | TERM /         | TERM / sd_Xxxu,     | TERM /      |
   |              | sd_cancel      | sd_cancel           | sd_cancel   |
   |              |                |                     |             |
   | ud_decline   | - / E          | TERM / sd_Xxxu,     | TERM /      |
   |              |                | sd_Xxxi             | sd_Xxxi     |
   |              |                |                     |             |
   | ud_propose   | UPDATE_OUT /   | IDLE / sd_2xxu_sd   | - / E       |
   |              | sd_update_sd   |                     |             |
   |              |                |                     |             |
   | ud_accept    | - / E          | - / e(488)          | - / E       |
   |              |                |                     |             |
   | ud_reject    | - / E          | IDLE / sd_Xxxu      | - / E       |
   |              |                |                     |             |
   | ud_hangup    | - / E          | - / E               | - / E       |
   +--------------+----------------+---------------------+-------------+

         State transition table for events coming from ifcU (3/3).




















Cuda & Marocco            Expires July 20, 2006                [Page 33]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +--------------+------------------+------------------+--------------+
   |              | INIT             | IDLE             | ACCEPTED     |
   +--------------+------------------+------------------+--------------+
   | su_invite_sd | - / E            | - / e(500)       | - / E        |
   |              |                  |                  |              |
   | su_invite    | - / E            | - / e(500)       | - / E        |
   |              |                  |                  |              |
   | su_2xxi_sd   | ACCEPTED /       | ACCEPTED /       | - / E        |
   |              | uu_close_pro     | uu_close_pro     |              |
   |              |                  |                  |              |
   | su_2xxi      | TERM / uu_close, | TERM / uu_close, | - / E        |
   |              | sd_ack           | sd_ack           |              |
   |              |                  |                  |              |
   | su_Xxxi      | TERM /           | TERM /           | - / E        |
   |              | uu_decline       | uu_decline       |              |
   |              |                  |                  |              |
   | su_ack_sd    | - / e(488)       | - / e(488)       | TERM /       |
   |              |                  |                  | uu_propose   |
   |              |                  |                  |              |
   | su_ack       | - / e(488)       | - / e(488)       | TERM / -     |
   |              |                  |                  |              |
   | su_prack_sd  | PRACK_IN /       | PRACK_IN /       | - / E        |
   |              | uu_propose       | uu_propose       |              |
   |              |                  |                  |              |
   | su_prack     | IDLE / sd_2xxp   | IDLE / sd_2xxp   | - / E        |
   |              |                  |                  |              |
   | su_2xxp_sd   | PRACK_IN /       | PRACK_IN /       | - / E        |
   |              | uu_propose       | uu_propose       |              |
   |              |                  |                  |              |
   | su_2xxp      | IDLE / -         | IDLE / -         | - / E        |
   |              |                  |                  |              |
   | su_Xxxp      | IDLE / -         | IDLE / -         | - / E        |
   |              |                  |                  |              |
   | su_update_sd | UPDATE_IN /      | UPDATE_IN /      | - / e(488)   |
   |              | uu_propose       | uu_propose       |              |
   |              |                  |                  |              |
   | su_2xxu_sd   | ACCEPTED /       | ACCEPTED /       | - / E        |
   |              | uu_propose       | uu_propose       |              |
   |              |                  |                  |              |
   | su_cancel    | TERM / uu_cancel | TERM / uu_cancel | - / E        |
   |              |                  |                  |              |
   | su_bye       | - / E            | - / E            | - / E        |
   |              |                  |                  |              |
   | su_1xxi_sd   | PROV_IN /        | PROV_IN /        | - / E        |
   |              | uu_propose       | uu_propose       |              |
   |              |                  |                  |              |
   | su_Xxxu      | - / E            | - / E            | - / E        |
   +--------------+------------------+------------------+--------------+



Cuda & Marocco            Expires July 20, 2006                [Page 34]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


         State transition table for events coming from ifcS (1/3).

   +--------------+------------------+------------------+--------------+
   |              | PROV_IN          | PROV_OUT         | PRACK_IN     |
   +--------------+------------------+------------------+--------------+
   | su_invite_sd | - / E            | - / E            | - / E        |
   |              |                  |                  |              |
   | su_invite    | - / E            | - / E            | - / E        |
   |              |                  |                  |              |
   | su_2xxi_sd   | ACCEPTED /       | - / e(481)       | - / e(481)   |
   |              | uu_close_pro     |                  |              |
   |              |                  |                  |              |
   | su_2xxi      | TERM / uu_close, | - / e(481)       | - / e(481)   |
   |              | sd_ack           |                  |              |
   |              |                  |                  |              |
   | su_Xxxi      | TERM /           | - / e(481)       | - / e(481)   |
   |              | uu_decline       |                  |              |
   |              |                  |                  |              |
   | su_ack_sd    | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_ack       | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_prack_sd  | - / e(481)       | IDLE /           | - / e(481)   |
   |              |                  | uu_propose       |              |
   |              |                  |                  |              |
   | su_prack     | - / e(481)       | IDLE / sd_2xxp   | - / e(481)   |
   |              |                  |                  |              |
   | su_2xxp_sd   | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_2xxp      | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_Xxxp      | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_update_sd | UPDATE_IN /      | UPDATE_IN /      | - / e(488)   |
   |              | su_prack         | uu_propose       |              |
   |              |                  |                  |              |
   | su_2xxu_sd   | - / e(481)       | - / e(481)       | - / e(481)   |
   |              |                  |                  |              |
   | su_cancel    | - / e(481)       | TERM / uu_cancel | TERM /       |
   |              |                  |                  | uu_cancel    |
   |              |                  |                  |              |
   | su_bye       | - / e(481)       | TERM / uu_cancel | TERM /       |
   |              |                  |                  | uu_cancel    |
   |              |                  |                  |              |
   | su_1xxi_sd   | - / (E) sd_prack | - / E            | - / E        |
   |              |                  |                  |              |
   | su_Xxxu      | - / E            | - / E            | - / E        |
   +--------------+------------------+------------------+--------------+



Cuda & Marocco            Expires July 20, 2006                [Page 35]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


         State transition table for events coming from ifcS (2/3).

   +--------------+---------------+-------------------+----------------+
   |              | PRACK_OUT     | UPDATE_IN         | UPDATE_OUT     |
   +--------------+---------------+-------------------+----------------+
   | su_invite_sd | - / E         | - / E             | - / E          |
   |              |               |                   |                |
   | su_invite    | - / E         | - / E             | - / E          |
   |              |               |                   |                |
   | su_2xxi_sd   | TERM /        | TERM / sd_Xxxu,   | TERM /         |
   |              | uu_close_pro  | uu_close_pro      | uu_close       |
   |              |               |                   |                |
   | su_2xxi      | TERM /        | - / uu_close,     | TERM /         |
   |              | uu_close,     | sd_ack            | uu_close,      |
   |              | sd_ack        |                   | sd_ack         |
   |              |               |                   |                |
   | su_Xxxi      | TERM /        | - / e(481)        | TERM /         |
   |              | uu_decline    |                   | uu_decline     |
   |              |               |                   |                |
   | su_ack_sd    | - / e(481)    | - / e(481)        | - / e(481)     |
   |              |               |                   |                |
   | su_ack       | - / e(481)    | - / e(481)        | - / e(481)     |
   |              |               |                   |                |
   | su_prack_sd  | - / e(481)    | - / uu_propose,   | - /            |
   |              |               | sd_2xxp           | uu_propose,    |
   |              |               |                   | sd_2xxp        |
   |              |               |                   |                |
   | su_prack     | - / e(481)    | - / sd_2xxp       | - / sd_2xxp    |
   |              |               |                   |                |
   | su_2xxp_sd   | IDLE /        | - / e(481)        | - / e(481)     |
   |              | uu_propose    |                   |                |
   |              |               |                   |                |
   | su_2xxp      | IDLE / -      | - / e(481)        | - / e(481)     |
   |              |               |                   |                |
   | su_Xxxp      | TERM / -      | - / e(481)        | - / e(481)     |
   |              |               |                   |                |
   | su_update_sd | UPDATE_IN /   | - / e(500)        | - / e(491)     |
   |              | uu_propose    |                   |                |
   |              |               |                   |                |
   | su_2xxu_sd   | - / e(481)    | - / e(481)        | IDLE /         |
   |              |               |                   | uu_propose     |
   |              |               |                   |                |
   | su_cancel    | - / e(481)    | TERM / sd_Xxxu,   | TERM /         |
   |              |               | uu_decline        | uu_decline     |
   |              |               |                   |                |
   | su_bye       | - / e(481)    | TERM / sd_Xxxu,   | TERM /         |
   |              |               | uu_decline        | uu_decline     |
   |              |               |                   |                |



Cuda & Marocco            Expires July 20, 2006                [Page 36]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   | su_1xxi_sd   | - / (E)       | - / (E) sd_prack  | - / (E)        |
   |              | sd_prack      |                   | sd_prack       |
   |              |               |                   |                |
   | su_Xxxu      | - / E         | - / E             | - / E          |
   +--------------+---------------+-------------------+----------------+

         State transition table for events coming from ifcS (3/3).

5.4.3.  Prop State Machine

                               +---------+
                               |   INIT  |
                               +---------+
                                 |     |
                         +-------+     +-------+
                         |                     |
                         v                     v
                  +-----------+          +------------+
                  | UPDATE_IN |          | UPDATE_OUT |
                  +-----------+          +------------+
                         |                     |
                         +-------+     +-------+
                                 |     |
                                 v     v
                             +-------------+
                             |    TERM     |
                             +-------------+

   +------------+-----------------------+-----------------+------------+
   |            | INIT                  | UPDATE_IN       | UPDATE_OUT |
   +------------+-----------------------+-----------------+------------+
   | ud_propose | UPDATE_OUT /          | TERM /          | - / e(500) |
   |            | sd_update_sd          | sd_2xxu_sd      |            |
   |            |                       |                 |            |
   | ud_accept  | - / E                 | TERM/ sd_Xxxu   | - / e(481) |
   |            |                       |                 |            |
   | ud_reject  | - / E                 | TERM / sd_Xxxu  | - / e(481) |
   +------------+-----------------------+-----------------+------------+

        State transition table for allowed events coming from ifcU.











Cuda & Marocco            Expires July 20, 2006                [Page 37]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


   +--------------+---------------------+-----------------+------------+
   |              | INIT                | UPDATE_IN       | UPDATE_OUT |
   +--------------+---------------------+-----------------+------------+
   | su_update_sd | UPDATE_IN /         | - / uu_propose  | - / e(488) |
   |              | uu_propose          |                 |            |
   |              |                     |                 |            |
   | su_2xxu_sd   | TERM / uu_propose   | TERM /          | - / E      |
   |              |                     | uu_propose      |            |
   +--------------+---------------------+-----------------+------------+

        State transition table for allowed events coming from ifcS.








































Cuda & Marocco            Expires July 20, 2006                [Page 38]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


6.  Open Issues

   A number of issues are still to be closed.  Some of them are
   limitations introduced by the model: it is important to tell whether
   they are acceptable or not.  Others are just cases that are not
   covered yet.

   o  There's a limited support for non-reliable provisional responses.
      In particular the UA can't generate them (however, we are
      interested only in negotiation events, so it should be ok);

   o  Offers (in opposite to answers) can only be sent through UPDATE,
      INVITE requests and INVITE final responses;

   o  All the events are defined as negotiation events.  Some of them
      aren't ([vu]_accept), they must be found and fixed;

   o  Probably we need some mechanism to make sure that when a
      negotiation scope has been closed, there are not outstanding
      offers.  For instance, now the sequence INVITE(SDP1) / 200(SDP2) /
      ACK(SDP3) brings UAs to an inconsistent state;

   o  It is not possible to send two different provisional responses
      simultaneously;

   o  Transition tables currently do not deal with reINVITEs and UPDATEs
      yet;

   o  Error conditions should be classified better;

   o  When a composite action (X[du]_ev1, X[du]_ev2) is introduced, no
      rollback/commit procedure has been detailed.  Shall be added as
      soon as the transition tables become stable enough;

   o  Some diagrams miss some arcs.
















Cuda & Marocco            Expires July 20, 2006                [Page 39]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


7.  Security Considerations

   This memo does not raise security issues.

8.  References

   [I-D.sawada-sipping-sip-offeranswer]
              Sawada, T. and P. Kyzivat, "Best Current Practice for SIP
              (Session Initiation Protocol) Usage of  Offer/Answer
              Model", draft-sawada-sipping-sip-offeranswer-00 (work in
              progress), October 2005.

   [RFC2119]  Bradner, S., "Key words for use in RFCs to Indicate
              Requirement Levels", BCP 14, RFC 2119, March 1997.

   [RFC3261]  Rosenberg, J., Schulzrinne, H., Camarillo, G., Johnston,
              A., Peterson, J., Sparks, R., Handley, M., and E.
              Schooler, "SIP: Session Initiation Protocol", RFC 3261,
              June 2002.

   [RFC3262]  Rosenberg, J. and H. Schulzrinne, "Reliability of
              Provisional Responses in Session Initiation Protocol
              (SIP)", RFC 3262, June 2002.

   [RFC3264]  Rosenberg, J. and H. Schulzrinne, "An Offer/Answer Model
              with Session Description Protocol (SDP)", RFC 3264,
              June 2002.

   [RFC3311]  Rosenberg, J., "The Session Initiation Protocol (SIP)
              UPDATE Method", RFC 3311, October 2002.





















Cuda & Marocco            Expires July 20, 2006                [Page 40]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


Authors' Addresses

   Alberto Cuda
   Telecom Italia
   Via G. Reiss Romoli, 274
   Turin  10148
   Italy

   Phone: +39 011 228 7026
   Email: alberto.cuda@telecomitalia.it


   Enrico Marocco
   Telecom Italia
   Via G. Reiss Romoli, 274
   Turin  10148
   Italy

   Phone: +39 011 228 5029
   Email: enrico.marocco@telecomitalia.it































Cuda & Marocco            Expires July 20, 2006                [Page 41]

Internet-Draft    A Formal Model for Media Negotiation      January 2006


Intellectual Property Statement

   The IETF takes no position regarding the validity or scope of any
   Intellectual Property Rights or other rights that might be claimed to
   pertain to the implementation or use of the technology described in
   this document or the extent to which any license under such rights
   might or might not be available; nor does it represent that it has
   made any independent effort to identify any such rights.  Information
   on the procedures with respect to rights in RFC documents can be
   found in BCP 78 and BCP 79.

   Copies of IPR disclosures made to the IETF Secretariat and any
   assurances of licenses to be made available, or the result of an
   attempt made to obtain a general license or permission for the use of
   such proprietary rights by implementers or users of this
   specification can be obtained from the IETF on-line IPR repository at
   http://www.ietf.org/ipr.

   The IETF invites any interested party to bring to its attention any
   copyrights, patents or patent applications, or other proprietary
   rights that may cover technology that may be required to implement
   this standard.  Please address the information to the IETF at
   ietf-ipr@ietf.org.


Disclaimer of Validity

   This document and the information contained herein are provided on an
   "AS IS" basis and THE CONTRIBUTOR, THE ORGANIZATION HE/SHE REPRESENTS
   OR IS SPONSORED BY (IF ANY), THE INTERNET SOCIETY AND THE INTERNET
   ENGINEERING TASK FORCE DISCLAIM ALL WARRANTIES, EXPRESS OR IMPLIED,
   INCLUDING BUT NOT LIMITED TO ANY WARRANTY THAT THE USE OF THE
   INFORMATION HEREIN WILL NOT INFRINGE ANY RIGHTS OR ANY IMPLIED
   WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.


Copyright Statement

   Copyright (C) The Internet Society (2006).  This document is subject
   to the rights, licenses and restrictions contained in BCP 78, and
   except as set forth therein, the authors retain all their rights.


Acknowledgment

   Funding for the RFC Editor function is currently provided by the
   Internet Society.




Cuda & Marocco            Expires July 20, 2006                [Page 42]