| 1 | :- dynamic parserVersionNum/1, parserVersionStr/1, parseResult/5. | |
| 2 | :- dynamic module/4. | |
| 3 | 'parserVersionStr'('0.6.2.1'). | |
| 4 | 'parseResult'('ok','',0,0,0). | |
| 5 | :- dynamic channel/2, bindval/3, agent/3. | |
| 6 | :- dynamic agent_curry/3, symbol/4. | |
| 7 | :- dynamic dataTypeDef/2, subTypeDef/2, nameType/2. | |
| 8 | :- dynamic cspTransparent/1. | |
| 9 | :- dynamic cspPrint/1. | |
| 10 | :- dynamic pragma/1. | |
| 11 | :- dynamic comment/2. | |
| 12 | :- dynamic assertBool/1, assertRef/5, assertTauPrio/6. | |
| 13 | :- dynamic assertModelCheckExt/4, assertModelCheck/3. | |
| 14 | :- dynamic assertLtl/4, assertCtl/4. | |
| 15 | 'parserVersionNum'([0,11,1,1]). | |
| 16 | 'parserVersionStr'('CSPM-Frontent-0.11.1.1'). | |
| 17 | 'dataTypeDef'('KEY',['constructor'('ka'),'constructor'('kb'),'constructor'('kc')]). | |
| 18 | 'dataTypeDef'('AKTEUR',['constructor'('A'),'constructor'('B'),'constructor'('C')]). | |
| 19 | 'dataTypeDef'('NONCE',['constructor'('NonceA'),'constructor'('NonceB'),'constructor'('NonceC')]). | |
| 20 | 'dataTypeDef'('TICKET1',['constructorC'('Encrypt1','dotTupleType'(['KEY','NONCE','AKTEUR']))]). | |
| 21 | 'dataTypeDef'('TICKET2',['constructorC'('Encrypt2','dotTupleType'(['KEY','NONCE','NONCE']))]). | |
| 22 | 'dataTypeDef'('TICKET3',['constructorC'('Encrypt3','dotTupleType'(['KEY','NONCE']))]). | |
| 23 | 'dataTypeDef'('MSG',['constructorC'('Msg1','dotTupleType'(['AKTEUR','AKTEUR','TICKET1'])),'constructorC'('Msg2','dotTupleType'(['AKTEUR','AKTEUR','TICKET2'])),'constructorC'('Msg3','dotTupleType'(['AKTEUR','AKTEUR','TICKET3']))]). | |
| 24 | 'channel'('comm','type'('dotTupleType'(['MSG']))). | |
| 25 | 'channel'('fake','type'('dotTupleType'(['MSG']))). | |
| 26 | 'channel'('intercept','type'('dotTupleType'(['MSG']))). | |
| 27 | 'channel'('user','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 28 | 'channel'('session','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 29 | 'channel'('I_running','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 30 | 'channel'('R_running','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 31 | 'channel'('I_commit','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 32 | 'channel'('R_commit','type'('dotTupleType'(['AKTEUR','AKTEUR']))). | |
| 33 | 'cspPrint'('agent_call'('src_span'(16,7,16,11,506,4),'card',['setExp'('rangeEnum'([_x]),['comprehensionGenerator'(_x,'TICKET1')])])). | |
| 34 | 'cspPrint'('agent_call'('src_span'(17,7,17,11,538,4),'card',['setExp'('rangeEnum'([_x2]),['comprehensionGenerator'(_x2,'TICKET2')])])). | |
| 35 | 'cspPrint'('agent_call'('src_span'(18,7,18,11,570,4),'card',['setExp'('rangeEnum'([_x3]),['comprehensionGenerator'(_x3,'TICKET3')])])). | |
| 36 | 'cspPrint'('agent_call'('src_span'(19,7,19,11,602,4),'card',['setExp'('rangeEnum'([_x4]),['comprehensionGenerator'(_x4,'MSG')])])). | |
| 37 | 'agent'('key'('B'),'kb','src_span'(21,8,21,10,632,2)). | |
| 38 | 'agent'('key'('A'),'ka','src_span'(22,8,22,10,642,2)). | |
| 39 | 'agent'('key'('C'),'kc','src_span'(23,8,23,10,652,2)). | |
| 40 | 'agent'('INITIATOR'(_a,_na),'prefix'('src_span'(26,2,26,8,674,6),['in'(_b)],'dotTuple'(['user',_a]),'prefix'('src_span'(27,2,27,15,686,13),[],'dotTuple'(['I_running',_a,_b]),'prefix'('src_span'(28,2,28,6,703,4),['out'('dotTuple'(['Msg1',_a,_b,'Encrypt1','agent_call'('src_span'(28,25,28,28,726,3),'key',[_b]),_na,_a]))],'comm','prefix'('src_span'(29,2,29,31,741,29),['in'('dotpat'([_na2,_nb]))],'dotTuple'(['comm','Msg2',_b,_a,'Encrypt2','agent_call'('src_span'(29,25,29,28,764,3),'key',[_a])]),'ifte'('=='(_na,_na2),'prefix'('src_span'(31,7,31,11,800,4),['out'('dotTuple'(['Msg3',_a,_b,'Encrypt3','agent_call'('src_span'(31,30,31,33,823,3),'key',[_b]),_nb]))],'comm','prefix'('src_span'(32,2,32,14,837,12),[],'dotTuple'(['I_commit',_a,_b]),'prefix'('src_span'(33,2,33,13,853,11),[],'dotTuple'(['session',_a,_b]),'skip'('src_span'(34,2,34,6,868,4)),'src_span'(33,14,34,1,864,19)),'src_span'(32,15,33,1,849,35)),'src_span'(31,40,32,1,832,68)),'stop'('src_span'(35,7,35,11,879,4)),'no_loc_info_available','no_loc_info_available','src_span'(34,7,35,6,872,83)),'src_span'(29,39,30,1,777,113)),'src_span'(28,37,29,1,737,176)),'src_span'(27,16,28,1,699,197)),'src_span'(26,11,27,1,682,203)),'src_span'(26,2,35,11,674,209)). | |
| 41 | 'agent'('RESPONDER'(_b2,_nb2),'prefix'('src_span'(38,2,38,6,903,4),['in'('dotpat'([_a2,_b3]))],'user','prefix'('src_span'(39,2,39,15,915,13),[],'dotTuple'(['R_running',_a2,_b3]),'prefix'('src_span'(40,2,40,31,932,29),['in'(_na3),'out'(_a2)],'dotTuple'(['comm','Msg1',_a2,_b3,'Encrypt1','agent_call'('src_span'(40,25,40,28,955,3),'key',[_b3])]),'prefix'('src_span'(41,2,41,6,970,4),['out'('dotTuple'(['Msg2',_b3,_a2,'Encrypt2','agent_call'('src_span'(41,25,41,28,993,3),'key',[_a2]),_na3,_nb2]))],'comm','prefix'('src_span'(42,2,42,31,1009,29),['in'(_nb22)],'dotTuple'(['comm','Msg3',_a2,_b3,'Encrypt3','agent_call'('src_span'(42,25,42,28,1032,3),'key',[_b3])]),'ifte'('=='(_nb2,_nb22),'prefix'('src_span'(44,7,44,19,1065,12),[],'dotTuple'(['R_commit',_a2,_b3]),'prefix'('src_span'(44,21,44,32,1079,11),[],'dotTuple'(['session',_a2,_b3]),'skip'('src_span'(44,34,44,38,1092,4)),'src_span'(44,33,44,33,1090,17)),'src_span'(44,20,44,20,1077,31)),'stop'('src_span'(46,2,46,6,1104,4)),'no_loc_info_available','no_loc_info_available','src_span'(44,39,46,1,1096,43)),'src_span'(42,36,43,1,1042,70)),'src_span'(41,38,42,1,1005,134)),'src_span'(40,37,41,1,966,144)),'src_span'(39,16,40,1,928,193)),'src_span'(38,11,39,1,911,201)),'src_span'(38,2,46,6,903,205)). | |
| 42 | 'bindval'('INITIATOR1','procRenaming'(['rename'('dotTuple'(['comm','Msg1']),'dotTuple'(['comm','Msg1'])),'rename'('dotTuple'(['comm','Msg1']),'dotTuple'(['intercept','Msg1'])),'rename'('dotTuple'(['comm','Msg2']),'dotTuple'(['comm','Msg2'])),'rename'('dotTuple'(['comm','Msg2']),'dotTuple'(['fake','Msg2'])),'rename'('dotTuple'(['comm','Msg3']),'dotTuple'(['comm','Msg3'])),'rename'('dotTuple'(['comm','Msg3']),'dotTuple'(['intercept','Msg3']))],'agent_call'('src_span'(49,2,49,11,1123,9),'INITIATOR',['A','NonceA']),'src_span'(50,2,54,4,1144,147)),'src_span'(48,1,54,4,1110,181)). | |
| 43 | 'bindval'('RESPONDER1','procRenaming'(['rename'('dotTuple'(['comm','Msg1']),'dotTuple'(['comm','Msg1'])),'rename'('dotTuple'(['comm','Msg1']),'dotTuple'(['fake','Msg1'])),'rename'('dotTuple'(['comm','Msg2']),'dotTuple'(['comm','Msg2'])),'rename'('dotTuple'(['comm','Msg2']),'dotTuple'(['intercept','Msg2'])),'rename'('dotTuple'(['comm','Msg3']),'dotTuple'(['comm','Msg3'])),'rename'('dotTuple'(['comm','Msg3']),'dotTuple'(['fake','Msg3']))],'agent_call'('src_span'(57,2,57,11,1306,9),'RESPONDER',['B','NonceB']),'src_span'(58,2,62,4,1327,142)),'src_span'(56,1,62,4,1293,176)). | |
| 44 | 'agent'('INTRUDER'(_m1s,_m2s,_m3s,_ns),'prefix'('src_span'(77,4,77,18,2040,14),['in'('dotpat'([_a3,_b4,'Encrypt1',_k,_n,_a22]))],'dotTuple'(['intercept','Msg1']),'ifte'('=='(_k,'agent_call'('src_span'(78,18,78,21,2094,3),'key',['C'])),'agent_call'('src_span'(78,30,78,38,2106,8),'INTRUDER',[_m1s,_m2s,_m3s,'agent_call'('src_span'(78,51,78,56,2127,5),'union',[_ns,'setExp'('rangeEnum'([_n]))])]),'[]'('agent_call'('src_span'(79,17,79,25,2158,8),'INTRUDER',['agent_call'('src_span'(79,26,79,31,2167,5),'union',[_m1s,'setExp'('rangeEnum'(['dotTuple'(['Encrypt1',_k,_n,_a22])]))]),_m2s,_m3s,_ns]),'prefix'('src_span'(81,2,81,16,2215,14),['in'('dotpat'([_b5,_a4,'Encrypt2',_k2,_n2,_n22]))],'dotTuple'(['intercept','Msg2']),'ifte'('=='(_k2,'agent_call'('src_span'(82,18,82,21,2269,3),'key',['C'])),'agent_call'('src_span'(82,30,82,38,2281,8),'INTRUDER',[_m1s,_m2s,_m3s,'agent_call'('src_span'(82,51,82,56,2302,5),'union',[_ns,'setExp'('rangeEnum'([_n2,_n22]))])]),'[]'('agent_call'('src_span'(83,17,83,25,2336,8),'INTRUDER',[_m1s,'agent_call'('src_span'(83,30,83,35,2349,5),'union',[_m2s,'setExp'('rangeEnum'(['dotTuple'(['Encrypt2',_k2,_n2,_n22])]))]),_m3s,_ns]),'prefix'('src_span'(85,2,85,16,2393,14),['in'('dotpat'([_a5,_b6,'Encrypt3',_k3,_n3]))],'dotTuple'(['intercept','Msg3']),'ifte'('=='(_k3,'agent_call'('src_span'(86,18,86,21,2444,3),'key',['C'])),'agent_call'('src_span'(86,30,86,38,2456,8),'INTRUDER',[_m1s,_m2s,_m3s,'agent_call'('src_span'(86,51,86,56,2477,5),'union',[_ns,'setExp'('rangeEnum'([_n3]))])]),'[]'('[]'('[]'('agent_call'('src_span'(87,17,87,25,2508,8),'INTRUDER',[_m1s,_m2s,'agent_call'('src_span'(87,34,87,39,2525,5),'union',[_m3s,'setExp'('rangeEnum'(['dotTuple'(['Encrypt3',_k3,_n3])]))]),_ns]),'prefix'('src_span'(91,2,91,11,2620,9),['in'('dotpat'([_a6,_b7])),'inGuard'(_m,_m2s)],'dotTuple'(['fake','Msg2']),'agent_call'('src_span'(91,23,91,31,2641,8),'INTRUDER',[_m1s,_m2s,_m3s,_ns]),'src_span'(91,22,91,22,2639,32)),'src_span_operator'('no_loc_info_available','src_span'(90,4,90,6,2616,2))),'prefix'('src_span'(95,2,95,11,2731,9),['in'('dotpat'([_a7,_b8])),'out'('Encrypt1'),'in'(_k4),'inGuard'(_n4,_ns),'in'(_a23)],'dotTuple'(['fake','Msg1']),'agent_call'('src_span'(95,36,95,44,2765,8),'INTRUDER',[_m1s,_m2s,_m3s,_ns]),'src_span'(95,35,95,35,2763,29)),'src_span_operator'('no_loc_info_available','src_span'(94,4,94,6,2727,2))),'prefix'('src_span'(99,2,99,11,2870,9),['in'('dotpat'([_a8,_b9])),'out'('Encrypt3'),'in'(_k5),'inGuard'(_n5,_ns)],'dotTuple'(['fake','Msg3']),'agent_call'('src_span'(99,33,99,41,2901,8),'INTRUDER',[_m1s,_m2s,_m3s,_ns]),'src_span'(99,32,99,32,2899,31)),'src_span_operator'('no_loc_info_available','src_span'(98,4,98,6,2866,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(85,34,86,11,2424,518)),'src_span_operator'('no_loc_info_available','src_span'(84,4,84,6,2389,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(81,37,82,11,2249,696)),'src_span_operator'('no_loc_info_available','src_span'(80,4,80,6,2211,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(77,39,78,11,2074,871)),'src_span'(77,4,99,57,2040,885)). | |
| 45 | 'agent'('INTRUDERneu'(_m1s2,_m2s2,_m3s2,_ns2),'[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(102,4,102,47,2961,43),[],'dotTuple'(['intercept','Msg1','A','C','Encrypt1','agent_call'('src_span'(102,32,102,35,2989,3),'key',['C']),'NonceA','A']),'agent_call'('src_span'(103,12,103,23,3018,11),'INTRUDERneu',[_m1s2,_m2s2,_m3s2,'agent_call'('src_span'(103,36,103,41,3042,5),'union',[_ns2,'setExp'('rangeEnum'(['NonceA']))])]),'src_span'(102,48,103,11,3004,100)),'prefix'('src_span'(105,2,105,31,3073,29),['inGuard'(_n6,_ns2),'inGuard'(_a9,'setExp'('rangeEnum'(['A'])))],'dotTuple'(['fake','Msg1','A','B','Encrypt1','agent_call'('src_span'(105,25,105,28,3096,3),'key',['B'])]),'agent_call'('src_span'(106,12,106,23,3127,11),'INTRUDERneu',[_m1s2,_m2s2,_m3s2,_ns2]),'src_span'(105,43,106,11,3113,47)),'src_span_operator'('no_loc_info_available','src_span'(104,8,104,10,3069,2))),'prefix'('src_span'(108,4,108,52,3168,48),[],'dotTuple'(['intercept','Msg2','B','A','Encrypt2','agent_call'('src_span'(108,32,108,35,3196,3),'key',['A']),'NonceA','NonceB']),'agent_call'('src_span'(109,12,109,23,3230,11),'INTRUDERneu',[_m1s2,'agent_call'('src_span'(109,28,109,33,3246,5),'union',[_m2s2,'setExp'('rangeEnum'(['dotTuple'(['Encrypt2','agent_call'('src_span'(109,48,109,51,3266,3),'key',['A']),'NonceA','NonceB'])]))]),_m3s2,_ns2]),'src_span'(108,53,109,11,3216,128)),'src_span_operator'('no_loc_info_available','src_span'(107,8,107,10,3162,2))),'prefix'('src_span'(111,2,111,15,3308,13),['inGuard'(_m2,_m2s2)],'dotTuple'(['fake','Msg2','C','A']),'agent_call'('src_span'(112,12,112,23,3341,11),'INTRUDERneu',[_m1s2,_m2s2,_m3s2,_ns2]),'src_span'(111,22,112,11,3327,47)),'src_span_operator'('no_loc_info_available','src_span'(110,8,110,10,3304,2))),'prefix'('src_span'(114,8,114,49,3386,41),[],'dotTuple'(['intercept','Msg3','A','C','Encrypt3','agent_call'('src_span'(114,36,114,39,3414,3),'key',['C']),'NonceB']),'agent_call'('src_span'(115,12,115,23,3441,11),'INTRUDERneu',[_m1s2,_m2s2,_m3s2,'agent_call'('src_span'(115,36,115,41,3465,5),'union',[_ns2,'setExp'('rangeEnum'(['NonceB']))])]),'src_span'(114,50,115,11,3427,98)),'src_span_operator'('no_loc_info_available','src_span'(113,8,113,10,3376,2))),'prefix'('src_span'(117,2,117,31,3496,29),['inGuard'(_n7,_ns2)],'dotTuple'(['fake','Msg3','A','B','Encrypt3','agent_call'('src_span'(117,25,117,28,3519,3),'key',['B'])]),'agent_call'('src_span'(118,12,118,23,3544,11),'INTRUDERneu',[_m1s2,_m2s2,_m3s2,_ns2]),'src_span'(117,37,118,11,3530,46)),'src_span_operator'('no_loc_info_available','src_span'(116,8,116,10,3492,2))),'no_loc_info_available'). | |
| 46 | 'bindval'('INTRUDER1','agent_call'('src_span'(121,13,121,24,3586,11),'INTRUDERneu',['setExp'('rangeEnum'([])),'setExp'('rangeEnum'([])),'setExp'('rangeEnum'([])),'setExp'('rangeEnum'(['NonceC']))]),'src_span'(121,1,121,43,3574,42)). | |
| 47 | 'bindval'('AGENT','sharing'('closure'(['comm','dotTuple'(['session','A','B'])]),'val_of'('INITIATOR1','src_span'(123,13,123,23,3630,10)),'val_of'('RESPONDER1','src_span'(123,49,123,59,3666,10)),'src_span'(123,24,123,48,3641,24)),'src_span'(123,1,123,59,3618,58)). | |
| 48 | 'bindval'('SYSTEM','sharing'('closure'(['comm','fake','intercept']),'val_of'('AGENT','src_span'(125,13,125,18,3690,5)),'val_of'('INTRUDER1','src_span'(125,47,125,56,3724,9)),'src_span'(125,19,125,46,3696,27)),'src_span'(125,1,125,56,3678,55)). | |
| 49 | 'bindval'('Sigma','closure'(['user','session','comm','fake','intercept','I_running','R_running','I_commit','R_commit']),'src_span'(127,1,128,56,3735,107)). | |
| 50 | 'bindval'('A1','closure'(['dotTuple'(['R_running','A','B']),'dotTuple'(['I_commit','A','B'])]),'src_span'(130,1,130,44,3844,43)). | |
| 51 | 'bindval'('RUN','repChoice'(['comprehensionGenerator'(_x5,'agent_call'('src_span'(132,19,132,23,3907,4),'diff',['val_of'('Sigma','src_span'(132,24,132,29,3912,5)),'val_of'('A1','src_span'(132,30,132,32,3918,2))]))],'prefix'('src_span'(132,37,132,38,3925,1),[],_x5,'val_of'('RUN','src_span'(132,42,132,45,3930,3)),'src_span'(132,39,132,41,3926,8)),'src_span'(132,16,132,36,3904,20)),'src_span'(132,1,132,45,3889,44)). | |
| 52 | 'bindval'('AR0','prefix'('src_span'(134,13,134,26,3947,13),[],'dotTuple'(['R_running','A','B']),'prefix'('src_span'(134,30,134,42,3964,12),[],'dotTuple'(['I_commit','A','B']),'val_of'('AR0','src_span'(134,46,134,49,3980,3)),'src_span'(134,43,134,45,3976,19)),'src_span'(134,27,134,29,3960,36)),'src_span'(134,1,134,49,3935,48)). | |
| 53 | 'bindval'('AR','|||'('val_of'('AR0','src_span'(136,13,136,16,3997,3)),'val_of'('RUN','src_span'(136,21,136,24,4005,3)),'src_span_operator'('no_loc_info_available','src_span'(136,17,136,20,4001,3))),'src_span'(136,1,136,24,3985,23)). | |
| 54 | 'bindval'('A2','closure'(['dotTuple'(['I_running','A','B']),'dotTuple'(['R_commit','A','B'])]),'src_span'(138,1,138,44,4010,43)). | |
| 55 | 'bindval'('RUN2','repChoice'(['comprehensionGenerator'(_x6,'agent_call'('src_span'(140,19,140,23,4073,4),'diff',['val_of'('Sigma','src_span'(140,24,140,29,4078,5)),'val_of'('A2','src_span'(140,30,140,32,4084,2))]))],'prefix'('src_span'(140,37,140,38,4091,1),[],_x6,'val_of'('RUN2','src_span'(140,42,140,46,4096,4)),'src_span'(140,39,140,41,4092,9)),'src_span'(140,16,140,36,4070,20)),'src_span'(140,1,140,46,4055,45)). | |
| 56 | 'bindval'('AI0','prefix'('src_span'(142,13,142,26,4114,13),[],'dotTuple'(['I_running','A','B']),'prefix'('src_span'(142,30,142,42,4131,12),[],'dotTuple'(['R_commit','A','B']),'val_of'('AI0','src_span'(142,46,142,49,4147,3)),'src_span'(142,43,142,45,4143,19)),'src_span'(142,27,142,29,4127,36)),'src_span'(142,1,142,49,4102,48)). | |
| 57 | 'bindval'('AI','|||'('val_of'('AI0','src_span'(144,13,144,16,4164,3)),'val_of'('RUN2','src_span'(144,21,144,25,4172,4)),'src_span_operator'('no_loc_info_available','src_span'(144,17,144,20,4168,3))),'src_span'(144,1,144,25,4152,24)). | |
| 58 | 'assertRef'('False','val_of'('AI','src_span'(148,9,148,11,4223,2)),'Trace','val_of'('SYSTEM','src_span'(148,16,148,22,4230,6)),'src_span'(148,1,148,22,4215,21)). | |
| 59 | 'assertRef'('False','val_of'('AR','src_span'(150,9,150,11,4318,2)),'Trace','val_of'('SYSTEM','src_span'(150,16,150,22,4325,6)),'src_span'(150,1,150,22,4310,21)). | |
| 60 | 'comment'('lineComment'('-- \x9\comm.Msg1?a.b.Encrypt1.k.n.a2->'),'src_position'(65,1,1497,37)). | |
| 61 | 'comment'('lineComment'('-- \x9\ if k==key(C) then INTRUDER(m1s,m2s,m3s,union(ns,{n}))'),'src_position'(66,1,1535,67)). | |
| 62 | 'comment'('lineComment'('-- \x9\ else INTRUDER(union(m1s,{Encrypt1.k.n.a2}),m2s,m3s,ns)'),'src_position'(67,1,1603,68)). | |
| 63 | 'comment'('lineComment'('-- \x9\[]'),'src_position'(68,1,1672,8)). | |
| 64 | 'comment'('lineComment'('--\x9\comm.Msg2?b.a.Encrypt2.k.n.n2->'),'src_position'(69,1,1681,34)). | |
| 65 | 'comment'('lineComment'('-- \x9\ if k==key(C) then INTRUDER(m1s,m2s,m3s,union(ns,{n,n2}))'),'src_position'(70,1,1716,70)). | |
| 66 | 'comment'('lineComment'('-- \x9\ else INTRUDER(m1s,union(m2s,{Encrypt2.k.n.n2}),m3s,ns)'),'src_position'(71,1,1787,68)). | |
| 67 | 'comment'('lineComment'('-- \x9\[]'),'src_position'(72,1,1856,8)). | |
| 68 | 'comment'('lineComment'('--\x9\comm.Msg3?a.b.Encrypt3.k.n->'),'src_position'(73,1,1865,31)). | |
| 69 | 'comment'('lineComment'('-- \x9\ if k==key(C) then INTRUDER(m1s,m2s,m3s,union(ns,{n}))'),'src_position'(74,1,1897,67)). | |
| 70 | 'comment'('lineComment'('-- else INTRUDER(m1s,m2s,union(m3s,{Encrypt3.k.n}),ns)'),'src_position'(75,1,1965,65)). | |
| 71 | 'comment'('lineComment'('--\x9\[]'),'src_position'(76,1,2031,5)). | |
| 72 | 'comment'('lineComment'('-- \x9\[]'),'src_position'(88,1,2555,8)). | |
| 73 | 'comment'('lineComment'('--\x9\fake.Msg1?a.b?m:m1s->INTRUDER(m1s,m2s,m3s,ns)'),'src_position'(89,1,2564,48)). | |
| 74 | 'comment'('lineComment'('-- \x9\[]'),'src_position'(92,1,2666,8)). | |
| 75 | 'comment'('lineComment'('--\x9\fake.Msg3?a.b?m:m3s->INTRUDER(m1s,m2s,m3s,ns)'),'src_position'(93,1,2675,48)). | |
| 76 | 'comment'('lineComment'('-- \x9\[]'),'src_position'(96,1,2790,7)). | |
| 77 | 'comment'('lineComment'('--\x9\fake.Msg2?b.a!Encrypt2?k?n:ns?n2:ns->INTRUDER(m1s,m2s,m3s,ns)'),'src_position'(97,1,2798,64)). | |
| 78 | 'comment'('lineComment'('-- proof obligations for refinement'),'src_position'(146,1,4178,35)). | |
| 79 | 'comment'('lineComment'('--assert INTRUDER({},{},{},{NonceC}) [T= INTRUDERneu({},{},{},{NonceC})'),'src_position'(149,1,4237,72)). | |
| 80 | 'symbol'('KEY','KEY','src_span'(1,10,1,13,9,3),'Datatype'). | |
| 81 | 'symbol'('ka','ka','src_span'(1,20,1,22,19,2),'Constructor of Datatype'). | |
| 82 | 'symbol'('kb','kb','src_span'(1,25,1,27,24,2),'Constructor of Datatype'). | |
| 83 | 'symbol'('kc','kc','src_span'(1,30,1,32,29,2),'Constructor of Datatype'). | |
| 84 | 'symbol'('AKTEUR','AKTEUR','src_span'(2,10,2,16,41,6),'Datatype'). | |
| 85 | 'symbol'('A','A','src_span'(2,20,2,21,51,1),'Constructor of Datatype'). | |
| 86 | 'symbol'('B','B','src_span'(2,24,2,25,55,1),'Constructor of Datatype'). | |
| 87 | 'symbol'('C','C','src_span'(2,28,2,29,59,1),'Constructor of Datatype'). | |
| 88 | 'symbol'('NONCE','NONCE','src_span'(3,10,3,15,70,5),'Datatype'). | |
| 89 | 'symbol'('NonceA','NonceA','src_span'(3,20,3,26,80,6),'Constructor of Datatype'). | |
| 90 | 'symbol'('NonceB','NonceB','src_span'(3,29,3,35,89,6),'Constructor of Datatype'). | |
| 91 | 'symbol'('NonceC','NonceC','src_span'(3,38,3,44,98,6),'Constructor of Datatype'). | |
| 92 | 'symbol'('TICKET1','TICKET1','src_span'(4,10,4,17,114,7),'Datatype'). | |
| 93 | 'symbol'('Encrypt1','Encrypt1','src_span'(4,20,4,28,124,8),'Constructor of Datatype'). | |
| 94 | 'symbol'('TICKET2','TICKET2','src_span'(5,10,5,17,160,7),'Datatype'). | |
| 95 | 'symbol'('Encrypt2','Encrypt2','src_span'(5,20,5,28,170,8),'Constructor of Datatype'). | |
| 96 | 'symbol'('TICKET3','TICKET3','src_span'(6,10,6,17,205,7),'Datatype'). | |
| 97 | 'symbol'('Encrypt3','Encrypt3','src_span'(6,20,6,28,215,8),'Constructor of Datatype'). | |
| 98 | 'symbol'('MSG','MSG','src_span'(8,10,8,13,244,3),'Datatype'). | |
| 99 | 'symbol'('Msg1','Msg1','src_span'(8,20,8,24,254,4),'Constructor of Datatype'). | |
| 100 | 'symbol'('Msg2','Msg2','src_span'(9,21,9,25,301,4),'Constructor of Datatype'). | |
| 101 | 'symbol'('Msg3','Msg3','src_span'(10,21,10,25,349,4),'Constructor of Datatype'). | |
| 102 | 'symbol'('comm','comm','src_span'(12,9,12,13,385,4),'Channel'). | |
| 103 | 'symbol'('fake','fake','src_span'(12,15,12,19,391,4),'Channel'). | |
| 104 | 'symbol'('intercept','intercept','src_span'(12,21,12,30,397,9),'Channel'). | |
| 105 | 'symbol'('user','user','src_span'(13,9,13,13,420,4),'Channel'). | |
| 106 | 'symbol'('session','session','src_span'(13,15,13,22,426,7),'Channel'). | |
| 107 | 'symbol'('I_running','I_running','src_span'(13,24,13,33,435,9),'Channel'). | |
| 108 | 'symbol'('R_running','R_running','src_span'(14,8,14,17,453,9),'Channel'). | |
| 109 | 'symbol'('I_commit','I_commit','src_span'(14,19,14,27,464,8),'Channel'). | |
| 110 | 'symbol'('R_commit','R_commit','src_span'(14,29,14,37,474,8),'Channel'). | |
| 111 | 'symbol'('card','card','src_span'(16,7,16,11,506,4),'BuiltIn primitive'). | |
| 112 | 'symbol'('x','x','src_span'(16,17,16,18,516,1),'Ident (Prolog Variable)'). | |
| 113 | 'symbol'('x2','x','src_span'(17,17,17,18,548,1),'Ident (Prolog Variable)'). | |
| 114 | 'symbol'('x3','x','src_span'(18,17,18,18,580,1),'Ident (Prolog Variable)'). | |
| 115 | 'symbol'('x4','x','src_span'(19,17,19,18,612,1),'Ident (Prolog Variable)'). | |
| 116 | 'symbol'('key','key','src_span'(21,1,21,4,625,3),'Funktion or Process'). | |
| 117 | 'symbol'('B','B','src_span'(2,24,2,25,55,1),'Constructor of Datatype'). | |
| 118 | 'symbol'('A','A','src_span'(2,20,2,21,51,1),'Constructor of Datatype'). | |
| 119 | 'symbol'('C','C','src_span'(2,28,2,29,59,1),'Constructor of Datatype'). | |
| 120 | 'symbol'('INITIATOR','INITIATOR','src_span'(25,1,25,10,656,9),'Funktion or Process'). | |
| 121 | 'symbol'('a','a','src_span'(25,11,25,12,666,1),'Ident (Prolog Variable)'). | |
| 122 | 'symbol'('na','na','src_span'(25,13,25,15,668,2),'Ident (Prolog Variable)'). | |
| 123 | 'symbol'('b','b','src_span'(26,9,26,10,681,1),'Ident (Prolog Variable)'). | |
| 124 | 'symbol'('na2','na2','src_span'(29,32,29,35,771,3),'Ident (Prolog Variable)'). | |
| 125 | 'symbol'('nb','nb','src_span'(29,36,29,38,775,2),'Ident (Prolog Variable)'). | |
| 126 | 'symbol'('RESPONDER','RESPONDER','src_span'(37,1,37,10,885,9),'Funktion or Process'). | |
| 127 | 'symbol'('b2','b','src_span'(37,11,37,12,895,1),'Ident (Prolog Variable)'). | |
| 128 | 'symbol'('nb2','nb','src_span'(37,13,37,15,897,2),'Ident (Prolog Variable)'). | |
| 129 | 'symbol'('a2','a','src_span'(38,7,38,8,908,1),'Ident (Prolog Variable)'). | |
| 130 | 'symbol'('b3','b','src_span'(38,9,38,10,910,1),'Ident (Prolog Variable)'). | |
| 131 | 'symbol'('na3','na','src_span'(40,32,40,34,962,2),'Ident (Prolog Variable)'). | |
| 132 | 'symbol'('nb22','nb2','src_span'(42,32,42,35,1039,3),'Ident (Prolog Variable)'). | |
| 133 | 'symbol'('INITIATOR1','INITIATOR1','src_span'(48,1,48,11,1110,10),'Ident (Groundrep.)'). | |
| 134 | 'symbol'('RESPONDER1','RESPONDER1','src_span'(56,1,56,11,1293,10),'Ident (Groundrep.)'). | |
| 135 | 'symbol'('INTRUDER','INTRUDER','src_span'(64,1,64,9,1471,8),'Funktion or Process'). | |
| 136 | 'symbol'('m1s','m1s','src_span'(64,10,64,13,1480,3),'Ident (Prolog Variable)'). | |
| 137 | 'symbol'('m2s','m2s','src_span'(64,14,64,17,1484,3),'Ident (Prolog Variable)'). | |
| 138 | 'symbol'('m3s','m3s','src_span'(64,18,64,21,1488,3),'Ident (Prolog Variable)'). | |
| 139 | 'symbol'('ns','ns','src_span'(64,22,64,24,1492,2),'Ident (Prolog Variable)'). | |
| 140 | 'symbol'('a3','a','src_span'(77,19,77,20,2055,1),'Ident (Prolog Variable)'). | |
| 141 | 'symbol'('b4','b','src_span'(77,21,77,22,2057,1),'Ident (Prolog Variable)'). | |
| 142 | 'symbol'('Encrypt1','Encrypt1','src_span'(4,20,4,28,124,8),'Constructor of Datatype'). | |
| 143 | 'symbol'('k','k','src_span'(77,32,77,33,2068,1),'Ident (Prolog Variable)'). | |
| 144 | 'symbol'('n','n','src_span'(77,34,77,35,2070,1),'Ident (Prolog Variable)'). | |
| 145 | 'symbol'('a22','a2','src_span'(77,36,77,38,2072,2),'Ident (Prolog Variable)'). | |
| 146 | 'symbol'('union','union','src_span'(78,51,78,56,2127,5),'BuiltIn primitive'). | |
| 147 | 'symbol'('b5','b','src_span'(81,17,81,18,2230,1),'Ident (Prolog Variable)'). | |
| 148 | 'symbol'('a4','a','src_span'(81,19,81,20,2232,1),'Ident (Prolog Variable)'). | |
| 149 | 'symbol'('Encrypt2','Encrypt2','src_span'(5,20,5,28,170,8),'Constructor of Datatype'). | |
| 150 | 'symbol'('k2','k','src_span'(81,30,81,31,2243,1),'Ident (Prolog Variable)'). | |
| 151 | 'symbol'('n2','n','src_span'(81,32,81,33,2245,1),'Ident (Prolog Variable)'). | |
| 152 | 'symbol'('n22','n2','src_span'(81,34,81,36,2247,2),'Ident (Prolog Variable)'). | |
| 153 | 'symbol'('a5','a','src_span'(85,17,85,18,2408,1),'Ident (Prolog Variable)'). | |
| 154 | 'symbol'('b6','b','src_span'(85,19,85,20,2410,1),'Ident (Prolog Variable)'). | |
| 155 | 'symbol'('Encrypt3','Encrypt3','src_span'(6,20,6,28,215,8),'Constructor of Datatype'). | |
| 156 | 'symbol'('k3','k','src_span'(85,30,85,31,2421,1),'Ident (Prolog Variable)'). | |
| 157 | 'symbol'('n3','n','src_span'(85,32,85,33,2423,1),'Ident (Prolog Variable)'). | |
| 158 | 'symbol'('a6','a','src_span'(91,12,91,13,2630,1),'Ident (Prolog Variable)'). | |
| 159 | 'symbol'('b7','b','src_span'(91,14,91,15,2632,1),'Ident (Prolog Variable)'). | |
| 160 | 'symbol'('m','m','src_span'(91,16,91,17,2634,1),'Ident (Prolog Variable)'). | |
| 161 | 'symbol'('a7','a','src_span'(95,12,95,13,2741,1),'Ident (Prolog Variable)'). | |
| 162 | 'symbol'('b8','b','src_span'(95,14,95,15,2743,1),'Ident (Prolog Variable)'). | |
| 163 | 'symbol'('k4','k','src_span'(95,25,95,26,2754,1),'Ident (Prolog Variable)'). | |
| 164 | 'symbol'('n4','n','src_span'(95,27,95,28,2756,1),'Ident (Prolog Variable)'). | |
| 165 | 'symbol'('a23','a2','src_span'(95,32,95,34,2761,2),'Ident (Prolog Variable)'). | |
| 166 | 'symbol'('a8','a','src_span'(99,12,99,13,2880,1),'Ident (Prolog Variable)'). | |
| 167 | 'symbol'('b9','b','src_span'(99,14,99,15,2882,1),'Ident (Prolog Variable)'). | |
| 168 | 'symbol'('k5','k','src_span'(99,25,99,26,2893,1),'Ident (Prolog Variable)'). | |
| 169 | 'symbol'('n5','n','src_span'(99,27,99,28,2895,1),'Ident (Prolog Variable)'). | |
| 170 | 'symbol'('INTRUDERneu','INTRUDERneu','src_span'(101,1,101,12,2927,11),'Funktion or Process'). | |
| 171 | 'symbol'('m1s2','m1s','src_span'(101,13,101,16,2939,3),'Ident (Prolog Variable)'). | |
| 172 | 'symbol'('m2s2','m2s','src_span'(101,17,101,20,2943,3),'Ident (Prolog Variable)'). | |
| 173 | 'symbol'('m3s2','m3s','src_span'(101,21,101,24,2947,3),'Ident (Prolog Variable)'). | |
| 174 | 'symbol'('ns2','ns','src_span'(101,25,101,27,2951,2),'Ident (Prolog Variable)'). | |
| 175 | 'symbol'('union','union','src_span'(103,36,103,41,3042,5),'BuiltIn primitive'). | |
| 176 | 'symbol'('n6','n','src_span'(105,32,105,33,3103,1),'Ident (Prolog Variable)'). | |
| 177 | 'symbol'('a9','a','src_span'(105,37,105,38,3108,1),'Ident (Prolog Variable)'). | |
| 178 | 'symbol'('union','union','src_span'(109,28,109,33,3246,5),'BuiltIn primitive'). | |
| 179 | 'symbol'('m2','m','src_span'(111,16,111,17,3322,1),'Ident (Prolog Variable)'). | |
| 180 | 'symbol'('union','union','src_span'(115,36,115,41,3465,5),'BuiltIn primitive'). | |
| 181 | 'symbol'('n7','n','src_span'(117,32,117,33,3526,1),'Ident (Prolog Variable)'). | |
| 182 | 'symbol'('INTRUDER1','INTRUDER1','src_span'(121,1,121,10,3574,9),'Ident (Groundrep.)'). | |
| 183 | 'symbol'('AGENT','AGENT','src_span'(123,1,123,6,3618,5),'Ident (Groundrep.)'). | |
| 184 | 'symbol'('SYSTEM','SYSTEM','src_span'(125,1,125,7,3678,6),'Ident (Groundrep.)'). | |
| 185 | 'symbol'('Sigma','Sigma','src_span'(127,1,127,6,3735,5),'Ident (Groundrep.)'). | |
| 186 | 'symbol'('A1','A1','src_span'(130,1,130,3,3844,2),'Ident (Groundrep.)'). | |
| 187 | 'symbol'('RUN','RUN','src_span'(132,1,132,4,3889,3),'Ident (Groundrep.)'). | |
| 188 | 'symbol'('x5','x','src_span'(132,16,132,17,3904,1),'Ident (Prolog Variable)'). | |
| 189 | 'symbol'('diff','diff','src_span'(132,19,132,23,3907,4),'BuiltIn primitive'). | |
| 190 | 'symbol'('AR0','AR0','src_span'(134,1,134,4,3935,3),'Ident (Groundrep.)'). | |
| 191 | 'symbol'('AR','AR','src_span'(136,1,136,3,3985,2),'Ident (Groundrep.)'). | |
| 192 | 'symbol'('A2','A2','src_span'(138,1,138,3,4010,2),'Ident (Groundrep.)'). | |
| 193 | 'symbol'('RUN2','RUN2','src_span'(140,1,140,5,4055,4),'Ident (Groundrep.)'). | |
| 194 | 'symbol'('x6','x','src_span'(140,16,140,17,4070,1),'Ident (Prolog Variable)'). | |
| 195 | 'symbol'('diff','diff','src_span'(140,19,140,23,4073,4),'BuiltIn primitive'). | |
| 196 | 'symbol'('AI0','AI0','src_span'(142,1,142,4,4102,3),'Ident (Groundrep.)'). | |
| 197 | 'symbol'('AI','AI','src_span'(144,1,144,3,4152,2),'Ident (Groundrep.)'). |