I'd like to include an extremely long line of code. I have tried using lstlisting but it can't handle it. The code overflows through the bottom of the page.
I am using a modified report style. The code appears in appendix in a section. Here is my tex script with the code.
Code: Select all
{\tiny
\begin{lstlisting}[breaklines=true]
Process:
new pkCh1_11;
new pkCh2_12;
new pkCh3_13;
new pkChn_14;
new pkChDC_15;
new pkChCA_16;
new skCh1_17;
new skCh2_18;
new skCh3_19;
new skChn_20;
new skChDC_21;
new skChCA_22;
new ca2_23;
new ca3_24;
(
new sk1_101;
new sk2_102;
new sk3_103;
new skn_104;
new skDC_105;
new skCA_106;
(
{145}let pk1_114 = pk(sk1_101) in
{146}!
{147}out(pkCh1_11, pk1_114);
0
) | (
{114}let pk2_107 = pk(sk2_102) in
(
{143}!
{144}out(pkCh2_12, pk2_107);
0
) | (
{115}let au2_108 = au(pk2_107) in
(
{141}!
{142}out(ca2_23, au2_108);
0
) | (
{116}let pk3_109 = pk(sk3_103) in
(
{139}!
{140}out(pkCh3_13, pk3_109);
0
) | (
{117}let au3_110 = au(pk3_109) in
(
{137}!
{138}out(ca3_24, au3_110);
0
) | (
{134}let pkn_113 = pk(skn_104) in
{135}!
{136}out(pkChn_14, pkn_113);
0
) | (
{131}let pkDC_112 = pk(skDC_105) in
{132}!
{133}out(pkChDC_15, pkDC_112);
0
) | (
{128}let pkCA_111 = pk(skCA_106) in
{129}!
{130}out(pkChCA_16, pkCA_111);
0
) | (
{126}!
{127}out(skCh1_17, sk1_101);
0
) | (
{124}!
{125}out(skCh2_18, sk2_102);
0
) | (
{122}!
{123}out(skCh3_19, sk3_103);
0
) | (
{121}out(skChn_20, skn_104);
0
) | (
{120}out(skChDC_21, skDC_105);
0
) | (
{118}!
{119}out(skChCA_22, skCA_106);
0
)
)
)
)
)
) | (
{108}!
{109}in(skChCA_22, skCA_96);
{110}in(cC, m_97);
{111}let (a_98,b_99) = m_97 in
{112}let sb_100 = getkey(b_99) in
{113}out(cC, sign((sb_100,b_99),skCA_96));
0
) | (
{100}!
{101}in(skCh1_17, seck1_91);
{102}in(pkCh2_12, pubk2_92);
{103}in(pkChDC_15, pubkDC_93);
new R0_94;
{104}out(cD, enc(R0_94,pubkDC_93));
new result1_95;
{105}event begin12(pk(seck1_91),pubk2_92,result1_95);
{106}out(c1, enc((pk(seck1_91),sign(result1_95,seck1_91)),pubk2_92));
{107}out(cD, enc(result1_95,pubkDC_93));
0
) | (
{69}!
{70}in(skCh2_18, seck2_71);
{71}in(pkCh1_11, pubk1_72);
{72}in(pkChn_14, pubkn_73);
{73}in(pkChDC_15, pubkDC_74);
{74}in(pkChCA_16, pubkCA_75);
{75}!
{76}in(c1, m1_76);
{77}!
{78}in(cD, t1_77);
{79}let (=pubk1_72,signed1_78) = dec(m1_76,seck2_71) in
{80}let R1_79 = checksign(pubk1_72,signed1_78) in
{81}event end12(pubk1_72,pk(seck2_71),R1_79);
{82}event end1(pubk1_72);
{83}out(c, syenc(sR1,R1_79));
{84}let D1_80 = dec(t1_77,seck2_71) in
{85}if R1_79 = D1_80 then
{86}in(ca2_23, au2_81);
{87}in(ca3_24, au3_82);
{88}out(cC, (au2_81,au3_82));
{89}in(cC, ms_83);
{90}let (pubk3_84,=au3_82) = checksign(pubkCA_75,ms_83) in
new N2_85;
{91}out(c2, enc((N2_85,au2_81),pubk3_84));
{92}in(c2, m_86);
{93}let (=N2_85,rN3_87,=au3_82) = dec(m_86,seck2_71) in
{94}event begin3(N2_85,au2_81,au3_82,pubk3_84,pk(seck2_71),rN3_87);
new result2_88;
new final2_89;
{95}let msg2_90 = (pk(seck2_71),sign(result2_88,seck2_71)) in
{96}out(c2, enc((msg2_90,rN3_87),pubk3_84));
{97}event end2(N2_85,au2_81,au3_82,pubk3_84,pk(seck2_71),rN3_87);
{98}out(c2n, enc((pk(seck2_71),sign(final2_89,seck2_71)),pubkn_73));
{99}out(cD, enc(result2_88,pubkDC_74));
0
) | (
{45}!
{46}in(skCh3_19, seck3_52);
{47}in(pkChn_14, pubkn_53);
{48}in(pkChDC_15, pubkDC_54);
{49}in(pkChCA_16, pubkCA_55);
{50}in(c2, m_56);
{51}let (rN2_57,au2_58) = dec(m_56,seck3_52) in
{52}in(ca3_24, au3_59);
{53}out(cC, (au3_59,au2_58));
{54}in(cC, ms_60);
{55}let (pubk2_61,=au2_58) = checksign(pubkCA_55,ms_60) in
new N3_62;
{56}event begin2(rN2_57,au2_58,au3_59,pk(seck3_52),pubk2_61,N3_62);
{57}out(c2, enc((rN2_57,N3_62,au3_59),pubk2_61));
{58}in(c2, m2_63);
{59}in(cD, t2_64);
{60}let (msg2_65,=N3_62) = dec(m2_63,seck3_52) in
{61}event end3(rN2_57,au2_58,au3_59,pk(seck3_52),pubk2_61,N3_62);
{62}let (=pubk2_61,signed2_66) = msg2_65 in
{63}let R2_67 = checksign(pubk2_61,signed2_66) in
{64}out(c, syenc(sR2,R2_67));
{65}let D2_68 = dec(t2_64,seck3_52) in
{66}if R2_67 = D2_68 then
new result3_69;
new final3_70;
{67}out(c3, enc((pk(seck3_52),sign((result3_69,final3_70),seck3_52)),pubkn_53));
{68}out(cD, enc(result3_69,pubkDC_54));
0
) | (
{22}in(skChn_20, seckn_36);
{23}in(pkCh2_12, pubk2_37);
{24}in(pkCh3_13, pubk3_38);
{25}in(pkChDC_15, pubkDC_39);
{26}!
{27}in(c2n, m2_40);
{28}let (=pubk2_37,signed2_41) = dec(m2_40,seckn_36) in
{29}let F2_42 = checksign(pubk2_37,signed2_41) in
{30}out(c, syenc(sF2,F2_42));
{31}!
{32}in(c3, m3_43);
{33}!
{34}in(cD, t3_44);
{35}let (=pubk3_38,signed3_45) = dec(m3_43,seckn_36) in
{36}let RF3_46 = checksign(pubk3_38,signed3_45) in
{37}out(c, syenc(sRF3,RF3_46));
{38}let (R3_47,F3_48) = RF3_46 in
{39}out(c, syenc(sR3,R3_47));
{40}out(c, syenc(sF3,F3_48));
{41}let D3_49 = dec(t3_44,seckn_36) in
{42}if R3_47 = D3_49 then
new resultn_50;
{43}out(c, (F2_42,F3_48,resultn_50));
new typoflag_51;
{44}out(c, typoflag_51);
0
) | (
{1}in(skChDC_21, seckDC_25);
{2}in(pkCh2_12, pubk2_26);
{3}in(pkCh3_13, pubk3_27);
{4}in(pkChn_14, pubkn_28);
{5}!
{6}in(cD, server0_29);
{7}!
{8}in(cD, server1_30);
{9}let pre1_31 = dec(server1_30,seckDC_25) in
{10}!
{11}out(cD, enc(pre1_31,pubk2_26));
{12}!
{13}in(cD, server2_32);
{14}let pre2_33 = dec(server2_32,seckDC_25) in
{15}!
{16}out(cD, enc(pre2_33,pubk3_27));
{17}!
{18}in(cD, server3_34);
{19}let pre3_35 = dec(server3_34,seckDC_25) in
{20}!
{21}out(cD, enc(pre3_35,pubkn_28));
0
)
-- Query evinj:end2(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin2(u_115,v_116,w_117,x_118,y_119,z_120); evinj:end3(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin3(u_115,v_116,w_117,x_118,y_119,z_120)
Completing...
200 rules inserted. The rule base contains 187 rules. 84 rules in the queue.
400 rules inserted. The rule base contains 336 rules. 86 rules in the queue.
600 rules inserted. The rule base contains 487 rules. 75 rules in the queue.
800 rules inserted. The rule base contains 613 rules. 10 rules in the queue.
1000 rules inserted. The rule base contains 744 rules. 34 rules in the queue.
1200 rules inserted. The rule base contains 872 rules. 9 rules in the queue.
1400 rules inserted. The rule base contains 994 rules. 37 rules in the queue.
1600 rules inserted. The rule base contains 1125 rules. 25 rules in the queue.
1800 rules inserted. The rule base contains 1261 rules. 79 rules in the queue.
2000 rules inserted. The rule base contains 1415 rules. 40 rules in the queue.
2200 rules inserted. The rule base contains 1522 rules. 23 rules in the queue.
Starting query evinj:end2(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin2(u_115,v_116,w_117,x_118,y_119,z_120)
goal reachable: begin:begin3(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = @sid_27117]), m_86 = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = @sid_27117],au(pk(sk3_103[]))),pk(sk2_102[])), ms_83 = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]), au3_82 = au(pk(sk3_103[])), au2_81 = au(pk(sk2_102[])), t1_77 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])), @sid_218 = endsid_27114, m1_76 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])), @sid_216 = @sid_27115, pubkCA_75 = pk(skCA_106[]), pubkDC_74 = pk(skDC_105[]), pubkn_73 = pk(skn_104[]), pubk1_72 = pk(sk1_101[]), seck2_71 = sk2_102[], @sid_210 = @sid_27116, @occ94_274 = @occ_cst() & begin:begin2(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = @sid_27117]), ms_60 = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]), au3_59 = au(pk(sk3_103[])), m_56 = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[]))),pk(sk3_103[])), pubkCA_55 = pk(skCA_106[]), pubkDC_54 = pk(skDC_105[]), pubkn_53 = pk(skn_104[]), seck3_52 = sk3_103[], @sid_327 = @sid_27117, @occ56_351 = @occ_cst() -> end:endsid_27114,end2(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],pk(sk2_102[])),!3 = endsid_27114,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27113],sk1_101[])),pk(sk2_102[])),!2 = @sid_27115,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27116],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = @sid_27117])
RESULT evinj:end2(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin2(u_115,v_116,w_117,x_118,y_119,z_120) is true.
Starting query evinj:end3(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin3(u_115,v_116,w_117,x_118,y_119,z_120)
goal reachable: attacker:t2_27148 & begin:begin3(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153]), m_86 = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153],au(pk(sk3_103[]))),pk(sk2_102[])), ms_83 = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]), au3_82 = au(pk(sk3_103[])), au2_81 = au(pk(sk2_102[])), t1_77 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])), @sid_218 = @sid_27150, m1_76 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])), @sid_216 = @sid_27151, pubkCA_75 = pk(skCA_106[]), pubkDC_74 = pk(skDC_105[]), pubkn_73 = pk(skn_104[]), pubk1_72 = pk(sk1_101[]), seck2_71 = sk2_102[], @sid_210 = @sid_27152, @occ94_274 = @occ_cst() & begin:begin2(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153]), ms_60 = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]), au3_59 = au(pk(sk3_103[])), m_56 = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])), pubkCA_55 = pk(skCA_106[]), pubkDC_54 = pk(skDC_105[]), pubkn_53 = pk(skn_104[]), seck3_52 = sk3_103[], @sid_327 = endsid_27153, @occ56_351 = @occ_cst() & begin:begin2(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153]), t2_64 = t2_27148, m2_63 = enc(((pk(sk2_102[]),sign(result2_88[m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153],au(pk(sk3_103[]))),pk(sk2_102[])),ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],sk2_102[])),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153]),pk(sk3_103[])), ms_60 = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]), au3_59 = au(pk(sk3_103[])), m_56 = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1
= enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])), pubkCA_55 = pk(skCA_106[]), pubkDC_54 = pk(skDC_105[]), pubkn_53 = pk(skn_104[]), seck3_52 = sk3_103[], @sid_327 = endsid_27153, @occ56_351 = @occ_cst() -> end:endsid_27153,end3(N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[])),au(pk(sk3_103[])),pk(sk3_103[]),pk(sk2_102[]),N3_62[ms = sign((pk(sk2_102[]),au(pk(sk2_102[]))),skCA_106[]),au3 = au(pk(sk3_103[])),m = enc((N2_85[ms = sign((pk(sk3_103[]),au(pk(sk3_103[]))),skCA_106[]),au3 = au(pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1 = enc(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],pk(sk2_102[])),!3 = @sid_27150,m1 = enc((pk(sk1_101[]),sign(result1_95[pubkDC = pk(skDC_105[]),pubk2 = pk(sk2_102[]),seck1 = sk1_101[],!1 = @sid_27149],sk1_101[])),pk(sk2_102[])),!2 = @sid_27151,pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),pubk1 = pk(sk1_101[]),seck2 = sk2_102[],!1 = @sid_27152],au(pk(sk2_102[]))),pk(sk3_103[])),pubkCA = pk(skCA_106[]),pubkDC = pk(skDC_105[]),pubkn = pk(skn_104[]),seck3 = sk3_103[],!1 = endsid_27153])
RESULT evinj:end3(u_115,v_116,w_117,x_118,y_119,z_120) ==> evinj:begin3(u_115,v_116,w_117,x_118,y_119,z_120) is true.
\end{lstlisting} }Code: Select all
! Dimension too large.
\lsthk@InitVarsEOL ->\ifdim \lst@currlwidth
>\lst@maxwidth \global \lst@maxw...
l.251 ...04[]),seck3 = sk3_103[],!1 = @sid_27117])
?
! Dimension too large.
<recently read> \lst@currlwidth
l.251 ...04[]),seck3 = sk3_103[],!1 = @sid_27117])
?
[144]
! Dimension too large.
\lsthk@InitVarsEOL ->\ifdim \lst@currlwidth
>\lst@maxwidth \global \lst@maxw...
l.254 ...pk(sk3_103[])),au2 = au(pk(sk2_102[])),t1
? Code: Select all
Overfull \vbox (175.61256pt too high) has occurred while \output is activeThe overfull box (second warning) is the one I'd like to solve.
Any suggestions? Thanks before!
PS. I'm using TeXworks on Windows 7.
