omated state space calculation, supported query functions of CPN ML, simulation, and performance tools, etc. Using the BYE attack detection model shown in Section 16.3.2 as an exam- ple, Figure 16.13 is the corresponding report and result of state space simu- lation. As state space is calculated, CPN ML query functions can be utilized for further analysis. CPN ML language is used for declarations and net inscrip- tions. The declarations of SIP message shown in Figure 16.14 are of standard CPN ML, which also provides many functions for state space, monitoring, and performance analysis. The following function is a query of a BYE attack State Space Nodes: UACI 'Incoming 1: 1 OK200@0 Arcs: UACI 'Outgoing 1 1: empty Secs: UACI 'RTP1 1: 1 RTPNONE@0 Status: Partial UACI'RTP2 1: 1 RTPNONE@ UACI 'Alarming 1: empty Boundedness properties UACI 'Store2 1: empty UACI l'G_RTP 1: empty Best Integer Bounds UAC2 'Incoming2 1: empty Upper Lower UAC2 "Outgoing2 1: 1 OK200@0 TOP'RTP 1 UAC2 'RTP2 1: 1 RTPNONE@0 TOP'RTP 2 UAC2 'Store 1: empty TOP'U1to U2 1 UAC2 'G_RTP 1: empty TOP'U2to U1 1 TOP'U1toU2 1: empty JAC1'Alarming 1 TOP'U2toU1 1: 1 ° OK200@0 UAC1'G_RTP 1 TOP'RTP1 1: 1 RTPNONE UAC1'Store2 1 TOP'RTP2 1: 1 RTPNONE@ UAC2'G_RTF 1 intruder'U1toU2 1: empty UAC2'Store 1 intruder'U2toU1 1: 1 OK200@0 intruder'G_BYE 1 intruder'RTP1 1: 1 RTPNONE@ intruder'RTP2 1: 1 RTPNONE@0 Liveness Properties intruder'G BYE 1: 1 BYE Dead Markings Dead Transition Instances UAC1'A_BYE 1 Live Transition Instances FIGURE 16.13 State space simulation report and result for model in Figure 16.11. fun AuthViolation():Node list = PredAllNodes(fn n=> cf(OK200, Mark.UAC1'Alarming 1 n)>0 andalso cf(RTPCONN, Mark.UAC2'RTP2 n)>0 AuthViolation(); FIGURE 16.14 CPN ML query functions for BYE attack. © 2009 by Taylor & Francis Group, LLC SIP Handbook: Services, Technologies, and Security model, which means that if alarming occurs when there is still an RTP package from UAC2, the BYE attack exists. The monitoring and performance tools are useful for simulation of models