This repository was archived by the owner on Feb 22, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathModel.aslan
915 lines (873 loc) · 73.7 KB
/
Model.aslan
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
% @specification(Model)
% @channel_model(ACM)
% @connector_name(AVANTSSAR ASLan++ Connector)
% @connector_version(1.3.9)
% @connector_options(-opt LUMP -hc ALL -gas)
section signature:
text > communication
text > cookie
text > fixedString
text > opid
text > pincode
text > slabel
text > userrequest
authentic_on : channel * agent -> fact
bilateral_conf_auth : channel * channel * agent * agent -> fact
ch : agent * agent * slabel -> channel
child : nat * nat -> fact
confidential_to : channel * agent -> fact
defaultPseudonym : agent * nat -> public_key
dishonest : agent -> fact
enrollmentDB : agent -> set(pair(agent, cookie))
hash : message -> message
link : channel * channel -> fact
pk : agent -> public_key
rcvd : agent * agent * message * channel -> fact
resilient : channel -> fact
sent : agent * agent * agent * message * channel -> fact
state_Browser : agent * nat * nat * agent * agent * agent * channel * channel * cookie * userrequest -> fact
state_EIC : agent * nat * nat * agent * agent * agent * channel * channel * channel * pincode * opid * agent -> fact
state_EICApp : agent * nat * nat * agent * agent * agent * agent * channel * channel * channel * channel * channel * channel * channel * opid * agent * pincode * userrequest -> fact
state_Environment : agent * nat * nat -> fact
state_FCMServer : agent * nat * nat * agent * agent * channel * channel * opid * userrequest -> fact
state_FCMService : agent * nat * nat * agent * agent * channel * channel * opid * userrequest -> fact
state_IdPServer : agent * nat * nat * agent * agent * agent * agent * agent * agent * channel * channel * channel * channel * cookie * opid * userrequest -> fact
state_SPServer : agent * nat * nat * agent * agent * agent * channel * channel * userrequest -> fact
state_Session : agent * nat * nat * agent * agent * agent * agent * agent * agent * agent * agent * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * channel * cookie * userrequest * pincode -> fact
state_User : agent * nat * nat * agent * agent * agent * agent * agent * channel * channel * channel * channel * channel * userrequest * pincode -> fact
succ : nat -> nat
unilateral_conf_auth : channel * channel * agent -> fact
weakly_authentic : channel -> fact
weakly_confidential : channel -> fact
section types:
ACM_Ch : channel
ACM_Msg : message
ACM_OS : agent
ACM_RS : agent
ACM_Rcv : agent
AM : message
AR : agent
AW : agent
Actor : agent
Browser : agent
Ch_B2IdPS : channel
Ch_B2SPS : channel
Ch_B2U : channel
Ch_EIC2EICApp : channel
Ch_EICApp2EIC : channel
Ch_EICApp2IdPS : channel
Ch_EICApp2U : channel
Ch_FCMSrv2FCMSvc : channel
Ch_FCMSrv2IdPS : channel
Ch_FCMSvc2EICApp : channel
Ch_FCMSvc2FCMSrv : channel
Ch_IdPS2B : channel
Ch_IdPS2EICApp : channel
Ch_IdPS2FCMSrv : channel
Ch_SPS2B : channel
Ch_U2B : channel
Ch_U2EIC : channel
Ch_U2EICApp : channel
EIC : agent
EICApp : agent
% @original_name(name=Actor)
E_S_Actor : agent
% @original_name(name=Actor)
E_S_B_Actor : agent
% @original_name(name=Ch_B2IdPS)
E_S_B_Ch_B2IdPS : channel
% @original_name(name=Ch_B2U)
E_S_B_Ch_B2U : channel
% @original_name(name=IID)
E_S_B_IID : nat
% @original_name(name=IdPCookie)
E_S_B_IdPCookie : cookie
% @original_name(name=IdPServer)
E_S_B_IdPServer : agent
% @original_name(name=Request)
E_S_B_Request : userrequest
% @original_name(name=Request; match=true)
E_S_B_Request_1 : userrequest
% @original_name(name=SL)
E_S_B_SL : nat
% @original_name(name=SPServer)
E_S_B_SPServer : agent
% @original_name(name=User)
E_S_B_User : agent
% @original_name(name=Actor)
E_S_EICA_Actor : agent
% @original_name(name=Ch_EIC2EICApp)
E_S_EICA_Ch_EIC2EICApp : channel
% @original_name(name=Ch_EICApp2EIC)
E_S_EICA_Ch_EICApp2EIC : channel
% @original_name(name=Ch_EICApp2IdPS)
E_S_EICA_Ch_EICApp2IdPS : channel
% @original_name(name=Ch_EICApp2U)
E_S_EICA_Ch_EICApp2U : channel
% @original_name(name=Ch_FCMSvc2EICApp)
E_S_EICA_Ch_FCMSvc2EICApp : channel
% @original_name(name=Ch_IdPS2EICApp)
E_S_EICA_Ch_IdPS2EICApp : channel
% @original_name(name=Ch_U2EICApp)
E_S_EICA_Ch_U2EICApp : channel
% @original_name(name=EIC)
E_S_EICA_EIC : agent
% @original_name(name=FCMService)
E_S_EICA_FCMService : agent
% @original_name(name=IID)
E_S_EICA_IID : nat
% @original_name(name=IdPServer)
E_S_EICA_IdPServer : agent
% @original_name(name=OpId)
E_S_EICA_OpId : opid
% @original_name(name=OpId; match=true)
E_S_EICA_OpId_1 : opid
% @original_name(name=PIN)
E_S_EICA_PIN : pincode
% @original_name(name=PIN; match=true)
E_S_EICA_PIN_1 : pincode
% @original_name(name=Request)
E_S_EICA_Request : userrequest
% @original_name(name=Request; match=true)
E_S_EICA_Request_1 : userrequest
% @original_name(name=SL)
E_S_EICA_SL : nat
% @original_name(name=SPServer)
E_S_EICA_SPServer : agent
% @original_name(name=SPServer; match=true)
E_S_EICA_SPServer_1 : agent
% @original_name(name=User)
E_S_EICA_User : agent
% @original_name(name=Actor)
E_S_EIC_Actor : agent
% @original_name(name=Ch_EIC2EICApp)
E_S_EIC_Ch_EIC2EICApp : channel
% @original_name(name=Ch_EICApp2EIC)
E_S_EIC_Ch_EICApp2EIC : channel
% @original_name(name=Ch_U2EIC)
E_S_EIC_Ch_U2EIC : channel
% @original_name(name=EICApp)
E_S_EIC_EICApp : agent
% @original_name(name=IID)
E_S_EIC_IID : nat
% @original_name(name=IdPServer)
E_S_EIC_IdPServer : agent
% @original_name(name=OpId)
E_S_EIC_OpId : opid
% @original_name(name=OpId; match=true)
E_S_EIC_OpId_1 : opid
% @original_name(name=PIN)
E_S_EIC_PIN : pincode
% @original_name(name=SL)
E_S_EIC_SL : nat
% @original_name(name=SPServer)
E_S_EIC_SPServer : agent
% @original_name(name=SPServer; match=true)
E_S_EIC_SPServer_1 : agent
% @original_name(name=User)
E_S_EIC_User : agent
% @original_name(name=Actor)
E_S_FCMS_Actor : agent
% @original_name(name=Actor)
E_S_FCMS_Actor_ : agent
% @original_name(name=Ch_FCMSrv2FCMSvc)
E_S_FCMS_Ch_FCMSrv2FCMSvc : channel
% @original_name(name=Ch_FCMSrv2FCMSvc)
E_S_FCMS_Ch_FCMSrv2FCMSvc_ : channel
% @original_name(name=Ch_FCMSvc2EICApp)
E_S_FCMS_Ch_FCMSvc2EICApp : channel
% @original_name(name=Ch_IdPS2FCMSrv)
E_S_FCMS_Ch_IdPS2FCMSrv : channel
% @original_name(name=EICApp)
E_S_FCMS_EICApp : agent
% @original_name(name=FCMServer)
E_S_FCMS_FCMServer : agent
% @original_name(name=FCMService)
E_S_FCMS_FCMService : agent
% @original_name(name=IID)
E_S_FCMS_IID : nat
% @original_name(name=IID)
E_S_FCMS_IID_ : nat
% @original_name(name=IdPServer)
E_S_FCMS_IdPServer : agent
% @original_name(name=OpId)
E_S_FCMS_OpId : opid
% @original_name(name=OpId)
E_S_FCMS_OpId_ : opid
% @original_name(name=OpId; match=true)
E_S_FCMS_OpId_1 : opid
% @original_name(name=OpId; match=true)
E_S_FCMS_OpId__1 : opid
% @original_name(name=Request)
E_S_FCMS_Request : userrequest
% @original_name(name=Request)
E_S_FCMS_Request_ : userrequest
% @original_name(name=Request; match=true)
E_S_FCMS_Request_1 : userrequest
% @original_name(name=Request; match=true)
E_S_FCMS_Request__1 : userrequest
% @original_name(name=SL)
E_S_FCMS_SL : nat
% @original_name(name=SL)
E_S_FCMS_SL_ : nat
% @original_name(name=IID)
E_S_IID : nat
% @original_name(name=Actor)
E_S_IPS_Actor : agent
% @original_name(name=Browser)
E_S_IPS_Browser : agent
% @original_name(name=Ch_B2IdPS)
E_S_IPS_Ch_B2IdPS : channel
% @original_name(name=Ch_EICApp2IdPS)
E_S_IPS_Ch_EICApp2IdPS : channel
% @original_name(name=Ch_IdPS2EICApp)
E_S_IPS_Ch_IdPS2EICApp : channel
% @original_name(name=Ch_IdPS2FCMSrv)
E_S_IPS_Ch_IdPS2FCMSrv : channel
% @original_name(name=EIC)
E_S_IPS_EIC : agent
% @original_name(name=EICApp)
E_S_IPS_EICApp : agent
% @original_name(name=FCMServer)
E_S_IPS_FCMServer : agent
% @original_name(name=IID)
E_S_IPS_IID : nat
% @original_name(name=IdPCookie)
E_S_IPS_IdPCookie : cookie
% @original_name(name=IdPCookie; match=true)
E_S_IPS_IdPCookie_1 : cookie
% @original_name(name=Request)
E_S_IPS_Request : userrequest
% @original_name(name=Request; match=true)
E_S_IPS_Request_1 : userrequest
% @original_name(name=SL)
E_S_IPS_SL : nat
% @original_name(name=SPServer)
E_S_IPS_SPServer : agent
% @original_name(name=User)
E_S_IPS_User : agent
% @original_name(name=SL)
E_S_SL : nat
% @original_name(name=Actor)
E_S_SPS_Actor : agent
% @original_name(name=Browser)
E_S_SPS_Browser : agent
% @original_name(name=Ch_B2SPS)
E_S_SPS_Ch_B2SPS : channel
% @original_name(name=Ch_SPS2B)
E_S_SPS_Ch_SPS2B : channel
% @original_name(name=IID)
E_S_SPS_IID : nat
% @original_name(name=IdPServer)
E_S_SPS_IdPServer : agent
% @original_name(name=Request)
E_S_SPS_Request : userrequest
% @original_name(name=SL)
E_S_SPS_SL : nat
% @original_name(name=User)
E_S_SPS_User : agent
% @original_name(name=Actor)
E_S_U_Actor : agent
% @original_name(name=Browser)
E_S_U_Browser : agent
% @original_name(name=Ch_B2U)
E_S_U_Ch_B2U : channel
% @original_name(name=Ch_EICApp2U)
E_S_U_Ch_EICApp2U : channel
% @original_name(name=Ch_U2B)
E_S_U_Ch_U2B : channel
% @original_name(name=Ch_U2EIC)
E_S_U_Ch_U2EIC : channel
% @original_name(name=Ch_U2EICApp)
E_S_U_Ch_U2EICApp : channel
% @original_name(name=EIC)
E_S_U_EIC : agent
% @original_name(name=EICApp)
E_S_U_EICApp : agent
% @original_name(name=IID)
E_S_U_IID : nat
% @original_name(name=IdPServer)
E_S_U_IdPServer : agent
% @original_name(name=PIN)
E_S_U_PIN : pincode
% @original_name(name=Request)
E_S_U_Request : userrequest
% @original_name(name=SL)
E_S_U_SL : nat
% @original_name(name=SPServer)
E_S_U_SPServer : agent
% @original_name(name=IID)
E_aUatSP_IID : nat
EnrollmentDB_arg_1 : agent
FCMServer : agent
FCMService : agent
FM : message
FR : agent
FW : agent
Hash_arg_1 : message
IID : nat
IID1 : nat
IID2 : nat
% @original_name(name=IID; fresh=true)
IID_1 : nat
% @original_name(name=IID; fresh=true)
IID_10 : nat
% @original_name(name=IID; fresh=true)
IID_2 : nat
% @original_name(name=IID; fresh=true)
IID_3 : nat
% @original_name(name=IID; fresh=true)
IID_4 : nat
% @original_name(name=IID; fresh=true)
IID_5 : nat
% @original_name(name=IID; fresh=true)
IID_6 : nat
% @original_name(name=IID; fresh=true)
IID_7 : nat
% @original_name(name=IID; fresh=true)
IID_8 : nat
% @original_name(name=IID; fresh=true)
IID_9 : nat
IdPCookie : cookie
IdPServer : agent
OpId : opid
% @original_name(name=OpId; fresh=true)
OpId_1 : opid
PIN : pincode
Pk_arg_1 : agent
Request : userrequest
SL : nat
SPServer : agent
Succ_arg_1 : nat
User : agent
auth : slabel
auth_User_authn_to_SP : protocol_id
browser : agent
ch_B2IdPS : channel
ch_B2IdPS_2 : channel
ch_B2SPS : channel
ch_B2SPS_2 : channel
ch_B2U : channel
ch_B2U_2 : channel
ch_EIC2EICApp : channel
ch_EIC2EICApp_2 : channel
ch_EICApp2EIC : channel
ch_EICApp2EIC_2 : channel
ch_EICApp2IdPS : channel
ch_EICApp2IdPS_2 : channel
ch_EICApp2U : channel
ch_EICApp2U_2 : channel
ch_FCMSrv2FCMSvc : channel
ch_FCMSrv2FCMSvc_2 : channel
ch_FCMSrv2IdPS : channel
ch_FCMSrv2IdPS_2 : channel
ch_FCMSvc2EICApp : channel
ch_FCMSvc2EICApp_2 : channel
ch_FCMSvc2FCMSrv : channel
ch_FCMSvc2FCMSrv_2 : channel
ch_IdPS2B : channel
ch_IdPS2B_2 : channel
ch_IdPS2EICApp : channel
ch_IdPS2EICApp_2 : channel
ch_IdPS2FCMSrv : channel
ch_IdPS2FCMSrv_2 : channel
ch_SPS2B : channel
ch_SPS2B_2 : channel
ch_U2B : channel
ch_U2B_2 : channel
ch_U2EIC : channel
ch_U2EICApp : channel
ch_U2EICApp_2 : channel
ch_U2EIC_2 : channel
conf : slabel
dummy_agent_1 : agent
dummy_agent_2 : agent
dummy_agent_3 : agent
dummy_agent_4 : agent
dummy_cookie_1 : cookie
dummy_nat : nat
dummy_opid_1 : opid
dummy_opid_2 : opid
dummy_opid_3 : opid
dummy_opid_4 : opid
dummy_opid_5 : opid
dummy_pincode_1 : pincode
dummy_userrequest_1 : userrequest
dummy_userrequest_2 : userrequest
dummy_userrequest_3 : userrequest
dummy_userrequest_4 : userrequest
dummy_userrequest_5 : userrequest
eic : agent
eicapp : agent
false : fact
fcmsrv : agent
fcmsvc : agent
fresh_User_authn_to_SP : protocol_id
idpcookie : cookie
idps : agent
pin : pincode
regular : slabel
request1 : userrequest
request2 : userrequest
res : slabel
res_auth : slabel
res_conf : slabel
res_sec : slabel
root : agent
sec : slabel
sps : agent
stringOK : fixedString
true : fact
useEIC : communication
user : agent
section inits:
% @new_instance(new_entity=Environment; Actor=root; IID=0; SL=1)
initial_state init :=
child(dummy_nat, 0).
dishonest(i).
iknows(0).
iknows(auth).
iknows(browser).
iknows(conf).
iknows(eic).
iknows(eicapp).
iknows(fcmsrv).
iknows(fcmsvc).
iknows(i).
iknows(idps).
iknows(inv(pk(i))).
iknows(regular).
iknows(request1).
iknows(request2).
iknows(res).
iknows(res_auth).
iknows(res_conf).
iknows(res_sec).
iknows(root).
iknows(sec).
iknows(sps).
iknows(stringOK).
iknows(useEIC).
iknows(user).
state_Environment(root, 0, 1).
true
section hornClauses:
hc public_pk(Pk_arg_1) :=
iknows(pk(Pk_arg_1)) :-
iknows(Pk_arg_1)
hc public_hash(Hash_arg_1) :=
iknows(hash(Hash_arg_1)) :-
iknows(Hash_arg_1)
hc public_succ(Succ_arg_1) :=
iknows(succ(Succ_arg_1)) :-
iknows(Succ_arg_1)
hc inv_succ_1(Succ_arg_1) :=
iknows(Succ_arg_1) :-
iknows(succ(Succ_arg_1))
hc inv_enrollmentDB_1(EnrollmentDB_arg_1) :=
iknows(EnrollmentDB_arg_1) :-
iknows(enrollmentDB(EnrollmentDB_arg_1))
section rules:
%retract facts
%sent(ACM_RS,ACM_OS,ACM_Rcv,ACM_Msg,ACM_Ch)
%introduce facts
%rcvd(ACM_Rcv,ACM_OS,ACM_Msg,ACM_Ch)
step step_001_ACM(ACM_Ch, ACM_Msg, ACM_OS, ACM_RS, ACM_Rcv) :=
sent(ACM_RS, ACM_OS, ACM_Rcv, ACM_Msg, ACM_Ch)
=>
rcvd(ACM_Rcv, ACM_OS, ACM_Msg, ACM_Ch)
% @introduce(entity=Environment; iid=IID; line=324; fact=contains(pair(user, idpcookie), enrollmentDB(idps)))
% @new_instance(entity=Environment; iid=IID; line=327; new_entity=Session; Actor=dummy_agent_1; IID=IID_1; SL=1; EIC=eic; FCMService=fcmsvc; EICApp=eicapp; User=user; Browser=browser; SPServer=sps; IdPServer=idps; FCMServer=fcmsrv; Ch_B2IdPS=ch_B2IdPS; Ch_IdPS2B=ch_IdPS2B; Ch_U2B=ch_U2B; Ch_B2U=ch_B2U; Ch_IdPS2FCMSrv=ch_IdPS2FCMSrv; Ch_FCMSrv2IdPS=ch_FCMSrv2IdPS; Ch_FCMSrv2FCMSvc=ch_FCMSrv2FCMSvc; Ch_FCMSvc2FCMSrv=ch_FCMSvc2FCMSrv; Ch_FCMSvc2EICApp=ch_FCMSvc2EICApp; Ch_U2EICApp=ch_U2EICApp; Ch_EICApp2U=ch_EICApp2U; Ch_EICApp2IdPS=ch_EICApp2IdPS; Ch_IdPS2EICApp=ch_IdPS2EICApp; Ch_EICApp2EIC=ch_EICApp2EIC; Ch_EIC2EICApp=ch_EIC2EICApp; Ch_B2SPS=ch_B2SPS; Ch_SPS2B=ch_SPS2B; Ch_U2EIC=ch_U2EIC; IdPCookie=idpcookie; Request=request1; PIN=pin)
% @new_instance(entity=Environment; iid=IID; line=328; new_entity=Session; Actor=dummy_agent_2; IID=IID_2; SL=1; EIC=eic; FCMService=fcmsvc; EICApp=eicapp; User=user; Browser=browser; SPServer=sps; IdPServer=idps; FCMServer=fcmsrv; Ch_B2IdPS=ch_B2IdPS_2; Ch_IdPS2B=ch_IdPS2B_2; Ch_U2B=ch_U2B_2; Ch_B2U=ch_B2U_2; Ch_IdPS2FCMSrv=ch_IdPS2FCMSrv_2; Ch_FCMSrv2IdPS=ch_FCMSrv2IdPS_2; Ch_FCMSrv2FCMSvc=ch_FCMSrv2FCMSvc_2; Ch_FCMSvc2FCMSrv=ch_FCMSvc2FCMSrv_2; Ch_FCMSvc2EICApp=ch_FCMSvc2EICApp_2; Ch_U2EICApp=ch_U2EICApp_2; Ch_EICApp2U=ch_EICApp2U_2; Ch_EICApp2IdPS=ch_EICApp2IdPS_2; Ch_IdPS2EICApp=ch_IdPS2EICApp_2; Ch_EICApp2EIC=ch_EICApp2EIC_2; Ch_EIC2EICApp=ch_EIC2EICApp_2; Ch_B2SPS=ch_B2SPS_2; Ch_SPS2B=ch_SPS2B_2; Ch_U2EIC=ch_U2EIC_2; IdPCookie=idpcookie; Request=request2; PIN=pin)
% @step_label(entity=Environment; iid=IID; line=328; variable=SL; term=4)
step step_002_Environment__line_324(Actor, IID, IID_1, IID_2) :=
state_Environment(Actor, IID, 1)
=[exists IID_1, IID_2]=>
child(IID, IID_1).
child(IID, IID_2).
contains(pair(user, idpcookie), enrollmentDB(idps)).
state_Environment(Actor, IID, 4).
state_Session(dummy_agent_1, IID_1, 1, eic, fcmsvc, eicapp, user, browser, sps, idps, fcmsrv, ch_B2IdPS, ch_IdPS2B, ch_U2B, ch_B2U, ch_IdPS2FCMSrv, ch_FCMSrv2IdPS, ch_FCMSrv2FCMSvc, ch_FCMSvc2FCMSrv, ch_FCMSvc2EICApp, ch_U2EICApp, ch_EICApp2U, ch_EICApp2IdPS, ch_IdPS2EICApp, ch_EICApp2EIC, ch_EIC2EICApp, ch_B2SPS, ch_SPS2B, ch_U2EIC, idpcookie, request1, pin).
state_Session(dummy_agent_2, IID_2, 1, eic, fcmsvc, eicapp, user, browser, sps, idps, fcmsrv, ch_B2IdPS_2, ch_IdPS2B_2, ch_U2B_2, ch_B2U_2, ch_IdPS2FCMSrv_2, ch_FCMSrv2IdPS_2, ch_FCMSrv2FCMSvc_2, ch_FCMSvc2FCMSrv_2, ch_FCMSvc2EICApp_2, ch_U2EICApp_2, ch_EICApp2U_2, ch_EICApp2IdPS_2, ch_IdPS2EICApp_2, ch_EICApp2EIC_2, ch_EIC2EICApp_2, ch_B2SPS_2, ch_SPS2B_2, ch_U2EIC_2, idpcookie, request2, pin)
% @introduce(entity=Session; iid=E_S_IID; line=261; fact=authentic_on(Ch_U2B, User))
% @introduce(entity=Session; iid=E_S_IID; line=266; fact=authentic_on(Ch_U2EICApp, User))
% @introduce(entity=Session; iid=E_S_IID; line=271; fact=authentic_on(Ch_U2EIC, User))
% @introduce(entity=Session; iid=E_S_IID; line=276; fact=confidential_to(Ch_U2EICApp, EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=292; fact=confidential_to(Ch_FCMSvc2EICApp, EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=293; fact=authentic_on(Ch_EICApp2U, EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=298; fact=weakly_authentic(Ch_B2IdPS))
% @introduce(entity=Session; iid=E_S_IID; line=298; fact=weakly_confidential(Ch_IdPS2B))
% @introduce(entity=Session; iid=E_S_IID; line=298; fact=link(Ch_B2IdPS, Ch_IdPS2B))
% @introduce(entity=Session; iid=E_S_IID; line=298; fact=confidential_to(Ch_B2IdPS, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=298; fact=authentic_on(Ch_IdPS2B, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=299; fact=weakly_authentic(Ch_B2SPS))
% @introduce(entity=Session; iid=E_S_IID; line=299; fact=weakly_confidential(Ch_SPS2B))
% @introduce(entity=Session; iid=E_S_IID; line=299; fact=link(Ch_B2SPS, Ch_SPS2B))
% @introduce(entity=Session; iid=E_S_IID; line=299; fact=confidential_to(Ch_B2SPS, SPServer))
% @introduce(entity=Session; iid=E_S_IID; line=299; fact=authentic_on(Ch_SPS2B, SPServer))
% @introduce(entity=Session; iid=E_S_IID; line=300; fact=authentic_on(Ch_IdPS2FCMSrv, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=300; fact=confidential_to(Ch_FCMSrv2IdPS, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=300; fact=confidential_to(Ch_IdPS2FCMSrv, FCMServer))
% @introduce(entity=Session; iid=E_S_IID; line=300; fact=authentic_on(Ch_FCMSrv2IdPS, FCMServer))
% @introduce(entity=Session; iid=E_S_IID; line=301; fact=weakly_authentic(Ch_FCMSvc2FCMSrv))
% @introduce(entity=Session; iid=E_S_IID; line=301; fact=weakly_confidential(Ch_FCMSrv2FCMSvc))
% @introduce(entity=Session; iid=E_S_IID; line=301; fact=link(Ch_FCMSvc2FCMSrv, Ch_FCMSrv2FCMSvc))
% @introduce(entity=Session; iid=E_S_IID; line=301; fact=confidential_to(Ch_FCMSvc2FCMSrv, FCMServer))
% @introduce(entity=Session; iid=E_S_IID; line=301; fact=authentic_on(Ch_FCMSrv2FCMSvc, FCMServer))
% @introduce(entity=Session; iid=E_S_IID; line=302; fact=authentic_on(Ch_FCMSvc2EICApp, FCMService))
% @introduce(entity=Session; iid=E_S_IID; line=303; fact=weakly_authentic(Ch_EICApp2IdPS))
% @introduce(entity=Session; iid=E_S_IID; line=303; fact=weakly_confidential(Ch_IdPS2EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=303; fact=link(Ch_EICApp2IdPS, Ch_IdPS2EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=303; fact=confidential_to(Ch_EICApp2IdPS, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=303; fact=authentic_on(Ch_IdPS2EICApp, IdPServer))
% @introduce(entity=Session; iid=E_S_IID; line=304; fact=weakly_authentic(Ch_EICApp2EIC))
% @introduce(entity=Session; iid=E_S_IID; line=304; fact=weakly_confidential(Ch_EIC2EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=304; fact=link(Ch_EICApp2EIC, Ch_EIC2EICApp))
% @introduce(entity=Session; iid=E_S_IID; line=304; fact=confidential_to(Ch_EICApp2EIC, EIC))
% @introduce(entity=Session; iid=E_S_IID; line=304; fact=authentic_on(Ch_EIC2EICApp, EIC))
% @new_instance(entity=Session; iid=E_S_IID; line=306; new_entity=User; Actor=User; IID=IID_3; SL=1; Browser=Browser; EICApp=EICApp; SPServer=SPServer; IdPServer=IdPServer; EIC=EIC; Ch_U2B=Ch_U2B; Ch_B2U=Ch_B2U; Ch_EICApp2U=Ch_EICApp2U; Ch_U2EICApp=Ch_U2EICApp; Ch_U2EIC=Ch_U2EIC; Request=Request; PIN=PIN)
% @new_instance(entity=Session; iid=E_S_IID; line=307; new_entity=Browser; Actor=Browser; IID=IID_4; SL=1; User=User; IdPServer=IdPServer; SPServer=SPServer; Ch_B2U=Ch_B2U; Ch_B2IdPS=Ch_B2IdPS; IdPCookie=IdPCookie; Request=dummy_userrequest_1)
% @new_instance(entity=Session; iid=E_S_IID; line=308; new_entity=SPServer; Actor=SPServer; IID=IID_5; SL=1; Browser=Browser; IdPServer=IdPServer; User=User; Ch_B2SPS=Ch_B2SPS; Ch_SPS2B=Ch_SPS2B; Request=Request)
% @new_instance(entity=Session; iid=E_S_IID; line=309; new_entity=IdPServer; Actor=IdPServer; IID=IID_6; SL=1; FCMServer=FCMServer; EICApp=EICApp; User=User; SPServer=SPServer; Browser=Browser; EIC=EIC; Ch_B2IdPS=Ch_B2IdPS; Ch_IdPS2FCMSrv=Ch_IdPS2FCMSrv; Ch_EICApp2IdPS=Ch_EICApp2IdPS; Ch_IdPS2EICApp=Ch_IdPS2EICApp; IdPCookie=dummy_cookie_1; OpId=dummy_opid_1; Request=dummy_userrequest_2)
% @new_instance(entity=Session; iid=E_S_IID; line=310; new_entity=FCMServer; Actor=FCMServer; IID=IID_7; SL=1; IdPServer=IdPServer; FCMService=FCMService; Ch_IdPS2FCMSrv=Ch_IdPS2FCMSrv; Ch_FCMSrv2FCMSvc=Ch_FCMSrv2FCMSvc; OpId=dummy_opid_2; Request=dummy_userrequest_3)
% @new_instance(entity=Session; iid=E_S_IID; line=311; new_entity=FCMService; Actor=FCMService; IID=IID_8; SL=1; FCMServer=FCMServer; EICApp=EICApp; Ch_FCMSrv2FCMSvc=Ch_FCMSrv2FCMSvc; Ch_FCMSvc2EICApp=Ch_FCMSvc2EICApp; OpId=dummy_opid_3; Request=dummy_userrequest_4)
% @new_instance(entity=Session; iid=E_S_IID; line=312; new_entity=EICApp; Actor=EICApp; IID=IID_9; SL=1; FCMService=FCMService; User=User; IdPServer=IdPServer; EIC=EIC; Ch_FCMSvc2EICApp=Ch_FCMSvc2EICApp; Ch_EICApp2U=Ch_EICApp2U; Ch_U2EICApp=Ch_U2EICApp; Ch_EICApp2IdPS=Ch_EICApp2IdPS; Ch_IdPS2EICApp=Ch_IdPS2EICApp; Ch_EICApp2EIC=Ch_EICApp2EIC; Ch_EIC2EICApp=Ch_EIC2EICApp; OpId=dummy_opid_4; SPServer=dummy_agent_3; PIN=dummy_pincode_1; Request=dummy_userrequest_5)
% @new_instance(entity=Session; iid=E_S_IID; line=313; new_entity=EIC; Actor=EIC; IID=IID_10; SL=1; EICApp=EICApp; IdPServer=IdPServer; User=User; Ch_EICApp2EIC=Ch_EICApp2EIC; Ch_EIC2EICApp=Ch_EIC2EICApp; Ch_U2EIC=Ch_U2EIC; PIN=PIN; OpId=dummy_opid_5; SPServer=dummy_agent_4)
% @step_label(entity=Session; iid=E_S_IID; line=313; variable=SL; term=45)
step step_003_Session__line_261(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_IID, FCMServer, FCMService, IID_10, IID_3, IID_4, IID_5, IID_6, IID_7, IID_8, IID_9, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
not(dishonest(E_S_Actor)).
state_Session(E_S_Actor, E_S_IID, 1, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=[exists IID_10, IID_3, IID_4, IID_5, IID_6, IID_7, IID_8, IID_9]=>
authentic_on(Ch_EIC2EICApp, EIC).
authentic_on(Ch_EICApp2U, EICApp).
authentic_on(Ch_FCMSrv2FCMSvc, FCMServer).
authentic_on(Ch_FCMSrv2IdPS, FCMServer).
authentic_on(Ch_FCMSvc2EICApp, FCMService).
authentic_on(Ch_IdPS2B, IdPServer).
authentic_on(Ch_IdPS2EICApp, IdPServer).
authentic_on(Ch_IdPS2FCMSrv, IdPServer).
authentic_on(Ch_SPS2B, SPServer).
authentic_on(Ch_U2B, User).
authentic_on(Ch_U2EIC, User).
authentic_on(Ch_U2EICApp, User).
child(E_S_IID, IID_10).
child(E_S_IID, IID_3).
child(E_S_IID, IID_4).
child(E_S_IID, IID_5).
child(E_S_IID, IID_6).
child(E_S_IID, IID_7).
child(E_S_IID, IID_8).
child(E_S_IID, IID_9).
confidential_to(Ch_B2IdPS, IdPServer).
confidential_to(Ch_B2SPS, SPServer).
confidential_to(Ch_EICApp2EIC, EIC).
confidential_to(Ch_EICApp2IdPS, IdPServer).
confidential_to(Ch_FCMSrv2IdPS, IdPServer).
confidential_to(Ch_FCMSvc2EICApp, EICApp).
confidential_to(Ch_FCMSvc2FCMSrv, FCMServer).
confidential_to(Ch_IdPS2FCMSrv, FCMServer).
confidential_to(Ch_U2EICApp, EICApp).
link(Ch_B2IdPS, Ch_IdPS2B).
link(Ch_B2SPS, Ch_SPS2B).
link(Ch_EICApp2EIC, Ch_EIC2EICApp).
link(Ch_EICApp2IdPS, Ch_IdPS2EICApp).
link(Ch_FCMSvc2FCMSrv, Ch_FCMSrv2FCMSvc).
state_Browser(Browser, IID_4, 1, User, IdPServer, SPServer, Ch_B2U, Ch_B2IdPS, IdPCookie, dummy_userrequest_1).
state_EIC(EIC, IID_10, 1, EICApp, IdPServer, User, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_U2EIC, PIN, dummy_opid_5, dummy_agent_4).
state_EICApp(EICApp, IID_9, 1, FCMService, User, IdPServer, EIC, Ch_FCMSvc2EICApp, Ch_EICApp2U, Ch_U2EICApp, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, dummy_opid_4, dummy_agent_3, dummy_pincode_1, dummy_userrequest_5).
state_FCMServer(FCMServer, IID_7, 1, IdPServer, FCMService, Ch_IdPS2FCMSrv, Ch_FCMSrv2FCMSvc, dummy_opid_2, dummy_userrequest_3).
state_FCMService(FCMService, IID_8, 1, FCMServer, EICApp, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2EICApp, dummy_opid_3, dummy_userrequest_4).
state_IdPServer(IdPServer, IID_6, 1, FCMServer, EICApp, User, SPServer, Browser, EIC, Ch_B2IdPS, Ch_IdPS2FCMSrv, Ch_EICApp2IdPS, Ch_IdPS2EICApp, dummy_cookie_1, dummy_opid_1, dummy_userrequest_2).
state_SPServer(SPServer, IID_5, 1, Browser, IdPServer, User, Ch_B2SPS, Ch_SPS2B, Request).
state_Session(E_S_Actor, E_S_IID, 45, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN).
state_User(User, IID_3, 1, Browser, EICApp, SPServer, IdPServer, EIC, Ch_U2B, Ch_B2U, Ch_EICApp2U, Ch_U2EICApp, Ch_U2EIC, Request, PIN).
weakly_authentic(Ch_B2IdPS).
weakly_authentic(Ch_B2SPS).
weakly_authentic(Ch_EICApp2EIC).
weakly_authentic(Ch_EICApp2IdPS).
weakly_authentic(Ch_FCMSvc2FCMSrv).
weakly_confidential(Ch_EIC2EICApp).
weakly_confidential(Ch_FCMSrv2FCMSvc).
weakly_confidential(Ch_IdPS2B).
weakly_confidential(Ch_IdPS2EICApp).
weakly_confidential(Ch_SPS2B)
% @communication(entity=User; iid=E_S_U_IID; line=53; sender=E_S_U_Actor; receiver=E_S_U_Browser; payload=E_S_U_Request; channel=E_S_U_Ch_U2B; fact=sent(E_S_U_Actor, E_S_U_Actor, E_S_U_Browser, E_S_U_Request, E_S_U_Ch_U2B); direction=send)
% @introduce(entity=User; iid=E_S_U_IID; line=53; fact=witness(E_S_U_Actor, E_S_U_SPServer, auth_User_authn_to_SP, E_S_U_Request))
% @step_label(entity=User; iid=E_S_U_IID; line=53; variable=SL; term=2)
step step_004_User__line_53(E_S_U_Actor, E_S_U_Browser, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2B, E_S_U_Ch_U2EIC, E_S_U_Ch_U2EICApp, E_S_U_EIC, E_S_U_EICApp, E_S_U_IID, E_S_U_IdPServer, E_S_U_PIN, E_S_U_Request, E_S_U_SPServer) :=
not(dishonest(E_S_U_Actor)).
state_User(E_S_U_Actor, E_S_U_IID, 1, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
=>
sent(E_S_U_Actor, E_S_U_Actor, E_S_U_Browser, E_S_U_Request, E_S_U_Ch_U2B).
state_User(E_S_U_Actor, E_S_U_IID, 2, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN).
witness(E_S_U_Actor, E_S_U_SPServer, auth_User_authn_to_SP, E_S_U_Request)
% @communication_guard(entity=User; iid=E_S_U_IID; line=56; sender=E_S_U_Browser; receiver=E_S_U_Actor; payload=E_S_U_IdPServer; channel=E_S_U_Ch_B2U; fact=rcvd(E_S_U_Actor, E_S_U_Browser, E_S_U_IdPServer, E_S_U_Ch_B2U); direction=receive)
% @communication(entity=User; iid=E_S_U_IID; line=57; sender=E_S_U_Actor; receiver=E_S_U_Browser; payload=E_S_U_Actor; channel=E_S_U_Ch_U2B; fact=sent(E_S_U_Actor, E_S_U_Actor, E_S_U_Browser, E_S_U_Actor, E_S_U_Ch_U2B); direction=send)
% @step_label(entity=User; iid=E_S_U_IID; line=57; variable=SL; term=4)
step step_005_User__line_56(E_S_U_Actor, E_S_U_Browser, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2B, E_S_U_Ch_U2EIC, E_S_U_Ch_U2EICApp, E_S_U_EIC, E_S_U_EICApp, E_S_U_IID, E_S_U_IdPServer, E_S_U_PIN, E_S_U_Request, E_S_U_SPServer) :=
rcvd(E_S_U_Actor, E_S_U_Browser, E_S_U_IdPServer, E_S_U_Ch_B2U).
state_User(E_S_U_Actor, E_S_U_IID, 2, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
=>
sent(E_S_U_Actor, E_S_U_Actor, E_S_U_Browser, E_S_U_Actor, E_S_U_Ch_U2B).
state_User(E_S_U_Actor, E_S_U_IID, 4, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
% @communication_guard(entity=User; iid=E_S_U_IID; line=60; sender=E_S_U_EICApp; receiver=E_S_U_Actor; payload=E_S_U_Request; channel=E_S_U_Ch_EICApp2U; fact=rcvd(E_S_U_Actor, E_S_U_EICApp, E_S_U_Request, E_S_U_Ch_EICApp2U); direction=receive)
% @communication(entity=User; iid=E_S_U_IID; line=61; sender=E_S_U_Actor; receiver=E_S_U_EICApp; payload=stringOK; channel=E_S_U_Ch_U2EICApp; fact=sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EICApp, stringOK, E_S_U_Ch_U2EICApp); direction=send)
% @step_label(entity=User; iid=E_S_U_IID; line=61; variable=SL; term=6)
step step_006_User__line_60(E_S_U_Actor, E_S_U_Browser, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2B, E_S_U_Ch_U2EIC, E_S_U_Ch_U2EICApp, E_S_U_EIC, E_S_U_EICApp, E_S_U_IID, E_S_U_IdPServer, E_S_U_PIN, E_S_U_Request, E_S_U_SPServer) :=
rcvd(E_S_U_Actor, E_S_U_EICApp, E_S_U_Request, E_S_U_Ch_EICApp2U).
state_User(E_S_U_Actor, E_S_U_IID, 4, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
=>
sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EICApp, stringOK, E_S_U_Ch_U2EICApp).
state_User(E_S_U_Actor, E_S_U_IID, 6, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
% @communication_guard(entity=User; iid=E_S_U_IID; line=64; sender=E_S_U_EICApp; receiver=E_S_U_Actor; payload=E_S_U_EICApp; channel=E_S_U_Ch_EICApp2U; fact=rcvd(E_S_U_Actor, E_S_U_EICApp, E_S_U_EICApp, E_S_U_Ch_EICApp2U); direction=receive)
% @communication(entity=User; iid=E_S_U_IID; line=65; sender=E_S_U_Actor; receiver=E_S_U_EICApp; payload=E_S_U_PIN; channel=E_S_U_Ch_U2EICApp; fact=sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EICApp, E_S_U_PIN, E_S_U_Ch_U2EICApp); direction=send)
% @communication(entity=User; iid=E_S_U_IID; line=66; sender=E_S_U_Actor; receiver=E_S_U_EIC; payload=useEIC; channel=E_S_U_Ch_U2EIC; fact=sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EIC, useEIC, E_S_U_Ch_U2EIC); direction=send)
% @step_label(entity=User; iid=E_S_U_IID; line=66; variable=SL; term=9)
step step_007_User__line_64(E_S_U_Actor, E_S_U_Browser, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2B, E_S_U_Ch_U2EIC, E_S_U_Ch_U2EICApp, E_S_U_EIC, E_S_U_EICApp, E_S_U_IID, E_S_U_IdPServer, E_S_U_PIN, E_S_U_Request, E_S_U_SPServer) :=
rcvd(E_S_U_Actor, E_S_U_EICApp, E_S_U_EICApp, E_S_U_Ch_EICApp2U).
state_User(E_S_U_Actor, E_S_U_IID, 6, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
=>
sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EIC, useEIC, E_S_U_Ch_U2EIC).
sent(E_S_U_Actor, E_S_U_Actor, E_S_U_EICApp, E_S_U_PIN, E_S_U_Ch_U2EICApp).
state_User(E_S_U_Actor, E_S_U_IID, 9, E_S_U_Browser, E_S_U_EICApp, E_S_U_SPServer, E_S_U_IdPServer, E_S_U_EIC, E_S_U_Ch_U2B, E_S_U_Ch_B2U, E_S_U_Ch_EICApp2U, E_S_U_Ch_U2EICApp, E_S_U_Ch_U2EIC, E_S_U_Request, E_S_U_PIN)
% @communication_guard(entity=Browser; iid=E_S_B_IID; line=83; sender=E_S_B_User; receiver=E_S_B_Actor; payload=E_S_B_Request_1; channel=Ch_U2B; fact=rcvd(E_S_B_Actor, E_S_B_User, E_S_B_Request_1, Ch_U2B); direction=receive)
% @match(entity=Browser; iid=E_S_B_IID; line=83; variable=Request; term=E_S_B_Request_1)
% @communication(entity=Browser; iid=E_S_B_IID; line=84; sender=E_S_B_Actor; receiver=E_S_B_SPServer; payload=E_S_B_Request_1; channel=Ch_B2SPS; fact=sent(E_S_B_Actor, E_S_B_Actor, E_S_B_SPServer, E_S_B_Request_1, Ch_B2SPS); direction=send)
% @step_label(entity=Browser; iid=E_S_B_IID; line=84; variable=SL; term=3)
step step_008_Browser__line_83(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_B_Actor, E_S_B_Ch_B2IdPS, E_S_B_Ch_B2U, E_S_B_IID, E_S_B_IdPCookie, E_S_B_IdPServer, E_S_B_Request, E_S_B_Request_1, E_S_B_SPServer, E_S_B_User, E_S_IID, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_B_IID).
not(dishonest(E_S_B_Actor)).
rcvd(E_S_B_Actor, E_S_B_User, E_S_B_Request_1, Ch_U2B).
state_Browser(E_S_B_Actor, E_S_B_IID, 1, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_B_IID).
sent(E_S_B_Actor, E_S_B_Actor, E_S_B_SPServer, E_S_B_Request_1, Ch_B2SPS).
state_Browser(E_S_B_Actor, E_S_B_IID, 3, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request_1).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=Browser; iid=E_S_B_IID; line=87; sender=E_S_B_SPServer; receiver=E_S_B_Actor; payload=E_S_B_Request; channel=Ch_SPS2B; fact=rcvd(E_S_B_Actor, E_S_B_SPServer, E_S_B_Request, Ch_SPS2B); direction=receive)
% @communication(entity=Browser; iid=E_S_B_IID; line=88; sender=E_S_B_Actor; receiver=E_S_B_IdPServer; payload=E_S_B_Request; channel=E_S_B_Ch_B2IdPS; fact=sent(E_S_B_Actor, E_S_B_Actor, E_S_B_IdPServer, E_S_B_Request, E_S_B_Ch_B2IdPS); direction=send)
% @step_label(entity=Browser; iid=E_S_B_IID; line=88; variable=SL; term=5)
step step_009_Browser__line_87(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_B_Actor, E_S_B_Ch_B2IdPS, E_S_B_Ch_B2U, E_S_B_IID, E_S_B_IdPCookie, E_S_B_IdPServer, E_S_B_Request, E_S_B_SPServer, E_S_B_User, E_S_IID, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_B_IID).
rcvd(E_S_B_Actor, E_S_B_SPServer, E_S_B_Request, Ch_SPS2B).
state_Browser(E_S_B_Actor, E_S_B_IID, 3, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_B_IID).
sent(E_S_B_Actor, E_S_B_Actor, E_S_B_IdPServer, E_S_B_Request, E_S_B_Ch_B2IdPS).
state_Browser(E_S_B_Actor, E_S_B_IID, 5, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=Browser; iid=E_S_B_IID; line=91; sender=E_S_B_IdPServer; receiver=E_S_B_Actor; payload=E_S_B_IdPServer; channel=Ch_IdPS2B; fact=rcvd(E_S_B_Actor, E_S_B_IdPServer, E_S_B_IdPServer, Ch_IdPS2B); direction=receive)
% @communication(entity=Browser; iid=E_S_B_IID; line=92; sender=E_S_B_Actor; receiver=E_S_B_User; payload=E_S_B_IdPServer; channel=E_S_B_Ch_B2U; fact=sent(E_S_B_Actor, E_S_B_Actor, E_S_B_User, E_S_B_IdPServer, E_S_B_Ch_B2U); direction=send)
% @step_label(entity=Browser; iid=E_S_B_IID; line=92; variable=SL; term=7)
step step_010_Browser__line_91(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_B_Actor, E_S_B_Ch_B2IdPS, E_S_B_Ch_B2U, E_S_B_IID, E_S_B_IdPCookie, E_S_B_IdPServer, E_S_B_Request, E_S_B_SPServer, E_S_B_User, E_S_IID, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_B_IID).
rcvd(E_S_B_Actor, E_S_B_IdPServer, E_S_B_IdPServer, Ch_IdPS2B).
state_Browser(E_S_B_Actor, E_S_B_IID, 5, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_B_IID).
sent(E_S_B_Actor, E_S_B_Actor, E_S_B_User, E_S_B_IdPServer, E_S_B_Ch_B2U).
state_Browser(E_S_B_Actor, E_S_B_IID, 7, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=Browser; iid=E_S_B_IID; line=95; sender=E_S_B_User; receiver=E_S_B_Actor; payload=E_S_B_User; channel=Ch_U2B; fact=rcvd(E_S_B_Actor, E_S_B_User, E_S_B_User, Ch_U2B); direction=receive)
% @communication(entity=Browser; iid=E_S_B_IID; line=96; sender=E_S_B_Actor; receiver=E_S_B_IdPServer; payload=pair(E_S_B_User, E_S_B_IdPCookie); channel=E_S_B_Ch_B2IdPS; fact=sent(E_S_B_Actor, E_S_B_Actor, E_S_B_IdPServer, pair(E_S_B_User, E_S_B_IdPCookie), E_S_B_Ch_B2IdPS); direction=send)
% @step_label(entity=Browser; iid=E_S_B_IID; line=96; variable=SL; term=9)
step step_011_Browser__line_95(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_B_Actor, E_S_B_Ch_B2IdPS, E_S_B_Ch_B2U, E_S_B_IID, E_S_B_IdPCookie, E_S_B_IdPServer, E_S_B_Request, E_S_B_SPServer, E_S_B_User, E_S_IID, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_B_IID).
rcvd(E_S_B_Actor, E_S_B_User, E_S_B_User, Ch_U2B).
state_Browser(E_S_B_Actor, E_S_B_IID, 7, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_B_IID).
sent(E_S_B_Actor, E_S_B_Actor, E_S_B_IdPServer, pair(E_S_B_User, E_S_B_IdPCookie), E_S_B_Ch_B2IdPS).
state_Browser(E_S_B_Actor, E_S_B_IID, 9, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=Browser; iid=E_S_B_IID; line=99; sender=E_S_B_IdPServer; receiver=E_S_B_Actor; payload=sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))); channel=Ch_IdPS2B; fact=rcvd(E_S_B_Actor, E_S_B_IdPServer, sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))), Ch_IdPS2B); direction=receive)
% @communication(entity=Browser; iid=E_S_B_IID; line=100; sender=E_S_B_Actor; receiver=E_S_B_SPServer; payload=sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))); channel=Ch_B2SPS; fact=sent(E_S_B_Actor, E_S_B_Actor, E_S_B_SPServer, sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))), Ch_B2SPS); direction=send)
% @step_label(entity=Browser; iid=E_S_B_IID; line=100; variable=SL; term=11)
step step_012_Browser__line_99(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_B_Actor, E_S_B_Ch_B2IdPS, E_S_B_Ch_B2U, E_S_B_IID, E_S_B_IdPCookie, E_S_B_IdPServer, E_S_B_Request, E_S_B_SPServer, E_S_B_User, E_S_IID, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_B_IID).
rcvd(E_S_B_Actor, E_S_B_IdPServer, sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))), Ch_IdPS2B).
state_Browser(E_S_B_Actor, E_S_B_IID, 9, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_B_IID).
sent(E_S_B_Actor, E_S_B_Actor, E_S_B_SPServer, sign(inv(pk(E_S_B_IdPServer)), pair(E_S_B_IdPServer, pair(E_S_B_User, E_S_B_SPServer))), Ch_B2SPS).
state_Browser(E_S_B_Actor, E_S_B_IID, 11, E_S_B_User, E_S_B_IdPServer, E_S_B_SPServer, E_S_B_Ch_B2U, E_S_B_Ch_B2IdPS, E_S_B_IdPCookie, E_S_B_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=SPServer; iid=E_S_SPS_IID; line=118; sender=E_S_SPS_Browser; receiver=E_S_SPS_Actor; payload=E_S_SPS_Request; channel=E_S_SPS_Ch_B2SPS; fact=rcvd(E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Request, E_S_SPS_Ch_B2SPS); direction=receive)
% @communication(entity=SPServer; iid=E_S_SPS_IID; line=119; sender=E_S_SPS_Actor; receiver=E_S_SPS_Browser; payload=E_S_SPS_Request; channel=E_S_SPS_Ch_SPS2B; fact=sent(E_S_SPS_Actor, E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Request, E_S_SPS_Ch_SPS2B); direction=send)
% @step_label(entity=SPServer; iid=E_S_SPS_IID; line=119; variable=SL; term=3)
step step_013_SPServer__line_118(E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_IID, E_S_SPS_IdPServer, E_S_SPS_Request, E_S_SPS_User) :=
not(dishonest(E_S_SPS_Actor)).
rcvd(E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Request, E_S_SPS_Ch_B2SPS).
state_SPServer(E_S_SPS_Actor, E_S_SPS_IID, 1, E_S_SPS_Browser, E_S_SPS_IdPServer, E_S_SPS_User, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_Request)
=>
sent(E_S_SPS_Actor, E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Request, E_S_SPS_Ch_SPS2B).
state_SPServer(E_S_SPS_Actor, E_S_SPS_IID, 3, E_S_SPS_Browser, E_S_SPS_IdPServer, E_S_SPS_User, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_Request)
% @communication_guard(entity=SPServer; iid=E_S_SPS_IID; line=122; sender=E_S_SPS_Browser; receiver=E_S_SPS_Actor; payload=sign(inv(pk(E_S_SPS_IdPServer)), pair(E_S_SPS_IdPServer, pair(E_S_SPS_User, E_S_SPS_Actor))); channel=E_S_SPS_Ch_B2SPS; fact=rcvd(E_S_SPS_Actor, E_S_SPS_Browser, sign(inv(pk(E_S_SPS_IdPServer)), pair(E_S_SPS_IdPServer, pair(E_S_SPS_User, E_S_SPS_Actor))), E_S_SPS_Ch_B2SPS); direction=receive)
% @assignment(entity=SPServer; iid=E_S_SPS_IID; line=123; variable=Request; term=E_S_SPS_Request)
% @introduce(entity=SPServer; iid=E_S_SPS_IID; line=123; fact=request(E_S_SPS_Actor, E_S_SPS_User, auth_User_authn_to_SP, E_S_SPS_Request, E_S_SPS_IID))
% @introduce(entity=SPServer; iid=E_S_SPS_IID; line=123; fact=request(E_S_SPS_Actor, E_S_SPS_User, fresh_User_authn_to_SP, E_S_SPS_Request, E_S_SPS_IID))
% @step_label(entity=SPServer; iid=E_S_SPS_IID; line=123; variable=SL; term=5)
step step_014_SPServer__line_122(E_S_SPS_Actor, E_S_SPS_Browser, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_IID, E_S_SPS_IdPServer, E_S_SPS_Request, E_S_SPS_User) :=
rcvd(E_S_SPS_Actor, E_S_SPS_Browser, sign(inv(pk(E_S_SPS_IdPServer)), pair(E_S_SPS_IdPServer, pair(E_S_SPS_User, E_S_SPS_Actor))), E_S_SPS_Ch_B2SPS).
state_SPServer(E_S_SPS_Actor, E_S_SPS_IID, 3, E_S_SPS_Browser, E_S_SPS_IdPServer, E_S_SPS_User, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_Request)
=>
request(E_S_SPS_Actor, E_S_SPS_User, auth_User_authn_to_SP, E_S_SPS_Request, E_S_SPS_IID).
request(E_S_SPS_Actor, E_S_SPS_User, fresh_User_authn_to_SP, E_S_SPS_Request, E_S_SPS_IID).
state_SPServer(E_S_SPS_Actor, E_S_SPS_IID, 5, E_S_SPS_Browser, E_S_SPS_IdPServer, E_S_SPS_User, E_S_SPS_Ch_B2SPS, E_S_SPS_Ch_SPS2B, E_S_SPS_Request)
% @communication_guard(entity=IdPServer; iid=E_S_IPS_IID; line=140; sender=E_S_IPS_Browser; receiver=E_S_IPS_Actor; payload=E_S_IPS_Request_1; channel=E_S_IPS_Ch_B2IdPS; fact=rcvd(E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Request_1, E_S_IPS_Ch_B2IdPS); direction=receive)
% @match(entity=IdPServer; iid=E_S_IPS_IID; line=140; variable=Request; term=E_S_IPS_Request_1)
% @communication(entity=IdPServer; iid=E_S_IPS_IID; line=141; sender=E_S_IPS_Actor; receiver=E_S_IPS_Browser; payload=E_S_IPS_Actor; channel=Ch_IdPS2B; fact=sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Actor, Ch_IdPS2B); direction=send)
% @step_label(entity=IdPServer; iid=E_S_IPS_IID; line=141; variable=SL; term=3)
step step_015_IdPServer__line_140(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_IID, E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_EIC, E_S_IPS_EICApp, E_S_IPS_FCMServer, E_S_IPS_IID, E_S_IPS_IdPCookie, E_S_IPS_Request, E_S_IPS_Request_1, E_S_IPS_SPServer, E_S_IPS_User, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, OpId, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_IPS_IID).
not(dishonest(E_S_IPS_Actor)).
rcvd(E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Request_1, E_S_IPS_Ch_B2IdPS).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 1, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_IPS_IID).
sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Actor, Ch_IdPS2B).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 3, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request_1).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=IdPServer; iid=E_S_IPS_IID; line=144; sender=E_S_IPS_Browser; receiver=E_S_IPS_Actor; payload=pair(E_S_IPS_User, E_S_IPS_IdPCookie_1); channel=E_S_IPS_Ch_B2IdPS; fact=rcvd(E_S_IPS_Actor, E_S_IPS_Browser, pair(E_S_IPS_User, E_S_IPS_IdPCookie_1), E_S_IPS_Ch_B2IdPS); direction=receive)
% @match(entity=IdPServer; iid=E_S_IPS_IID; line=144; variable=IdPCookie; term=E_S_IPS_IdPCookie_1)
% @guard(entity=IdPServer; iid=E_S_IPS_IID; line=144; test=contains(pair(E_S_IPS_User, E_S_IPS_IdPCookie_1), enrollmentDB(E_S_IPS_Actor)))
% @match(entity=IdPServer; iid=E_S_IPS_IID; line=144; variable=IdPCookie; term=E_S_IPS_IdPCookie_1)
% @fresh(entity=IdPServer; iid=E_S_IPS_IID; line=146; variable=OpId; term=OpId_1)
% @communication(entity=IdPServer; iid=E_S_IPS_IID; line=147; sender=E_S_IPS_Actor; receiver=E_S_IPS_FCMServer; payload=pair(OpId_1, E_S_IPS_Request); channel=E_S_IPS_Ch_IdPS2FCMSrv; fact=sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_FCMServer, pair(OpId_1, E_S_IPS_Request), E_S_IPS_Ch_IdPS2FCMSrv); direction=send)
% @step_label(entity=IdPServer; iid=E_S_IPS_IID; line=147; variable=SL; term=6)
step step_016_IdPServer__line_144(E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_EIC, E_S_IPS_EICApp, E_S_IPS_FCMServer, E_S_IPS_IID, E_S_IPS_IdPCookie, E_S_IPS_IdPCookie_1, E_S_IPS_Request, E_S_IPS_SPServer, E_S_IPS_User, OpId, OpId_1) :=
contains(pair(E_S_IPS_User, E_S_IPS_IdPCookie_1), enrollmentDB(E_S_IPS_Actor)).
rcvd(E_S_IPS_Actor, E_S_IPS_Browser, pair(E_S_IPS_User, E_S_IPS_IdPCookie_1), E_S_IPS_Ch_B2IdPS).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 3, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request)
=[exists OpId_1]=>
contains(pair(E_S_IPS_User, E_S_IPS_IdPCookie_1), enrollmentDB(E_S_IPS_Actor)).
sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_FCMServer, pair(OpId_1, E_S_IPS_Request), E_S_IPS_Ch_IdPS2FCMSrv).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 6, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie_1, OpId_1, E_S_IPS_Request)
% @communication_guard(entity=IdPServer; iid=E_S_IPS_IID; line=150; sender=E_S_IPS_EICApp; receiver=E_S_IPS_Actor; payload=OpId; channel=E_S_IPS_Ch_EICApp2IdPS; fact=rcvd(E_S_IPS_Actor, E_S_IPS_EICApp, OpId, E_S_IPS_Ch_EICApp2IdPS); direction=receive)
% @communication(entity=IdPServer; iid=E_S_IPS_IID; line=151; sender=E_S_IPS_Actor; receiver=E_S_IPS_EICApp; payload=pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)); channel=E_S_IPS_Ch_IdPS2EICApp; fact=sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_EICApp, pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)), E_S_IPS_Ch_IdPS2EICApp); direction=send)
% @step_label(entity=IdPServer; iid=E_S_IPS_IID; line=151; variable=SL; term=8)
step step_017_IdPServer__line_150(E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_EIC, E_S_IPS_EICApp, E_S_IPS_FCMServer, E_S_IPS_IID, E_S_IPS_IdPCookie, E_S_IPS_Request, E_S_IPS_SPServer, E_S_IPS_User, OpId) :=
rcvd(E_S_IPS_Actor, E_S_IPS_EICApp, OpId, E_S_IPS_Ch_EICApp2IdPS).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 6, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request)
=>
sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_EICApp, pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)), E_S_IPS_Ch_IdPS2EICApp).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 8, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request)
% @communication_guard(entity=IdPServer; iid=E_S_IPS_IID; line=154; sender=E_S_IPS_EICApp; receiver=E_S_IPS_Actor; payload=pair(OpId, sign(inv(pk(E_S_IPS_EIC)), pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)))); channel=E_S_IPS_Ch_EICApp2IdPS; fact=rcvd(E_S_IPS_Actor, E_S_IPS_EICApp, pair(OpId, sign(inv(pk(E_S_IPS_EIC)), pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)))), E_S_IPS_Ch_EICApp2IdPS); direction=receive)
% @communication(entity=IdPServer; iid=E_S_IPS_IID; line=155; sender=E_S_IPS_Actor; receiver=E_S_IPS_Browser; payload=sign(inv(pk(E_S_IPS_Actor)), pair(E_S_IPS_Actor, pair(E_S_IPS_User, E_S_IPS_SPServer))); channel=Ch_IdPS2B; fact=sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_Browser, sign(inv(pk(E_S_IPS_Actor)), pair(E_S_IPS_Actor, pair(E_S_IPS_User, E_S_IPS_SPServer))), Ch_IdPS2B); direction=send)
% @step_label(entity=IdPServer; iid=E_S_IPS_IID; line=155; variable=SL; term=10)
step step_018_IdPServer__line_154(Browser, Ch_B2IdPS, Ch_B2SPS, Ch_B2U, Ch_EIC2EICApp, Ch_EICApp2EIC, Ch_EICApp2IdPS, Ch_EICApp2U, Ch_FCMSrv2FCMSvc, Ch_FCMSrv2IdPS, Ch_FCMSvc2EICApp, Ch_FCMSvc2FCMSrv, Ch_IdPS2B, Ch_IdPS2EICApp, Ch_IdPS2FCMSrv, Ch_SPS2B, Ch_U2B, Ch_U2EIC, Ch_U2EICApp, EIC, EICApp, E_S_Actor, E_S_IID, E_S_IPS_Actor, E_S_IPS_Browser, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_EIC, E_S_IPS_EICApp, E_S_IPS_FCMServer, E_S_IPS_IID, E_S_IPS_IdPCookie, E_S_IPS_Request, E_S_IPS_SPServer, E_S_IPS_User, E_S_SL, FCMServer, FCMService, IdPCookie, IdPServer, OpId, PIN, Request, SPServer, User) :=
child(E_S_IID, E_S_IPS_IID).
rcvd(E_S_IPS_Actor, E_S_IPS_EICApp, pair(OpId, sign(inv(pk(E_S_IPS_EIC)), pair(OpId, pair(E_S_IPS_Actor, E_S_IPS_SPServer)))), E_S_IPS_Ch_EICApp2IdPS).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 8, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
=>
child(E_S_IID, E_S_IPS_IID).
sent(E_S_IPS_Actor, E_S_IPS_Actor, E_S_IPS_Browser, sign(inv(pk(E_S_IPS_Actor)), pair(E_S_IPS_Actor, pair(E_S_IPS_User, E_S_IPS_SPServer))), Ch_IdPS2B).
state_IdPServer(E_S_IPS_Actor, E_S_IPS_IID, 10, E_S_IPS_FCMServer, E_S_IPS_EICApp, E_S_IPS_User, E_S_IPS_SPServer, E_S_IPS_Browser, E_S_IPS_EIC, E_S_IPS_Ch_B2IdPS, E_S_IPS_Ch_IdPS2FCMSrv, E_S_IPS_Ch_EICApp2IdPS, E_S_IPS_Ch_IdPS2EICApp, E_S_IPS_IdPCookie, OpId, E_S_IPS_Request).
state_Session(E_S_Actor, E_S_IID, E_S_SL, EIC, FCMService, EICApp, User, Browser, SPServer, IdPServer, FCMServer, Ch_B2IdPS, Ch_IdPS2B, Ch_U2B, Ch_B2U, Ch_IdPS2FCMSrv, Ch_FCMSrv2IdPS, Ch_FCMSrv2FCMSvc, Ch_FCMSvc2FCMSrv, Ch_FCMSvc2EICApp, Ch_U2EICApp, Ch_EICApp2U, Ch_EICApp2IdPS, Ch_IdPS2EICApp, Ch_EICApp2EIC, Ch_EIC2EICApp, Ch_B2SPS, Ch_SPS2B, Ch_U2EIC, IdPCookie, Request, PIN)
% @communication_guard(entity=FCMServer; iid=E_S_FCMS_IID; line=175; sender=E_S_FCMS_IdPServer; receiver=E_S_FCMS_Actor; payload=pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1); channel=E_S_FCMS_Ch_IdPS2FCMSrv; fact=rcvd(E_S_FCMS_Actor, E_S_FCMS_IdPServer, pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1), E_S_FCMS_Ch_IdPS2FCMSrv); direction=receive)
% @match(entity=FCMServer; iid=E_S_FCMS_IID; line=175; variable=OpId; term=E_S_FCMS_OpId_1)
% @match(entity=FCMServer; iid=E_S_FCMS_IID; line=175; variable=Request; term=E_S_FCMS_Request_1)
% @communication(entity=FCMServer; iid=E_S_FCMS_IID; line=176; sender=E_S_FCMS_Actor; receiver=E_S_FCMS_FCMService; payload=pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1); channel=E_S_FCMS_Ch_FCMSrv2FCMSvc; fact=sent(E_S_FCMS_Actor, E_S_FCMS_Actor, E_S_FCMS_FCMService, pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1), E_S_FCMS_Ch_FCMSrv2FCMSvc); direction=send)
% @step_label(entity=FCMServer; iid=E_S_FCMS_IID; line=176; variable=SL; term=3)
step step_019_FCMServer__line_175(E_S_FCMS_Actor, E_S_FCMS_Ch_FCMSrv2FCMSvc, E_S_FCMS_Ch_IdPS2FCMSrv, E_S_FCMS_FCMService, E_S_FCMS_IID, E_S_FCMS_IdPServer, E_S_FCMS_OpId, E_S_FCMS_OpId_1, E_S_FCMS_Request, E_S_FCMS_Request_1) :=
not(dishonest(E_S_FCMS_Actor)).
rcvd(E_S_FCMS_Actor, E_S_FCMS_IdPServer, pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1), E_S_FCMS_Ch_IdPS2FCMSrv).
state_FCMServer(E_S_FCMS_Actor, E_S_FCMS_IID, 1, E_S_FCMS_IdPServer, E_S_FCMS_FCMService, E_S_FCMS_Ch_IdPS2FCMSrv, E_S_FCMS_Ch_FCMSrv2FCMSvc, E_S_FCMS_OpId, E_S_FCMS_Request)
=>
sent(E_S_FCMS_Actor, E_S_FCMS_Actor, E_S_FCMS_FCMService, pair(E_S_FCMS_OpId_1, E_S_FCMS_Request_1), E_S_FCMS_Ch_FCMSrv2FCMSvc).
state_FCMServer(E_S_FCMS_Actor, E_S_FCMS_IID, 3, E_S_FCMS_IdPServer, E_S_FCMS_FCMService, E_S_FCMS_Ch_IdPS2FCMSrv, E_S_FCMS_Ch_FCMSrv2FCMSvc, E_S_FCMS_OpId_1, E_S_FCMS_Request_1)
% @communication_guard(entity=FCMService; iid=E_S_FCMS_IID_; line=190; sender=E_S_FCMS_FCMServer; receiver=E_S_FCMS_Actor_; payload=pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1); channel=E_S_FCMS_Ch_FCMSrv2FCMSvc_; fact=rcvd(E_S_FCMS_Actor_, E_S_FCMS_FCMServer, pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1), E_S_FCMS_Ch_FCMSrv2FCMSvc_); direction=receive)
% @match(entity=FCMService; iid=E_S_FCMS_IID_; line=190; variable=OpId; term=E_S_FCMS_OpId__1)
% @match(entity=FCMService; iid=E_S_FCMS_IID_; line=190; variable=Request; term=E_S_FCMS_Request__1)
% @communication(entity=FCMService; iid=E_S_FCMS_IID_; line=191; sender=E_S_FCMS_Actor_; receiver=E_S_FCMS_EICApp; payload=pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1); channel=E_S_FCMS_Ch_FCMSvc2EICApp; fact=sent(E_S_FCMS_Actor_, E_S_FCMS_Actor_, E_S_FCMS_EICApp, pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1), E_S_FCMS_Ch_FCMSvc2EICApp); direction=send)
% @step_label(entity=FCMService; iid=E_S_FCMS_IID_; line=191; variable=SL; term=3)
step step_020_FCMService__line_190(E_S_FCMS_Actor_, E_S_FCMS_Ch_FCMSrv2FCMSvc_, E_S_FCMS_Ch_FCMSvc2EICApp, E_S_FCMS_EICApp, E_S_FCMS_FCMServer, E_S_FCMS_IID_, E_S_FCMS_OpId_, E_S_FCMS_OpId__1, E_S_FCMS_Request_, E_S_FCMS_Request__1) :=
not(dishonest(E_S_FCMS_Actor_)).
rcvd(E_S_FCMS_Actor_, E_S_FCMS_FCMServer, pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1), E_S_FCMS_Ch_FCMSrv2FCMSvc_).
state_FCMService(E_S_FCMS_Actor_, E_S_FCMS_IID_, 1, E_S_FCMS_FCMServer, E_S_FCMS_EICApp, E_S_FCMS_Ch_FCMSrv2FCMSvc_, E_S_FCMS_Ch_FCMSvc2EICApp, E_S_FCMS_OpId_, E_S_FCMS_Request_)
=>
sent(E_S_FCMS_Actor_, E_S_FCMS_Actor_, E_S_FCMS_EICApp, pair(E_S_FCMS_OpId__1, E_S_FCMS_Request__1), E_S_FCMS_Ch_FCMSvc2EICApp).
state_FCMService(E_S_FCMS_Actor_, E_S_FCMS_IID_, 3, E_S_FCMS_FCMServer, E_S_FCMS_EICApp, E_S_FCMS_Ch_FCMSrv2FCMSvc_, E_S_FCMS_Ch_FCMSvc2EICApp, E_S_FCMS_OpId__1, E_S_FCMS_Request__1)
% @communication_guard(entity=EICApp; iid=E_S_EICA_IID; line=208; sender=E_S_EICA_FCMService; receiver=E_S_EICA_Actor; payload=pair(E_S_EICA_OpId_1, E_S_EICA_Request_1); channel=E_S_EICA_Ch_FCMSvc2EICApp; fact=rcvd(E_S_EICA_Actor, E_S_EICA_FCMService, pair(E_S_EICA_OpId_1, E_S_EICA_Request_1), E_S_EICA_Ch_FCMSvc2EICApp); direction=receive)
% @match(entity=EICApp; iid=E_S_EICA_IID; line=208; variable=OpId; term=E_S_EICA_OpId_1)
% @match(entity=EICApp; iid=E_S_EICA_IID; line=208; variable=Request; term=E_S_EICA_Request_1)
% @communication(entity=EICApp; iid=E_S_EICA_IID; line=209; sender=E_S_EICA_Actor; receiver=E_S_EICA_User; payload=E_S_EICA_Request_1; channel=E_S_EICA_Ch_EICApp2U; fact=sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_Request_1, E_S_EICA_Ch_EICApp2U); direction=send)
% @step_label(entity=EICApp; iid=E_S_EICA_IID; line=209; variable=SL; term=3)
step step_021_EICApp__line_208(E_S_EICA_Actor, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_U2EICApp, E_S_EICA_EIC, E_S_EICA_FCMService, E_S_EICA_IID, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_OpId_1, E_S_EICA_PIN, E_S_EICA_Request, E_S_EICA_Request_1, E_S_EICA_SPServer, E_S_EICA_User) :=
not(dishonest(E_S_EICA_Actor)).
rcvd(E_S_EICA_Actor, E_S_EICA_FCMService, pair(E_S_EICA_OpId_1, E_S_EICA_Request_1), E_S_EICA_Ch_FCMSvc2EICApp).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 1, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
=>
sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_Request_1, E_S_EICA_Ch_EICApp2U).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 3, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId_1, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request_1)
% @communication_guard(entity=EICApp; iid=E_S_EICA_IID; line=212; sender=E_S_EICA_User; receiver=E_S_EICA_Actor; payload=stringOK; channel=E_S_EICA_Ch_U2EICApp; fact=rcvd(E_S_EICA_Actor, E_S_EICA_User, stringOK, E_S_EICA_Ch_U2EICApp); direction=receive)
% @communication(entity=EICApp; iid=E_S_EICA_IID; line=213; sender=E_S_EICA_Actor; receiver=E_S_EICA_IdPServer; payload=E_S_EICA_OpId; channel=E_S_EICA_Ch_EICApp2IdPS; fact=sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_Ch_EICApp2IdPS); direction=send)
% @step_label(entity=EICApp; iid=E_S_EICA_IID; line=213; variable=SL; term=5)
step step_022_EICApp__line_212(E_S_EICA_Actor, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_U2EICApp, E_S_EICA_EIC, E_S_EICA_FCMService, E_S_EICA_IID, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_PIN, E_S_EICA_Request, E_S_EICA_SPServer, E_S_EICA_User) :=
rcvd(E_S_EICA_Actor, E_S_EICA_User, stringOK, E_S_EICA_Ch_U2EICApp).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 3, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
=>
sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_Ch_EICApp2IdPS).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 5, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
% @communication_guard(entity=EICApp; iid=E_S_EICA_IID; line=216; sender=E_S_EICA_IdPServer; receiver=E_S_EICA_Actor; payload=pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer_1)); channel=E_S_EICA_Ch_IdPS2EICApp; fact=rcvd(E_S_EICA_Actor, E_S_EICA_IdPServer, pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer_1)), E_S_EICA_Ch_IdPS2EICApp); direction=receive)
% @match(entity=EICApp; iid=E_S_EICA_IID; line=216; variable=SPServer; term=E_S_EICA_SPServer_1)
% @communication(entity=EICApp; iid=E_S_EICA_IID; line=217; sender=E_S_EICA_Actor; receiver=E_S_EICA_User; payload=E_S_EICA_Actor; channel=E_S_EICA_Ch_EICApp2U; fact=sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_Actor, E_S_EICA_Ch_EICApp2U); direction=send)
% @step_label(entity=EICApp; iid=E_S_EICA_IID; line=217; variable=SL; term=7)
step step_023_EICApp__line_216(E_S_EICA_Actor, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_U2EICApp, E_S_EICA_EIC, E_S_EICA_FCMService, E_S_EICA_IID, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_PIN, E_S_EICA_Request, E_S_EICA_SPServer, E_S_EICA_SPServer_1, E_S_EICA_User) :=
rcvd(E_S_EICA_Actor, E_S_EICA_IdPServer, pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer_1)), E_S_EICA_Ch_IdPS2EICApp).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 5, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
=>
sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_Actor, E_S_EICA_Ch_EICApp2U).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 7, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer_1, E_S_EICA_PIN, E_S_EICA_Request)
% @communication_guard(entity=EICApp; iid=E_S_EICA_IID; line=220; sender=E_S_EICA_User; receiver=E_S_EICA_Actor; payload=E_S_EICA_PIN_1; channel=E_S_EICA_Ch_U2EICApp; fact=rcvd(E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_PIN_1, E_S_EICA_Ch_U2EICApp); direction=receive)
% @match(entity=EICApp; iid=E_S_EICA_IID; line=220; variable=PIN; term=E_S_EICA_PIN_1)
% @communication(entity=EICApp; iid=E_S_EICA_IID; line=221; sender=E_S_EICA_Actor; receiver=E_S_EICA_EIC; payload=pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, pair(E_S_EICA_SPServer, E_S_EICA_PIN_1))); channel=E_S_EICA_Ch_EICApp2EIC; fact=sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_EIC, pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, pair(E_S_EICA_SPServer, E_S_EICA_PIN_1))), E_S_EICA_Ch_EICApp2EIC); direction=send)
% @step_label(entity=EICApp; iid=E_S_EICA_IID; line=221; variable=SL; term=9)
step step_024_EICApp__line_220(E_S_EICA_Actor, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_U2EICApp, E_S_EICA_EIC, E_S_EICA_FCMService, E_S_EICA_IID, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_PIN, E_S_EICA_PIN_1, E_S_EICA_Request, E_S_EICA_SPServer, E_S_EICA_User) :=
rcvd(E_S_EICA_Actor, E_S_EICA_User, E_S_EICA_PIN_1, E_S_EICA_Ch_U2EICApp).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 7, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
=>
sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_EIC, pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, pair(E_S_EICA_SPServer, E_S_EICA_PIN_1))), E_S_EICA_Ch_EICApp2EIC).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 9, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN_1, E_S_EICA_Request)
% @communication_guard(entity=EICApp; iid=E_S_EICA_IID; line=224; sender=E_S_EICA_EIC; receiver=E_S_EICA_Actor; payload=sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer))); channel=E_S_EICA_Ch_EIC2EICApp; fact=rcvd(E_S_EICA_Actor, E_S_EICA_EIC, sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer))), E_S_EICA_Ch_EIC2EICApp); direction=receive)
% @communication(entity=EICApp; iid=E_S_EICA_IID; line=225; sender=E_S_EICA_Actor; receiver=E_S_EICA_IdPServer; payload=pair(E_S_EICA_OpId, sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer)))); channel=E_S_EICA_Ch_EICApp2IdPS; fact=sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_IdPServer, pair(E_S_EICA_OpId, sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer)))), E_S_EICA_Ch_EICApp2IdPS); direction=send)
% @step_label(entity=EICApp; iid=E_S_EICA_IID; line=225; variable=SL; term=11)
step step_025_EICApp__line_224(E_S_EICA_Actor, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_U2EICApp, E_S_EICA_EIC, E_S_EICA_FCMService, E_S_EICA_IID, E_S_EICA_IdPServer, E_S_EICA_OpId, E_S_EICA_PIN, E_S_EICA_Request, E_S_EICA_SPServer, E_S_EICA_User) :=
rcvd(E_S_EICA_Actor, E_S_EICA_EIC, sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer))), E_S_EICA_Ch_EIC2EICApp).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 9, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
=>
sent(E_S_EICA_Actor, E_S_EICA_Actor, E_S_EICA_IdPServer, pair(E_S_EICA_OpId, sign(inv(pk(E_S_EICA_EIC)), pair(E_S_EICA_OpId, pair(E_S_EICA_IdPServer, E_S_EICA_SPServer)))), E_S_EICA_Ch_EICApp2IdPS).
state_EICApp(E_S_EICA_Actor, E_S_EICA_IID, 11, E_S_EICA_FCMService, E_S_EICA_User, E_S_EICA_IdPServer, E_S_EICA_EIC, E_S_EICA_Ch_FCMSvc2EICApp, E_S_EICA_Ch_EICApp2U, E_S_EICA_Ch_U2EICApp, E_S_EICA_Ch_EICApp2IdPS, E_S_EICA_Ch_IdPS2EICApp, E_S_EICA_Ch_EICApp2EIC, E_S_EICA_Ch_EIC2EICApp, E_S_EICA_OpId, E_S_EICA_SPServer, E_S_EICA_PIN, E_S_EICA_Request)
% @communication_guard(entity=EIC; iid=E_S_EIC_IID; line=247; sender=E_S_EIC_EICApp; receiver=E_S_EIC_Actor; payload=pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, pair(E_S_EIC_SPServer_1, E_S_EIC_PIN))); channel=E_S_EIC_Ch_EICApp2EIC; fact=rcvd(E_S_EIC_Actor, E_S_EIC_EICApp, pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, pair(E_S_EIC_SPServer_1, E_S_EIC_PIN))), E_S_EIC_Ch_EICApp2EIC); direction=receive)
% @match(entity=EIC; iid=E_S_EIC_IID; line=247; variable=OpId; term=E_S_EIC_OpId_1)
% @match(entity=EIC; iid=E_S_EIC_IID; line=247; variable=SPServer; term=E_S_EIC_SPServer_1)
% @communication_guard(entity=EIC; iid=E_S_EIC_IID; line=247; sender=E_S_EIC_User; receiver=E_S_EIC_Actor; payload=useEIC; channel=E_S_EIC_Ch_U2EIC; fact=rcvd(E_S_EIC_Actor, E_S_EIC_User, useEIC, E_S_EIC_Ch_U2EIC); direction=receive)
% @communication(entity=EIC; iid=E_S_EIC_IID; line=249; sender=E_S_EIC_Actor; receiver=E_S_EIC_EICApp; payload=sign(inv(pk(E_S_EIC_Actor)), pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, E_S_EIC_SPServer_1))); channel=E_S_EIC_Ch_EIC2EICApp; fact=sent(E_S_EIC_Actor, E_S_EIC_Actor, E_S_EIC_EICApp, sign(inv(pk(E_S_EIC_Actor)), pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, E_S_EIC_SPServer_1))), E_S_EIC_Ch_EIC2EICApp); direction=send)
% @step_label(entity=EIC; iid=E_S_EIC_IID; line=249; variable=SL; term=3)
step step_026_EIC__line_247(E_S_EIC_Actor, E_S_EIC_Ch_EIC2EICApp, E_S_EIC_Ch_EICApp2EIC, E_S_EIC_Ch_U2EIC, E_S_EIC_EICApp, E_S_EIC_IID, E_S_EIC_IdPServer, E_S_EIC_OpId, E_S_EIC_OpId_1, E_S_EIC_PIN, E_S_EIC_SPServer, E_S_EIC_SPServer_1, E_S_EIC_User) :=
not(dishonest(E_S_EIC_Actor)).
rcvd(E_S_EIC_Actor, E_S_EIC_EICApp, pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, pair(E_S_EIC_SPServer_1, E_S_EIC_PIN))), E_S_EIC_Ch_EICApp2EIC).
rcvd(E_S_EIC_Actor, E_S_EIC_User, useEIC, E_S_EIC_Ch_U2EIC).
state_EIC(E_S_EIC_Actor, E_S_EIC_IID, 1, E_S_EIC_EICApp, E_S_EIC_IdPServer, E_S_EIC_User, E_S_EIC_Ch_EICApp2EIC, E_S_EIC_Ch_EIC2EICApp, E_S_EIC_Ch_U2EIC, E_S_EIC_PIN, E_S_EIC_OpId, E_S_EIC_SPServer)
=>
sent(E_S_EIC_Actor, E_S_EIC_Actor, E_S_EIC_EICApp, sign(inv(pk(E_S_EIC_Actor)), pair(E_S_EIC_OpId_1, pair(E_S_EIC_IdPServer, E_S_EIC_SPServer_1))), E_S_EIC_Ch_EIC2EICApp).
state_EIC(E_S_EIC_Actor, E_S_EIC_IID, 3, E_S_EIC_EICApp, E_S_EIC_IdPServer, E_S_EIC_User, E_S_EIC_Ch_EICApp2EIC, E_S_EIC_Ch_EIC2EICApp, E_S_EIC_Ch_U2EIC, E_S_EIC_PIN, E_S_EIC_OpId_1, E_S_EIC_SPServer_1)
section goals:
% @goal(name=auth_User_authn_to_SP; line=317; AM=AM; AR=AR; AW=AW; IID=E_aUatSP_IID)
attack_state auth_User_authn_to_SP(AM, AR, AW, E_aUatSP_IID) :=
not(dishonest(AW)).
not(witness(AW, AR, auth_User_authn_to_SP, AM)).
request(AR, AW, auth_User_authn_to_SP, AM, E_aUatSP_IID)
% @goal(name=fresh_User_authn_to_SP; line=317; FM=FM; FR=FR; FW=FW; IID1=IID1; IID2=IID2)
attack_state fresh_User_authn_to_SP(FM, FR, FW, IID1, IID2) :=
not(dishonest(FW)).
request(FR, FW, fresh_User_authn_to_SP, FM, IID1).
request(FR, FW, fresh_User_authn_to_SP, FM, IID2) &
not(equal(IID1, IID2))