toastie-stuff/chroma
3
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
chroma/lexers/testdata/promela/sample.expected
Toastie f9f64b0558
Added lexars
2025-03-22 20:46:00 +13:00

1491 lines
61 KiB
Text
Raw Permalink Blame History

[
{"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"}
]
Reference in a new issue View git blame Copy permalink