/* ======================================================================== DESCRIPTION This model provides a formal definition of user agents engaged in an invite dialog, according to the basic version of SIP as documented by RFC 3261, with the single addition of Info requests. The "caller UA" is the UA sending the initial invite. The "callee UA" is the UA receiving the initial invite. The user agents are modeled at the level of the transaction user, so 100 messages, retransmissions, and acks sent in response to invite failures are not included. ======================================================================== */ /* ======================================================================== DEFINITION OF MESSAGE TYPES Requests invite ack cancel info bye Provisional Responses prov18x (a non-reliable 180, 181, or 182 response to an initial invite) dialog183 (a non-reliable 183 response to an initial invite) Final Responses ("DVR" stands for Dialog Vanished Response) inv200 (a 200 in response to an invite) invFail (any 3xx-6xx response to an invite except 408, 481, or 491) invDVR (a 408 or 481 response to an invite) inv491 (a 491 response to a re-invite) ackTimeout (a timeout generated by waiting for ack to initial invite) canc200 (a 200 in response to a cancel) cancDVR (a 408 or 481 response to a cancel) infoDVR (a 408 or 481 response to an info) infoRsp (any other response to an info, whether successful or failing) bye200 (a 200 in response to a bye) byeDVR (a 408 or 481 response to a bye) ======================================================================== */ proctype callerUA(chan in,out) { bool early = false; /* Note E1 */ bool initAcked = false; bool reInvited = false; bool reInviting = false; bool infoRsped = true; /* to bound queue size, only one */ /* outstanding info request is allowed */ mtype media = noFlow; mtype sdp; if :: out!invite,offer; media = offering :: out!invite,none fi; Inviting: do :: in?invite,sdp; assert(false) :: in?ack,sdp; assert(false) :: in?cancel,sdp; assert(false) :: in?info,sdp; assert(early); if :: out!infoRsp,none /* Note N1 */ :: out!infoDVR,none; goto end fi :: in?bye,sdp; assert(false) :: in?prov18x,sdp; early = true :: in?dialog183,sdp; assert(sdp == answer || sdp == none); early = true; if /* Note E2 */ :: sdp == answer; assert(media == offering); media = flow :: sdp == none fi; :: in?inv200,sdp; if :: sdp == answer; assert(media == offering || media == flow); if :: out!ack,none; initAcked = true :: out!ackTimeout,none; goto end fi; if :: media == offering; media = flow :: else fi /* Note E2 */ :: sdp == offer; assert(media == noFlow); media = offered :: sdp == none; assert(false) fi; early = false; goto Confirmed /* Note D1 */ :: in?invFail,sdp; goto end :: in?invDVR,sdp; goto end :: in?inv491,sdp; assert(false) :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp; assert(early && !infoRsped); infoRsped = true :: in?infoDVR,sdp; assert(early && !infoRsped); /* Note F1 */ goto ForcedBye :: in?bye200,sdp; assert(false) :: in?byeDVR,sdp; assert(false) :: early && infoRsped; out!info,none; infoRsped = false :: early; out!bye,none; goto Byeing /* Note B1 */ :: out!cancel,none; goto Canceling od; Confirmed: do :: in?invite,sdp; assert(!reInvited); if :: out!invDVR,none; goto ending :: reInviting; out!inv491,none /* Note I2 */ :: !reInviting; assert(media == flow); if :: sdp != none; assert(sdp == offer); if :: media = offered; reInvited = true /* Note I1 */ :: out!invFail,none fi :: sdp == none; if :: reInvited = true :: out!invFail,none fi fi fi :: in?ack,sdp; /* Notes I3, I4 */ if :: sdp != none; assert(reInvited && media == offering && sdp == answer); media = flow; reInvited = false :: sdp == none; assert(!reInvited); assert(media == flow || (reInviting && media == offering)) fi :: in?cancel,sdp; assert(false) :: in?info,sdp; if :: out!infoRsp,none :: out!infoDVR,none; goto ending fi :: in?bye,sdp; assert(initAcked); /* Note B3 */ if :: reInvited && media == flow; if :: out!inv200,offer; out!bye200,none :: out!byeDVR,none fi :: reInvited && media == offered; if :: out!inv200,answer; out!bye200,none :: out!byeDVR,none fi :: reInviting && media == offered; if :: out!ack,answer; out!bye200,none :: out!byeDVR,none fi :: else; if :: out!bye200,none :: out!byeDVR,none fi fi; goto ending :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp; /* Note I4 */ assert(reInviting && media != offered && sdp != none); if :: media == flow; assert(sdp == offer); media = offered :: media == offering; assert(sdp == answer); media = flow; reInviting = false; out!ack,none fi :: in?invFail,sdp; assert(reInviting && !reInvited); reInviting = false; media = flow :: in?invDVR,sdp; assert(reInviting && !reInvited); goto ForcedBye /* Note F1 */ :: in?inv491,sdp; assert(reInviting && !reInvited); reInviting = false; if :: media == offering; media = flow :: else fi :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp; assert(!infoRsped); infoRsped = true :: in?infoDVR,sdp; assert(!infoRsped); goto ForcedBye :: in?bye200,sdp; assert(false) :: in?byeDVR,sdp; assert(false) :: !reInvited && !reInviting && initAcked; assert(media==flow); if /* Note I3 */ :: out!invite,offer; reInviting = true; media = offering :: out!invite,none; reInviting = true fi :: reInvited && (media == offered || media == flow); if /* Note I4 */ :: media == offered; out!inv200,answer; media = flow; reInvited = false :: media == flow; out!inv200,offer; media = offering fi :: !reInvited && media == offered; /* Note I4 */ if :: reInviting; reInviting = false; media = flow; out!ack,answer :: !reInviting; assert(!initAcked); initAcked = true; media = flow; out!ack,answer fi :: infoRsped; out!info,none; infoRsped = false :: (!reInvited || (reInvited && media == offering)) && (!reInviting || (reInviting && media != offered)) && initAcked; /* Note B2 */ out!bye,none; goto Byeing od; Canceling: do :: in?invite,sdp; assert(false) :: in?ack,sdp; assert(false) :: in?cancel,sdp; assert(false) :: in?info,sdp; if :: out!infoRsp,none :: out!infoDVR,none; goto end fi :: in?bye,sdp; assert(false) :: in?prov18x,sdp :: in?dialog183,sdp :: in?inv200,sdp; assert(sdp == offer || sdp == answer); if :: sdp == offer; out!ack,answer :: sdp == answer; out!ack,none fi; initAcked = true; out!bye,none; goto Byeing /* Note C2 */ :: in?invFail,sdp; goto end :: in?invDVR,sdp; early = true; goto ForcedBye /* Notes F1, E3*/ :: in?inv491,sdp; assert(false) :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp :: in?cancDVR,sdp; /* Note C4 */ if :: early; goto ForcedBye :: early; goto end :: !early; goto end fi :: in?infoRsp,sdp :: in?infoDVR,sdp; early = true; goto ForcedBye /* Note E3 */ :: in?bye200,sdp; assert(false) :: in?byeDVR,sdp; assert(false) od; ForcedBye: if /* Note B2 */ :: !initAcked && media == flow; initAcked = true; out!ack,none :: !initAcked && media == offered; out!ack,answer; initAcked = true :: reInvited && media == flow; out!inv200,offer; media = offering :: reInvited && media == offered; out!inv200,answer; reInvited = false; media = flow :: reInviting && media == offered; out!ack,answer; reInviting = false; media = flow :: else fi; out!bye,none; goto Byeing; Byeing: assert( (!reInvited || (reInvited && media == offering)) && (!reInviting || (reInviting && media != offered)) && (initAcked || early) ); do :: in?invite,sdp; if :: out!invFail,none /* Note F4 */ :: out!invDVR,none; goto ending fi :: in?ack,sdp :: in?cancel,sdp; assert(false) :: in?info,sdp; if :: out!infoRsp,none :: out!infoDVR,none; goto ending fi :: in?bye,sdp; if :: out!bye200,none :: out!byeDVR,none; goto ending fi :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp; assert(sdp == offer || sdp == answer); if :: sdp == offer; out!ack,answer :: sdp == answer; out!ack,none fi; initAcked = true :: in?invFail,sdp :: in?invDVR,sdp :: in?inv491,sdp :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp :: in?cancDVR,sdp :: in?infoRsp,sdp :: in?infoDVR,sdp :: in?bye200,sdp; goto ending :: in?byeDVR,sdp; goto ending od; ending: /* state visited if and only if dialog confirmed; */ /* the timeout is actually generated in UAS */ if :: !initAcked; out!ackTimeout,none :: else fi; end: do /* if the "DVR" messages are actually DVRs (as opposed to */ /* 481s), they are actually generated by UAS container */ :: in?invite,sdp; out!invDVR,none :: in?ack,sdp :: in?cancel,sdp; assert(false) :: in?info,sdp; out!infoDVR,none :: in?bye,sdp; out!byeDVR,none :: in?prov18x,sdp :: in?dialog183,sdp :: in?inv200,sdp; goto ending :: in?invFail,sdp :: in?invDVR,sdp :: in?inv491,sdp :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp :: in?cancDVR,sdp :: in?infoRsp,sdp :: in?infoDVR,sdp :: in?bye200,sdp :: in?byeDVR,sdp od } proctype calleeUA(chan in,out) { bool early = false; /* Note E1 */ bool initAcked = false; bool reInvited = false; bool reInviting = false; bool provSent = false; /* to bound queue size */ bool infoRsped = true; /* to bound queue size, only one */ /* outstanding info request is allowed */ bool blocked = false; mtype media = noFlow; mtype sdp; in?invite,sdp; if :: sdp != none; assert(sdp == offer); media = offered :: sdp == none fi; /* Note I1 */ Invited: do :: in?invite,sdp; assert(false) :: in?ack,sdp; assert(false) :: in?cancel,sdp; if :: out!canc200,none; out!invFail,none; goto end /* Note C1 */ :: out!invFail,none; out!canc200,none; goto end :: out!cancDVR,none; out!invDVR,none; goto end :: out!invDVR,none; out!cancDVR,none; goto end fi :: in?info,sdp; assert(early); if :: out!infoRsp,none /* Note N1 */ :: out!infoDVR,none; goto end fi :: in?bye,sdp; assert(early); if :: out!bye200,none; out!invFail,none; goto end /* Note B3 */ :: out!invFail,none; out!bye200,none; goto end :: out!byeDVR,none; goto end fi :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp; assert(false) :: in?invFail,sdp; assert(false) :: in?invDVR,sdp; assert(false) :: in?inv491,sdp; assert(false) :: in?ackTimeout,sdp; assert(false) :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp; assert(early && !infoRsped); infoRsped = true :: in?infoDVR,sdp; assert(early && !infoRsped); out!invFail,none; goto end /* Note F2 */ :: in?bye200,sdp; assert(false) :: in?byeDVR,sdp; assert(false) :: early && infoRsped; out!info,none; infoRsped = false :: !provSent; out!prov18x,none; early = true; provSent = true :: !provSent; early = true; provSent = true; if :: out!dialog183,none; :: media == offered; out!dialog183,answer; media = flow fi /* Note E2 */ :: media == noFlow; out!inv200,offer; media = offering; goto Confirmed /* Note D1 */ :: media == offered; out!inv200,answer; media = flow; goto Confirmed :: media == flow; out!inv200,answer; goto Confirmed /* repeat early answer; Note E2 */ :: out!invFail,none; goto end /* Note B1 */ :: out!invDVR,none; goto end od; Confirmed: do :: in?invite,sdp; assert(!reInvited); if :: out!invDVR,none; goto end :: reInviting; out!inv491,none /* Note I2 */ :: !reInviting; assert(media == flow); if :: sdp != none; assert(sdp == offer); if :: media = offered; reInvited = true /* Note I1 */ :: out!invFail,none fi :: sdp == none; if :: reInvited = true :: out!invFail,none fi fi fi :: in?ack,sdp; /* Note I5 */ if :: sdp != none; assert(!reInviting && media == offering && sdp == answer); media = flow; if :: !initAcked; initAcked = true :: reInvited; reInvited = false fi; :: sdp == none; if :: !initAcked; initAcked = true :: else fi; assert(!reInvited); assert(media==flow || (reInviting && media==offering)); fi; :: in?cancel,sdp; assert(!initAcked); if :: out!canc200,none /* Note C3 */ :: out!cancDVR,none; goto end fi :: in?info,sdp; if :: out!infoRsp,none :: out!infoDVR,none; goto end fi :: in?bye,sdp; /* Note B3 */ if :: reInvited && media == flow; if :: out!inv200,offer; out!bye200,none :: out!byeDVR,none fi :: reInvited && media == offered; if :: out!inv200,answer; out!bye200,none :: out!byeDVR,none fi :: reInviting && media == offered; if :: out!ack,answer; out!bye200,none :: out!byeDVR,none fi :: else; if :: out!bye200,none :: out!byeDVR,none fi fi; goto end :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp; /* Note I4 */ assert(reInviting && media != offered && sdp != none); if :: media == flow; assert(sdp == offer); media = offered :: media == offering; assert(sdp == answer); media = flow; reInviting = false; out!ack,none fi :: in?invFail,sdp; assert(reInviting && !reInvited && initAcked); reInviting = false; media = flow :: in?invDVR,sdp; assert(reInviting && !reInvited && initAcked); goto ForcedBye /* Note F1 */ :: in?inv491,sdp; assert(reInviting && !reInvited); reInviting = false; if :: media == offering; media = flow :: else fi :: in?ackTimeout,sdp; initAcked = true; goto ForcedBye /* Note I6 */ :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp; assert(!infoRsped); infoRsped = true :: in?infoDVR,sdp; assert(!infoRsped); goto ForcedBye /* Note F1 */ :: in?bye200,sdp; assert(false) :: in?byeDVR,sdp; assert(false) :: !reInviting && !reInvited && media == flow; if /* Note I3 */ :: out!invite,offer; reInviting = true; media = offering :: out!invite,none; reInviting = true fi :: reInvited && (media == offered || media == flow); if /* Note I4 */ :: media == offered; out!inv200,answer; media = flow; reInvited = false :: media == flow; out!inv200,offer; media = offering fi :: reInviting && media == offered; /* Note I4 */ media = flow; reInviting = false; out!ack,answer :: infoRsped; out!info,none; infoRsped = false :: (!reInvited || (reInvited && media == offering)) && (!reInviting || (reInviting && media != offered)) && initAcked; /* Note B2 */ out!bye,none; goto Byeing od; ForcedBye: if /* Note B2 */ :: reInvited && media == flow; out!inv200,offer; media = offering :: reInvited && media == offered; out!inv200,answer; reInvited = false; media = flow :: reInviting && media == offered; out!ack,answer; reInviting = false; media = flow :: else fi; if :: initAcked; out!bye,none; goto Byeing :: else; blocked = true; goto Byeing /* Note F3 */ fi; Byeing: assert( (!reInvited || (reInvited && media == offering)) && (!reInviting || (reInviting && media != offered)) && (initAcked || blocked) ); do :: in?invite,sdp; if :: out!invFail,none /* Note F4 */ :: out!invDVR,none; goto end fi :: in?ack,sdp :: in?cancel,sdp; assert(false) :: in?info,sdp; if :: out!infoRsp,none; :: out!infoDVR,none; goto end fi :: in?bye,sdp; if :: out!bye200,none; if :: blocked; goto end :: else fi :: out!byeDVR,none; goto end fi :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp :: in?invFail,sdp :: in?invDVR,sdp :: in?inv491,sdp :: in?ackTimeout,sdp; /* Note F3 */ if :: blocked; out!bye,none; blocked = false :: else fi :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp :: in?infoDVR,sdp :: in?bye200,sdp; goto end :: in?byeDVR,sdp; goto end od; end: do /* if the "DVR" messages are actually DVRs (as opposed to */ /* 481s), they are actually generated by UAC container */ :: in?invite,sdp; out!invDVR,none :: in?ack,sdp :: in?cancel,sdp; out!cancDVR,none :: in?info,sdp; out!infoDVR,none :: in?bye,sdp; out!byeDVR,none :: in?prov18x,sdp; assert(false) :: in?dialog183,sdp; assert(false) :: in?inv200,sdp :: in?invFail,sdp :: in?invDVR,sdp :: in?inv491,sdp :: in?ackTimeout,sdp :: in?canc200,sdp; assert(false) :: in?cancDVR,sdp; assert(false) :: in?infoRsp,sdp :: in?infoDVR,sdp :: in?bye200,sdp :: in?byeDVR,sdp od } /* ======================================================================== NOTES EARLY DIALOGS AND EARLY MEDIA E1 A dialog established by a non-final response to the initial invite is in the "early" state (RFC 3261, Sec. 12.1). E2 If the callee UA sends an answer to the initial offer in a 183, this is "early media". The callee UA must repeat the same answer in the final response to the initial invite, because the provisional response is not reliable (RFC 3261, Sec. 13.2.1). E3 Setting early = true is artificial here. It satisfies the assertion on entrance to the Byeing state, in the case that the caller UA sent cancel before establishment of the dialog. CONFIRMED DIALOGS D1 A dialog becomes "confirmed" at a UA when a successful final response to the initial invite is sent or received (RFC 3261, Sec. 12 and 15). CANCELING C1 No order is specified for these two messages, so they can be sent in any order (RFC 3261, Sec. 9.2). C2 If the caller UA receives inv200 in the Canceling state, then the cancel message arrived at the callee UA too late. Strictly speaking, the caller UA is not required to end the dialog. However, it does not make much sense for the caller UA to change its mind, so the model assumes that the caller UA still wants to end the dialog, and ends it by sending bye. C3 This is a cancel race--the cancel has arrived too late to cause the initial invite transaction to fail. RFC 3261 says that the non-failure behavior here is to send canc481, on the grounds that the invite transaction no longer exists (Sec 9.2). However, the active Internet Draft draft-ietf-sipcore-invfix explains that 3261 is considering the initial invite transaction to be gone too early, and describes the problems that this causes. The ID proposes a fix in which the initial transaction lasts longer, and specifies that the correct non-failure behavior here is to send canc200. We are modeling this fix. Note that without this change, when a caller UA receives a canc481, it does not know whether there has been a benign cancel race or a catastrophic callee UA failure. This is a big problem, because the caller UA's behavior should be different in the two cases. C4 Sending a bye here is required if the cancel is considered a mid-dialog request (see FAILURES), and prohibited if there is no early dialog. We don't know if cancel is considered a mid-dialog request. The model includes all possibilities that don't violate the prohibition. INVITE TRANSACTIONS I1 In an offer/answer exchange within an invite transaction, there can be a delay between receiving an offer and sending an answer. This delay allows interaction with a user. I2 If a UA receives an invite when it has sent an invite in the same dialog and not yet been answered, it must send a 491 message in response to the received invite (RFC 3261, Sec. 14.2). This is a re-invite race. I3 A UA cannot re-invite if there is on ongoing invite transaction (RFC 3261, Sec. 14.1). Normally an invite transaction ends when the invited has sent inv200 and the inviting has received inv200 and sent ack. Either side can then re-invite, even though the invited has not yet received ack. However, the invite might contain a solicit (no sdp), in which case the inv200 carries an offer and the ack carries an answer. In this case the ack might not be sent immediately on receiving the inv200, and the invite transaction cannot be considered ended until the sending and receiving of the ack (RFC 3264, Sec. 4). I4 Here are some helpful rules for understanding re-invites: reInvited && media != offering => this UA owes inv200 reInvited && media == offering => this UA expects ack reInviting && media != offered => this UA expects inv200 reInviting && media == offered => this UA owes ack I5 Interpreting an ack in the callee UA is particularly complex. (a) If the ack carries sdp, then it is completing an offer/answer exchange that began with a solicit (invite,none). We know that media == offering and sdp == answer. We also know that the callee UA cannot be reInviting, because there is an uncompleted offer/answer exchange initiated by the caller UA. (a1) The solicit may have been the initial invite. In this case we must set initAcked to true. (a2) The solicit may have been a re-invite from the caller UA. In this case we must set reInvited to false. (b) If the ack does not carry sdp, then the offer/answer exchange was completed previously. The invite may have been the initial invite, in which case we must set initAcked to true. Even if the invite was a re-invite, reInvited will be false, because it was set to false when the offer/answer exchange was completed. (b1) Probably media == flow. This is what we would expect. (b2) However, it is possible that reInviting == true and media == offering. The caller UA can re-invite as soon as its last offer/answer exchange is completed, even if the last invite received has not yet been acked. I6 If the ack to the initial invite times out, the callee UA should end the session with a bye (RFC 3261, Sec. 13.3.1.4). BYE TRANSACTIONS B1 A caller UA can send a bye for either confirmed or early dialogs (RFC 3261, Sec. 15). If the callee UA wants to end an early dialog, it should send invFail. B2 The callee UA cannot send a bye until the initial transaction is confirmed and it has received an ack or ack timeout for the initial invite (RFC 3261, Sec. 15). Also, neither UA can send a bye if it has an outstanding obligation on any invite transaction. See Note I4 for obligations related to re-invites. B3 If a bye is received when there is an invite transaction pending, the invite transaction must be completed (RFC 3261, Sec. 15.1.2). No order is imposed on multiple response messages. INFO TRANSACTIONS N1 In this model, for simplicity, a UA always responds immediately to an info request. If a real UA does not respond immediately, then it must complete the transaction before sending or responding to a bye, as in Notes B2 and B3, or before sending invFail. FAILURES F1 When a UA receives a 408 or 481 within a dialog, it should terminate the dialog (RFC 3261, Sec. 12.2.1.2) by sending bye. F2 When a UA receives a 408 or 481 within a dialog, it should terminate the dialog (RFC 3261, Sec. 12.2.1.2). Although the section says to do this by sending a bye, in the Invited state a bye is illegal, and invFail is sent instead. F3 On receiving a 408 or 481 in a confirmed dialog, a UA should send bye. However, a callee UA cannot send bye until the initial invite has been acked or the ack has timed out (Note B2). The UA becomes blocked until it receives the ack timeout, then sends bye. F4 RFC 5407 (Sec. 3.2.2) says that, in the case of receiving an invite after sending a bye, a UA should respond with 481. Although this behavior is modeled, we are also include sending 487, which seems more consistent, because this UA expects to receive bye200. ======================================================================== */