[
  {"type":"CommentMultiline","value":"/**\n\tNeedham-Schroeder message passing protocol (patched). \n\t|\tmsg1:\tagentA -\u003e agentB\t(keyB, agentA, nonceA, 0)\n\t|\tmsg2:\tagentB -\u003e agentA\t(keyA, agentB, nonceA, nonceB)\n\t|\tmsg3:\tagentA -\u003e 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*/"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"CommentMultiline","value":"/* Status Codes */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"err"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\n\t"},
  {"type":"CommentMultiline","value":"/* Message Codes */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"msg1"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"msg2"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"msg3"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\n\t"},
  {"type":"CommentMultiline","value":"/*\tAgent (A)lice */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"keyA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"nonceA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/*\tAgent (B)ob */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"keyB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"nonceB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/*\tAgent (I)ntruder */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"keyI"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"agentI"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"nonceI"},
  {"type":"TextWhitespace","value":" \n"},
  {"type":"Punctuation","value":"};"},
  {"type":"TextWhitespace","value":"\n\n\n"},
  {"type":"CommentMultiline","value":"/**\n\tDeclare a structured data type to model our encrypted messages.\n\tMessages will contain either 2 or 3 content fields.\n*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"typedef"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"key"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"content1"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Name","value":"content2"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"content3"},
  {"type":"TextWhitespace","value":" \n"},
  {"type":"Punctuation","value":"};"},
  {"type":"TextWhitespace","value":"\n\n\n"},
  {"type":"CommentMultiline","value":"/**\n\tModel network between agents via a rendezvous channel. \n\tSend and recieve operations are performed synchronously. \n*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"chan"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"["},
  {"type":"LiteralNumberInteger","value":"0"},
  {"type":"Punctuation","value":"]"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"of"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Crypt"},
  {"type":"Punctuation","value":"};"},
  {"type":"TextWhitespace","value":"\n\n\n"},
  {"type":"CommentMultiline","value":"/* global variables for verification*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"partnerA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"partnerB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"err"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"err"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordType","value":"bool"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n"},
  {"type":"KeywordType","value":"bool"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/* Agent (A)lice */"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"active"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordDeclaration","value":"proctype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Alice"},
  {"type":"Punctuation","value":"()"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* local variables */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t\t"},
  {"type":"CommentMultiline","value":"/* reciever's public key */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pnonce"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t"},
  {"type":"CommentMultiline","value":"/* reciever's nonce\t */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"messageAB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"CommentMultiline","value":"/* sent messages\t\t\t */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t\t"},
  {"type":"CommentMultiline","value":"/* recieved messages\t */"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* \n\t\tInitialization: In this example we non-deterministically choose between \n\t\tagents (B)ob and (I)ntruder\n\t*/"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"partnerA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"partnerA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* prepare (msg1) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"LiteralNumberInteger","value":"0"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* send (msg1) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"messageAB"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* recv (msg2) : blocking */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"?"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"msg2"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* verify (msg2) : blocking\t*/"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"partnerA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* obtain (msg2) sender's nonce */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"pnonce"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* prepare (msg3) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pnonce"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"LiteralNumberInteger","value":"0"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageAB"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"LiteralNumberInteger","value":"0"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* send (msg3) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerA"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"messageAB"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* update status */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/* Agent (B)ob */"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"active"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordDeclaration","value":"proctype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Bob"},
  {"type":"Punctuation","value":"()"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":"\n\t\t\n\t"},
  {"type":"CommentMultiline","value":"/* local variables */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t\t"},
  {"type":"CommentMultiline","value":"/* reciever's public key */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pnonce"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t"},
  {"type":"CommentMultiline","value":"/* reciever's nonce\t */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"messageBA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"CommentMultiline","value":"/* sent messages\t\t\t */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\t\t"},
  {"type":"CommentMultiline","value":"/* recieved messages\t */"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* Initialization\t*/"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"partnerB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"pkey"},
  {"type":"TextWhitespace","value":"\t "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* recv (msg1) : blocking */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"?"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"msg1"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* verify (msg1) : blocking */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* obtain (msg1) sender's nonce */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"pnonce"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\t\n\n\t"},
  {"type":"CommentMultiline","value":"/* prepare (msg2) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageBA"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pkey"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageBA"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageBA"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"pnonce"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"messageBA"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* send (msg2) */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"messageBA"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* recv (msg3) : blocking */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"?"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"msg3"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* verify (msg3) : blocking */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/* Agent (I)ntruder */"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"active"},
  {"type":"TextWhitespace","value":" "},
  {"type":"KeywordDeclaration","value":"proctype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"Intruder"},
  {"type":"Punctuation","value":"()"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"KeywordDeclaration","value":"mtype"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"recpt"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"Crypt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"CommentMultiline","value":"/* Initialize knows_nonce variables to false */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"false"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"false"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"Keyword","value":"do"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"?"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"msg"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"_"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" \n\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* perhaps store the message */"},
  {"type":"TextWhitespace","value":"\n\t\t\t\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":"\t\t "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t\n\t\t\t"},
  {"type":"CommentMultiline","value":"/*\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*/"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" \n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":"  "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyI"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"true"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"TextWhitespace","value":" \n\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Keyword","value":"skip"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"TextWhitespace","value":" \n\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Keyword","value":"skip"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* Replay or send a message */"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* choose message type */"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg1"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg2"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg3"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\n\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* choose a recepient */"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"recpt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"recpt"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t \n\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* replay intercepted message or assemble it */"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":"\t\t"},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":"\t"},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"intercepted"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" \n\t\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* assemble content1 */"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content1"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" "},
  {"type":"CommentMultiline","value":"/* assemble key */"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyA"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyB"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"key"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"keyI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" \n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content2"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"TextWhitespace","value":" \n\n\t\t"},
  {"type":"Keyword","value":"if"},
  {"type":"TextWhitespace","value":" \n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceA"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceB"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Operator","value":"::"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Operator","value":"."},
  {"type":"NameAttribute","value":"content3"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"nonceI"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\t\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"TextWhitespace","value":" \n\t\t\n\t"},
  {"type":"Keyword","value":"fi"},
  {"type":"Punctuation","value":";"},
  {"type":"TextWhitespace","value":"\n\n\t"},
  {"type":"Name","value":"network"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"!"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"msg"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"recpt"},
  {"type":"Punctuation","value":","},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"data"},
  {"type":"Punctuation","value":");"},
  {"type":"TextWhitespace","value":"\n\t"},
  {"type":"Keyword","value":"od"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/**\n\tAlways, one process will terminate in error\n*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"ltl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"alwaysErr"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"[]"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"err"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"||"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"err"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/**\n\tEventually the protocol will complete without error\n*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"ltl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"eventuallyOk"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u003c\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/*\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*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"ltl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"propAB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"[]"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/*\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*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"ltl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"propA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"[]"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":"  "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentB"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":"  "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceA"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"false"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n\n"},
  {"type":"CommentMultiline","value":"/*\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*/"},
  {"type":"TextWhitespace","value":"\n"},
  {"type":"KeywordDeclaration","value":"ltl"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"propB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"{"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"[]"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"statusB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"ok"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":"  "},
  {"type":"Operator","value":"\u0026\u0026"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"("},
  {"type":"Name","value":"partnerB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"agentA"},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"-\u003e"},
  {"type":"TextWhitespace","value":"  "},
  {"type":"Punctuation","value":"("},
  {"type":"TextWhitespace","value":" "},
  {"type":"Name","value":"knows_nonceB"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Operator","value":"=="},
  {"type":"TextWhitespace","value":" "},
  {"type":"NameBuiltin","value":"false"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":")"},
  {"type":"TextWhitespace","value":" "},
  {"type":"Punctuation","value":"}"},
  {"type":"TextWhitespace","value":"\n"}
]