timed global protocol Smtp(role S, role C) { 220() from S to C within [0;1] using a and resetting (); choice at C // Choice 0 { Ehlo1() from C to S within [0;1] using a and resetting (); rec X { choice at S // Choice 1 { 250d() from S to C within [0;1] using a and resetting (); continue X within [0;1] using a and resetting (); } or { 250() from S to C within [0;1] using a and resetting (); choice at C // Choice 2 { StartTls() from C to S within [0;1] using a and resetting (); 220() from S to C within [0;1] using a and resetting (); // Do TLS handshake here: level below the application level protocol (like regular TCP handshake) choice at C // Choice 3 { Ehlo2() from C to S within [0;1] using a and resetting (); rec X { choice at S // Choice 4 { 250d1() from S to C within [0;1] using a and resetting (); continue X within [0;1] using a and resetting (); } or { 2501() from S to C within [0;1] using a and resetting (); rec Y { choice at C // Choice 5 { Auth() from C to S within [0;1] using a and resetting (); choice at S // Choice 6 { 235() from S to C within [0;1] using a and resetting (); rec Z1 { choice at C // Choice 7 { Mail() from C to S within [0;1] using a and resetting (); //Mail from: choice at S // Choice 8 { 501() from S to C within [0;1] using a and resetting (); continue Z1 within [0;1] using a and resetting (); } or { 2502() from S to C within [0;1] using a and resetting (); rec Z2 { choice at C // Choice 9 { Rcpt() from C to S within [0;1] using a and resetting (); //Rcpt to: choice at S // What is this choice??? // Choice X { 2503() from S to C within [0;1] using a and resetting (); continue Z2 within [0;1] using a and resetting (); } } or { Data() from C to S within [0;1] using a and resetting (); 354() from S to C within [0;1] using a and resetting (); too from C to S within [0;1] using a and resetting (); //to: froom from C to S within [0;1] using a and resetting (); //from: rec Z3 { choice at C // Choice 10 { DataLine() from C to S within [0;1] using a and resetting (); DataLine() from C to S within [0;1] using a and resetting (); continue Z3 within [0;1] using a and resetting (); } or { Subject() from C to S within [0;1] using a and resetting (); //Subject: Subject() from C to S within [0;1] using a and resetting (); //Subject: continue Z3 within [0;1] using a and resetting (); } or { EndOfData() from C to S within [0;1] using a and resetting (); // CRLF.CRLF 2504() from S to C within [0;1] using a and resetting (); continue Z1 within [0;1] using a and resetting (); } } } } } } or { Quit5() from C to S within [0;1] using a and resetting (); 221() from S to C within [0;1] using a and resetting (); } } } or { 535() from S to C within [0;1] using a and resetting (); continue Y within [0;1] using a and resetting (); } //.. 501 Invalid base64 Data } or { Quit4() from C to S } } } } } or { Quit3() from C to S within [0;1] using a and resetting (); } } or { Quit2() from C to S within [0;1] using a and resetting (); } } } } or { Quit1() from C to S within [0;1] using a and resetting (); } }