Speaker:  Catalin Dima (Université Paris-Est Créteil)

Abstract:

We report on the verification of anonymity and coercion-freeness properties of the Prêt-À-Voter electronic voting protocol using the Tamarin tool for symbolic verification of security properties. Our approach is to generate many models corresponding with each choice of attacker actions (i.e. attacker strategies) and check, on each model, a “trace equivalence” lemma modeling the fact that the attacker does not distinguish between a trace in which the coerced voter has obeyed the orders, from a trace in which the voter has ignored the coercion. This seems to be the only approach available in Tamarin for modeling epistemic knowledge, a notion necessary for encoding anonymity. The results are far from encouraging since many false negatives or positives are obtained, necessitating model adaptations which cannot be done automatically, and when correct results are obtained the running times are prohibitive. Our conclusions point the need for theory and tool improvement in which equational and rewriting logics be combined with strategy logics.

Speaker: Mihai Stancu

Abstract:

The security trend today is to stop security threats even before they
arrive on the target machine or system.

With that in mind we will explore, what packers are and what they do to
transform original malicious code in into something that is much harder to
confidently mark as a threat.

This talk will be focused on executables in the PE format running on the
Windows platform and during the presentation we will form a basic
understanding of the executable structure, packing technique, and other
anti-dumping and anti-debug techniques work to protect and run the original
payload.