Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 2, bâtiment C

                           Lundi 5 septembre, 10h30

                           -----------------------
                           Jean-Karim Zinzindohoué
                           -----------------------

                                 Inria Paris

                    ======================================
                    Verified, efficient cryptography in F*
                    ======================================

In response to increasing demand for elliptic curve cryptography, new elliptic
curves such as Curve25519 and Curve448 are currently being standardized,
implemented, and deployed in major protocols such as Transport Layer
Security. As with all new cryptographic code, the correctness of these curve
implementations is of concern. We present a principled approach towards the
verification of elliptic curve implementations by writing them in the
dependently-typed programming language F* and proving them functionally
correct against a readable mathematical specification derived from a previous
Coq development.  A key technical innovation in our work is the use of
templates to write and verify arbitrary precision arithmetic once and for all
for a variety of Bignum representations used in different curves. We also show
how to use abstract types to enforce a discipline that mitigates side-channels
at the source level. We present a verified F* library that implements popular
curves such as Curve25519, or NIST-P256, and we show how to extend this
library further with minimal verification effort to other curves as well as to
other cryptographic primitives.