'/**\n\tNeedham-Schroeder message passing protocol (patched). \n\t|\tmsg1:\tagentA -> agentB\t(keyB, agentA, nonceA, 0)\n\t|\tmsg2:\tagentB -> agentA\t(keyA, agentB, nonceA, nonceB)\n\t|\tmsg3:\tagentA -> agentB\t(keyB, nonceB, 0, 0)\n\n\tNote that sending (keyB, agentA, nonceA) from agentA to agentB \n\tover the network (chan)nel models agentA encrypting the message \n\t"[agentA, nonceB]" with agentB\'s public key.\n*/' Comment.Multiline '\n' Text.Whitespace '\n' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '{' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace '/* Status Codes */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'ok' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'err' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* Message Codes */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'msg1' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'msg2' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'msg3' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/*\tAgent (A)lice */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'keyA' Name ',' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'agentA' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'nonceA' Name ',' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/*\tAgent (B)ob */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'keyB' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'agentB' Name ',' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'nonceB' Name ',' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/*\tAgent (I)ntruder */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'keyI' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'agentI' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'nonceI' Name ' ' Text.Whitespace '\n' Text.Whitespace '}' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '/**\n\tDeclare a structured data type to model our encrypted messages.\n\tMessages will contain either 2 or 3 content fields.\n*/' Comment.Multiline '\n' Text.Whitespace 'typedef' Keyword.Declaration ' ' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'key' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'content1' Name ',' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'content2' Name ',' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'content3' Name ' ' Text.Whitespace '\n' Text.Whitespace '}' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '/**\n\tModel network between agents via a rendezvous channel. \n\tSend and recieve operations are performed synchronously. \n*/' Comment.Multiline '\n' Text.Whitespace 'chan' Keyword.Declaration ' ' Text.Whitespace 'network' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '[' Punctuation '0' Literal.Number.Integer ']' Punctuation ' ' Text.Whitespace 'of' Name ' ' Text.Whitespace '{' Punctuation 'mtype' Keyword.Declaration ',' Punctuation ' ' Text.Whitespace 'mtype' Keyword.Declaration ',' Punctuation ' ' Text.Whitespace 'Crypt' Name '}' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '/* global variables for verification*/' Comment.Multiline '\n' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'partnerA' Name ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'partnerB' Name ';' Punctuation '\n' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'statusA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'err' Name ';' Punctuation '\n' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'statusB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'err' Name ';' Punctuation '\n' Text.Whitespace 'bool' Keyword.Type ' ' Text.Whitespace 'knows_nonceA' Name ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace 'bool' Keyword.Type ' ' Text.Whitespace 'knows_nonceB' Name ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '/* Agent (A)lice */' Comment.Multiline '\n' Text.Whitespace 'active' Keyword.Declaration ' ' Text.Whitespace 'proctype' Keyword.Declaration ' ' Text.Whitespace 'Alice' Name '(' Punctuation ')' Punctuation ' ' Text.Whitespace '{' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* local variables */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'pkey' Name ';' Punctuation '\t\t\t' Text.Whitespace "/* reciever's public key */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'pnonce' Name ';' Punctuation '\t\t' Text.Whitespace "/* reciever's nonce\t */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace 'messageAB' Name ';' Punctuation '\t' Text.Whitespace '/* sent messages\t\t\t */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace 'data' Name ';' Punctuation '\t\t\t' Text.Whitespace '/* recieved messages\t */' Comment.Multiline '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* \n\t\tInitialization: In this example we non-deterministically choose between \n\t\tagents (B)ob and (I)ntruder\n\t*/' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'partnerA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentB' Name ';' Punctuation ' ' Text.Whitespace 'pkey' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyB' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'partnerA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentI' Name ';' Punctuation ' ' Text.Whitespace 'pkey' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyI' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* prepare (msg1) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pkey' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentA' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceA' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '0' Literal.Number.Integer ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* send (msg1) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '!' Operator ' ' Text.Whitespace 'msg1' Name ' ' Text.Whitespace '(' Punctuation 'partnerA' Name ',' Punctuation ' ' Text.Whitespace 'messageAB' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* recv (msg2) : blocking */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '?' Operator ' ' Text.Whitespace '(' Punctuation 'msg2' Name ',' Punctuation ' ' Text.Whitespace 'agentA' Name ',' Punctuation ' ' Text.Whitespace 'data' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* verify (msg2) : blocking\t*/' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'keyA' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'partnerA' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceA' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace "/* obtain (msg2) sender's nonce */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'pnonce' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content3' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* prepare (msg3) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pkey' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pnonce' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '0' Literal.Number.Integer ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageAB' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '0' Literal.Number.Integer ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* send (msg3) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '!' Operator ' ' Text.Whitespace 'msg3' Name ' ' Text.Whitespace '(' Punctuation 'partnerA' Name ',' Punctuation ' ' Text.Whitespace 'messageAB' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* update status */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'statusA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'ok' Name ';' Punctuation '\n' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '/* Agent (B)ob */' Comment.Multiline '\n' Text.Whitespace 'active' Keyword.Declaration ' ' Text.Whitespace 'proctype' Keyword.Declaration ' ' Text.Whitespace 'Bob' Name '(' Punctuation ')' Punctuation ' ' Text.Whitespace '{' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* local variables */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'pkey' Name ';' Punctuation '\t\t\t' Text.Whitespace "/* reciever's public key */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'pnonce' Name ';' Punctuation '\t\t' Text.Whitespace "/* reciever's nonce\t */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace 'messageBA' Name ';' Punctuation '\t' Text.Whitespace '/* sent messages\t\t\t */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace 'data' Name ';' Punctuation '\t\t\t' Text.Whitespace '/* recieved messages\t */' Comment.Multiline '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* Initialization\t*/' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'partnerB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentA' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'pkey' Name '\t ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyA' Name ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* recv (msg1) : blocking */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '?' Operator ' ' Text.Whitespace '(' Punctuation 'msg1' Name ',' Punctuation ' ' Text.Whitespace 'agentB' Name ',' Punctuation ' ' Text.Whitespace 'data' Name ')' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* verify (msg1) : blocking */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'keyB' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'agentA' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace "/* obtain (msg1) sender's nonce */" Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'pnonce' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute ';' Punctuation '\t' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* prepare (msg2) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'messageBA' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pkey' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageBA' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentB' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageBA' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pnonce' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'messageBA' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceB' Name ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* send (msg2) */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '!' Operator ' ' Text.Whitespace 'msg2' Name ' ' Text.Whitespace '(' Punctuation 'partnerB' Name ',' Punctuation ' ' Text.Whitespace 'messageBA' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* recv (msg3) : blocking */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '?' Operator ' ' Text.Whitespace '(' Punctuation 'msg3' Name ',' Punctuation ' ' Text.Whitespace 'agentB' Name ',' Punctuation ' ' Text.Whitespace 'data' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* verify (msg3) : blocking */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'keyB' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceB' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'statusB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'ok' Name ';' Punctuation '\n' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '/* Agent (I)ntruder */' Comment.Multiline '\n' Text.Whitespace 'active' Keyword.Declaration ' ' Text.Whitespace 'proctype' Keyword.Declaration ' ' Text.Whitespace 'Intruder' Name '(' Punctuation ')' Punctuation ' ' Text.Whitespace '{' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'mtype' Keyword.Declaration ' ' Text.Whitespace 'msg' Name ',' Punctuation ' ' Text.Whitespace 'recpt' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'Crypt' Name ' ' Text.Whitespace 'data' Name ',' Punctuation ' ' Text.Whitespace 'intercepted' Name ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace '/* Initialize knows_nonce variables to false */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'knows_nonceA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'false' Name.Builtin ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'knows_nonceB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'false' Name.Builtin ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'do' Keyword '\n' Text.Whitespace '\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'network' Name ' ' Text.Whitespace '?' Operator ' ' Text.Whitespace '(' Punctuation 'msg' Name ',' Punctuation ' ' Text.Whitespace '_' Name.Builtin ',' Punctuation ' ' Text.Whitespace 'data' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* perhaps store the message */' Comment.Multiline '\n' Text.Whitespace '\t\t\t' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator '\t' Text.Whitespace 'intercepted' Name '.' Operator 'key' Name.Attribute '\t\t ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'key' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'intercepted' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'intercepted' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace '\n' Text.Whitespace '\t\t\t' Text.Whitespace "/*\t\n\t\t\t\tMessage contains (I)ntruder's (public) key, the intruder can \n\t\t\t\tdecrypt the message. Note that we can learn nonce values from \n\t\t\t\teither content1 or content2\n\t\t\t\t|\tmsg1:\t(keyB, agentA, nonceA, 0)\n\t\t\t\t|\tmsg2:\t(keyA, agentB, nonceA, nonceB)\n\t\t\t\t|\tmsg3: \t(keyB, nonceB, 0, 0)\n\t\t\t*/" Comment.Multiline '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'intercepted' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'keyI' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceA' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceB' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceA' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceB' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceA' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceA' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation ' ' Text.Whitespace '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'nonceB' Name ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'knows_nonceB' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'true' Name.Builtin ';' Punctuation '\n' Text.Whitespace '\t\t\t\t' Text.Whitespace 'fi' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'skip' Keyword ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'fi' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'skip' Keyword ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '/* Replay or send a message */' Comment.Multiline '\n' Text.Whitespace '\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* choose message type */' Comment.Multiline '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'msg' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'msg1' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'msg' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'msg2' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'msg' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'msg3' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* choose a recepient */' Comment.Multiline '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'recpt' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentA' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'recpt' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentB' Name ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\t\t\t ' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* replay intercepted message or assemble it */' Comment.Multiline '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator '\t' Text.Whitespace 'data' Name '.' Operator 'key' Name.Attribute '\t\t' Text.Whitespace '=' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'key' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute '\t' Text.Whitespace '=' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content1' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute '\t' Text.Whitespace '=' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content2' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace 'data' Name '.' Operator 'content3' Name.Attribute '\t' Text.Whitespace '=' Operator ' ' Text.Whitespace 'intercepted' Name '.' Operator 'content3' Name.Attribute ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* assemble content1 */' Comment.Multiline '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentA' Name ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentB' Name ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'agentI' Name ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceA' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceA' Name '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceB' Name '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation '!' Operator 'knows_nonceA' Name ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '!' Operator 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content1' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceI' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '/* assemble key */' Comment.Multiline '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyA' Name ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyB' Name ';' Punctuation '\n' Text.Whitespace '\t\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'key' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'keyI' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceA' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceA' Name '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceB' Name '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation '!' Operator 'knows_nonceA' Name ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '!' Operator 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content2' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceI' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace 'fi' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace 'if' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceA' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceA' Name '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceB' Name '\n' Text.Whitespace '\t\t' Text.Whitespace ':' Operator ':' Operator ' ' Text.Whitespace '(' Punctuation '!' Operator 'knows_nonceA' Name ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '!' Operator 'knows_nonceB' Name ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace 'data' Name '.' Operator 'content3' Name.Attribute ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nonceI' Name ';' Punctuation '\n' Text.Whitespace '\t\t' Text.Whitespace 'fi' Keyword ' ' Text.Whitespace '\n' Text.Whitespace '\t\t' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'fi' Keyword ';' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '\t' Text.Whitespace 'network' Name ' ' Text.Whitespace '!' Operator ' ' Text.Whitespace 'msg' Name ' ' Text.Whitespace '(' Punctuation 'recpt' Name ',' Punctuation ' ' Text.Whitespace 'data' Name ')' Punctuation ';' Punctuation '\n' Text.Whitespace '\t' Text.Whitespace 'od' Keyword '\n' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '/**\n\tAlways, one process will terminate in error\n*/' Comment.Multiline '\n' Text.Whitespace 'ltl' Keyword.Declaration ' ' Text.Whitespace 'alwaysErr' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '[]' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'statusA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'err' Name ')' Punctuation ' ' Text.Whitespace '|' Operator '|' Operator ' ' Text.Whitespace '(' Punctuation 'statusB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'err' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace '/**\n\tEventually the protocol will complete without error\n*/' Comment.Multiline '\n' Text.Whitespace 'ltl' Keyword.Declaration ' ' Text.Whitespace 'eventuallyOk' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '<>' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'statusA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'statusB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace "/*\n\tpropAB: If both Alice and Bob reach the end of their runs (i.e. both statusA and statusB are ok) \n\tthen Alice's communication partner is Bob, and Bob's communication partner is Alice.\n*/" Comment.Multiline '\n' Text.Whitespace 'ltl' Keyword.Declaration ' ' Text.Whitespace 'propAB' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '[]' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'statusA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'statusB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'partnerB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'agentA' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'partnerA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'agentB' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace "/*\n\tpropA: If agent A reaches the end of its run (statusA is ok) and A believes it is talking to B \n\t(partnerA is agentB) then the intruder does not know A's nonce (!knows_nonceA).\n*/" Comment.Multiline '\n' Text.Whitespace 'ltl' Keyword.Declaration ' ' Text.Whitespace 'propA' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '[]' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'statusA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'partnerA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'agentB' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace 'knows_nonceA' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'false' Name.Builtin ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '}' Punctuation '\n' Text.Whitespace '\n' Text.Whitespace "/*\n\tpropB: If agent B reaches the end of its run (statusB is ok) and it believes it is talking to A \n\t(partnerB is agentA) then the intruder does not know B's nonce (!knows_nonceB)\n*/" Comment.Multiline '\n' Text.Whitespace 'ltl' Keyword.Declaration ' ' Text.Whitespace 'propB' Name ' ' Text.Whitespace '{' Punctuation ' ' Text.Whitespace '[]' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace '(' Punctuation 'statusB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'ok' Name ')' Punctuation ' ' Text.Whitespace '&' Operator '&' Operator ' ' Text.Whitespace '(' Punctuation 'partnerB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'agentA' Name ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '-' Operator '>' Operator ' ' Text.Whitespace '(' Punctuation ' ' Text.Whitespace 'knows_nonceB' Name ' ' Text.Whitespace '=' Operator '=' Operator ' ' Text.Whitespace 'false' Name.Builtin ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace ')' Punctuation ' ' Text.Whitespace '}' Punctuation '\n' Text.Whitespace