BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
hes
SUMMARY:Cryptanalysis with SAT - a propositional programmi
ng environment - Mateusz Srebrny
DTSTART;TZID=Europe/London:20070814T130000
DTEND;TZID=Europe/London:20070814T140000
UID:TALK7762AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/7762
DESCRIPTION:In this talk\, a polynomial time translation of in
teger factorization and the cryptographic hash fun
ctions MD5 and SHA-1 into propositional formulas w
ill be presented and discussed\, along with some i
nteresting experimental\nresults obtained with the
use of the current best SAT solvers. Those comput
ational problems can also serve as benchmark for v
arious SAT solvers.\n\nPropositional satisfiabilit
y\, SAT\, is one of the best known NP-complete pro
blems. There is no feasible algorithm known for te
sting satisfiability of the propositional formulas
in general. Nevertheless\, there are algorithms (
implemented by so-called SAT solvers\, or SAT chec
kers) that turn out to be feasible and very effici
ent on many instances of propositional formulas.\n
\nOn the other hand\, no one knows any polynomial
run-time solving algorithm for the problem of inte
ger factorization. The famous and challenging cryp
tosystem RSA was built on the problem in 1977 and
has been widely applied since then.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
m SS03
CONTACT:Thomas Tuerk
END:VEVENT
END:VCALENDAR