Works will be to consolidate the research prototypes developed during the project, including the SAT_Equiv tool to verify the cryptographic protocols from the established theorem. The mission will also consist in developing tools for visualizing results. These graphic components will be used to graphically replay a detected attack to better understand how it works.
Our suggestion will be to extend Jupyter OCaml Kernel if necessary and produce visualization plugin adapted.
More information about satequiv here : https://projects.lsv.ens-cachan.fr/satequiv/
And a french description in PDF associated : https://filesender.renater.fr/?s=download&token=00584a42-352f-897b-5519-58a659b607e6