BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//SECURITY & APPLIED LOGIC - ECPv6.15.9//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://sal.cs.unibuc.ro
X-WR-CALDESC:Events for SECURITY & APPLIED LOGIC
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20180101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20190207T083000
DTEND;TZID=UTC:20190207T100000
DTSTAMP:20260404T162006
CREATED:20190205T043140Z
LAST-MODIFIED:20190205T055045Z
UID:287-1549528200-1549533600@sal.cs.unibuc.ro
SUMMARY:Verification of strategic properties for the Prêt-À-Voter protocol using Tamarin  (joint work with Wojtek Jamroga and Damian Kurpiewski)
DESCRIPTION:Speaker:   Catalin Dima (Université Paris-Est Créteil) \n\nAbstract: \nWe 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. \n  \n 
URL:https://sal.cs.unibuc.ro/event/verification-of-strategic-properties-for-the-pret-a-voter-protocol-using-tamarin-joint-work-with-wojtek-jamroga-and-damian-kurpiewski/
LOCATION:Facultatea de Matematica si Informatica\, sala Google
CATEGORIES:Security Seminar
END:VEVENT
END:VCALENDAR