Galois Tech Talk: Equivalence Checking Public-Key Crypto Algorithms

Skip to first unread message

Don Stewart

Jul 17, 2008, 2:48:04 PM7/17/08
Next week's Galois Tech Talk:


Title:      Equivalence Checking Public-Key Crypto Algorithms

Speaker:    John Matthews
Date:       Tuesday, July 22nd, 10.30am

Location:   Galois, Inc.
            421 SW 6th Ave. Suite 300
            (3rd floor of the Commonwealth Building)
            Portland, Oregon


   The Cryptol team has had a lot of success in automatically verifying the
   functional correctness of hardware implementations of symmetric key
   algorithms such as DES and AES by using SAT-based and Satisfiability
   Modulo Theories (SMT)-based equivalence checking.

   We've recently started trying to equivalence check public key crypto
   algorithm primitives such as modular multiplication, but here the story is
   much worse: public key primitives operate on word sizes that are hundreds
   or thousands of bits long, yet the Cryptol equivalence checker and every
   SMT solver we've tried times out on just 20-bit words.

   In this talk I'll lay out the problems we've hit, how we've had some
   initial success using the Isabelle theorem prover, and how our lives would
   be much easier if SMT solvers directly supported user-given rewrite rules.
   This is a repeat of a talk I gave at the Bit-Precise Reasoning workshop
   earlier this week at Princeton

About the Galois Tech Talks.

    Galois ( has been holding weekly technical
    seminars for several years on topics from functional programming,
    formal methods, compiler and language design, to cryptography, and
    operating system construction, with talks by many figures from the
    programming language and formal methods communities.

    The talks are open and free. If you're planning to attend, dropping
    a note to <> is appreciated, but not required.
    If you're interested in giving a talk, Don's always looking for new

Reply all
Reply to author
0 new messages