Elliptische Kurven bilden heute die Grundlage der bei Amazon & Co. verwendeten Verschlüsselungsverfahren. Eine neue, am 25. April auf dem ArXiv erschienene Arbeit von Hales und Rays (Formal Proof of the Group Law for Edwards Elliptic Curves) liefert nun einen computerformalisierten Beweis der dafür grundlegenden Eigenschaften elliptischer Kurven.
Elliptische Kurven sind für Kryptographie geeignet, weil sie eine (abelsche) Gruppe bilden. Notorisch schwierig ist dabei der Beweis des Assoziativitätsgesetzes, für das alle bekannten Beweise sehr rechenaufwändig sind. Einen Beweis mittels Computeralgebra gab erstmals Friedl (An elementary proof of the group law for elliptic curves), was 1998 noch mehrere Stunden Rechenzeit auf einem Computer benötigte. Eine Realisierung in Coq durch Thery benötigte 2007 noch 80 Sekunden.
Der neue Ansatz beruht nun auf einem vier Jahre alten Skript von Hales (The Group Law for Edwards Curves). Die grundlegende Idee ist, elliptische Kurven nicht in der üblichen Weierstraß-Form y2=x3+ax+b, sondern in der Edwards-Form, eine gewisse Deformation der Kreisgleichung, in der die Additionsformel dann sehr symmetrisch aussieht, zu verwenden. Im damaligen Skript hatte er das bereits benutzt, um einen kurzen Beweis des Assoziativitätsgesetzes zu geben und in der neuen Arbeit wird das nun also auch in HOL computerformalisiert, ebenso wie die anderen grundlegenden Eigenschaften elliptischer Kurven.
Kommentare (11)