From f98d9043d6da16ee6e99c1395876b31a864dac0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ben=20Br=C3=BCcker?= Date: Tue, 4 Feb 2014 20:57:58 +0100 Subject: [PATCH] Added screenshot and text for simul connect (Better screenshot will follow) --- Report/GDN.tex | 3 ++- Report/verifier-simul.png | Bin 1173 -> 1712 bytes 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Report/GDN.tex b/Report/GDN.tex index 4abf815..abcc3bd 100644 --- a/Report/GDN.tex +++ b/Report/GDN.tex @@ -248,7 +248,7 @@ or Host1.SynSent) and Host2.Established) % subsubsection Case 1: Basic three-way handshake (end) \subsubsection{Case 2: Simultaneous connection request} - Now we prove that when a simultaneous connection request happens, there will always be a established connection between both hosts. To check for this condition, we remove the transition between Closed and Listen. This way, both hosts have to establish a connection using a simultaneous connection set-up. Within the query we force that both hosts pass the SynSent state. + Now we prove that when a simultaneous connection request happens, there will always be a established connection between both hosts. To check for this condition, we remove the transition between Closed-Listen, Listen-Closed and SynSent-Closed. This way, both hosts have to establish a connection using a simultaneous connection set-up. Within the query we force that both hosts pass the SynSent state. Also we had to remove the packet discarding in the closed state. This is due to the fact that we do not handle reset packets. Please see the next section for a related problem. \begin{verbatim} (Host1.SynSent and Host2.SynSent) --> (Host1.Established and Host2.Established) @@ -273,6 +273,7 @@ or Host1.SynSent) and Host2.Established) \item Host2 is now waiting for a Syn, or a SynAck packet and keeps re-sending Syn packets. \item Host1 is now waiting for a Ack packet, and keeps re-sending Ack packets. \end{enumerate} + They may exist cases where this edge case exists because of interesting timings, even with Reset packages. But this is outside the scope of this project % subsubsection Issues concerning the checking of this model (end) % subsection guaranteeing_an_connection (end) % section model_checking_and_verification (end) diff --git a/Report/verifier-simul.png b/Report/verifier-simul.png index 672d0794167a12941e8bfb3ec569979662f31972..e005d7af8f63836da5c7424489af387f0bdad928 100644 GIT binary patch delta 1681 zcmV;C25$M439t;D^IzIlDWYKR2W$JK@8}PX`KxLZMJ78wnb5Y{suX z9|$3Y5V8qu#)J?;$i}c46G8|ff6EgpDHJSh#)J?;$il?ldlkaV5UxYGNuL;BjrLA@B{w~zJ z&xgA-xVs%_o{a2v^jJ6n!NiFts3>f%ASWzcw>j2zwOg< zQ+84vFr$#^YMSE9!{P8yP6EkQ=ZF;L_PG;zKEi3M=CWyVT~OfmQLv9d?8H~;&!X`L zjK2Fegug@hCxox*6JyL^e;!w%GyM7SL^DQ8X$;`pF0l~5AKl~;c&m^)$bNiIMjAT# z^vV8Fapv+9Z+SLt53J|;IL7ypSG~$UJ#RB}0Zy`QkJXXJE&bW%-Hm6(9Fts5TX^zu zbJ$C9P2T1c58T29yH~o`;@9aZAq8 z3Y{6xSsL4rg7$%W-VR z*Xeh)@cR2cy$z!W{};l2`otJBn8#JWN;2AlEd@)6@pZo7Lyf2OMUoIR60>Mlsb1ESDL zZ^j~?2e7lK*pjrrNbPMqj&>He=`P32`JT5r%Moobx7h%i`>77-h*-;yILJ#{7_VRP z`9>11NyVgldbCqc*YKGH$m5~AvhgFh4X@n=mGuG#CX4HW0;da~HL)4rq~D#EX8bk1 z6QdL33O+H$e~dI^=-kY1#t4ATq#Ptoi{VcKa^|HdisT*KWJv`Piq~+;ED{+5!vR*af zF=bcP0Uexf9T=H?kd27_PS58K@5ME#ob*n&I$8*Yf8Z9fuSBz19iY%}OxA2$To)8L zY&%)7PoK5kj1d6q*(0)6fu;svJZs$)X<%~~Yl|eXSDlui3Pa-+fBCra1E8k)XZEl6 zY-MdlUcRX3vF)+tVQ*w(&#zY7h=rQbU{}>4u_z`p?SnAmCGEN2>54hs>U1IYlHsW8 zfHE>6f9jZ&a3@_>3LLhblb;t9xXWqAYy8X@`DESgWUU4!p#jS=D3YlkL&3(Z&W2b^ z#Z#eoP$cDqH6z=p=8Y^LO9d(_4A7>s@Nrf^lqe|CTQ&pLd?q(q1#@2n3M&ew=03z|$d5Fyh6`Og;dl8!} zRy1;D)*{A9K}44e*hFV)JL4^kEl=s9f+ha)q+A>ClGW0!;TFdBR82@!)~Xv)FBb!J ze;%SH&Gr1yArNdXnzHTwJ&#FygXbc4j)cHxH`QTJ5s^#t56Uxr(#E6lJ>DDO8V`{# z`pHQ-y*nj2xw|S3tdb!sCuvki#O7EZ5r48`mB0;i9>T!MyuFuaO!soU_}?>z>ot>h z3o>v2Mm|e6^!y$&^GQ?(A$#DWie=8fXTVh~0Tay_&u;o`wL`kcG|2eFFIj_)J@5Uz z>halmbr7-__EE5pOng7~{%z_)O_^xMgb+dqIf45B+Egf5*o+AwgpiG4GbV%(LN?~Z b$4~zQuJ+G~4v%_300000NkvXXu0mjfQLjfQ literal 1173 zcmeAS@N?(olHy`uVBq!ia0y~yVAKJ!O*xo=WXVRyqdD)!O>yDjW zGQ;Iczq1!tS#o73%jbsOlYcCK!`bxvhf+(6lc10gkE@4=frz5w!GM+)7H6snRLnVl z{H^m2Tf5ay>y>}soBy>)QU9Cm+<$xO&j?R?Jn4MZVvg74SJo?QzY-76OBb`2-Yy}8d&Ax_plQzHU zc6O37^U}E-o}3WLaq@o4w7q%T8{aBTnfhzSVo&jPb_rW%uxq^!;BJgv?a$>9Q`Z0T z-Won>wpx~glN&4Nm0M2T&#Lk6cr(|dmwG#%JkELc_Dt9MUGlTUnm6pYal5(X$PK0# z*)vx+`)*isY4cvyhewZYd3hv8-+t@u19gIj{9aC(p7CESxOA5J$sVzua{Y_hizKB? zbDVt-?wH4R*XUVZ_v+K?kqI`t8J<|Smu=#+J`k7Yt+Pvh&bHe}dy4(9ZJ61;?`MRp zP*NL%*vo4@rMZzEhC5f6Nmn#;{0^#Rzbh{0_vG%E<=4(Ief-wCWtpX;%Th_jy`_v^ ztnml#Z0%p5m#u$;?}FH>*<3F!ILtQ8-okC)wBbcv!7VxUwD$PJX?nkQom>0n%UkuA zr#BvaoK%&UbTg0ny+ESvORfz)(Z0 z&u2+2%6T@2;alXpo12*qm#75get!3}sccWraaJ>@yv_UA+eE@%Ce82dO?}$&&>%E1 zXM5xKjthD=_3oCYVZiYIy?d7I|176U|Ffc9YXdhgh(2~_Ve+9JTO>qQeQ*CaAtO=s zgxPD!9fz`>#;mZ4v(zq|(d4qqclUJf!~VBpBlOJQW_T_BxjFr2czesgW&H(ZIU2Js zcz(|JSADa*O!|h#A&Dm!-!vcUjp_XRZSvtim4dV6lj9~m@zOXH|LM7F$9@Nu6$dOp z9DWy%6ZhMcR8%CoCQL}saB^x|$ic};rofc->+>aVo=9et^g0bJN*Fv{{an^LB{Ts5 DqiGTO