DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

missing action in attack trace #61

Closed steve-kremer closed 4 years ago

steve-kremer commented 4 years ago

In

Examples/trace_equivalence/Private_authentication/PrivateAuthentication-1session-attack.dps

the attack trace (as displayed by deepsec-ui) is

out(c,ax1);​out(c,ax2);​out(c,ax3);​out(ca,ax4);​in(cb,aenc((#n0,ax1),ax2))

missing the last action out(cb,ax5), necessary to distinguish the processes.

Note: only the display seems buggy, the results are all consistent.