"Eesti Teadusfondi uurimistoetus" projekt ETF6944
ETF6944 "Krüptograafiliste protokollide turvatõestused (1.01.2007−31.12.2009)", Peeter Laud, Cybernetica AS.
ETF6944
Krüptograafiliste protokollide turvatõestused
Security proofs for cryptographic protocols
1.01.2007
31.12.2009
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP175 Informaatika, süsteemiteooria1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
AsutusRollPeriood
Cybernetica ASkoordinaator01.01.2007−31.12.2009
PerioodSumma
01.01.2007−31.12.2007175 800,00 EEK (11 235,67 EUR)
01.01.2008−31.12.2008175 800,00 EEK (11 235,67 EUR)
01.01.2009−31.12.2009168 768,00 EEK (10 786,24 EUR)
33 257,58 EUR

Grandiprojekti eesmärgiks on edasi arendada meetodeid krüptograafiliste protokollide turvatõestuseks ja nende tõestuste automaatseks koostamiseks. Käesoleval ajal on üldjoontes teada, kuidas käib protokollide (automaatne) turvaanalüüs klassikaliste turvaomaduste (konfidentsiaalsus, autentsus) ning klassikaliste kasutatavate krüptoprimitiivide (sümmeetriline ja asümmeetriline krüptimine, signeerimine, juhuarvude genereerimine) jaoks. Seda teadmust on kavas laiendada teistele turvaomadustele ja primitiividele, aga samuti olemasolevate primitiivide teistele, nõrgematele turvadefinitsioonile. Töö käigus on kavas võimalikult paljudele mingi analüüsi korrektsust väitvatele teoreemidele masinkontrollitud tõestused anda. See suurendab kindlust, et automaatselt leitud turvatõestused ikka korrektsed on.
The goal of the grant project is to continue the development of methods for proving cryptographic protocols secure and for the automatic construction of these proofs. Currently it is more or less known how to automatically analyse protocols for classical security properties (confidentiality, authenticity), if the protocols use classical cryptographic primitives (symmetric and asymmetric encryption, signing, random number generation). We plan to extend this knowledge to other security properties and primitives, but also to other, weaker security definitions of existing primitives. In the course of the work we attempt to give machine-verified proofs to most of the theorems stating the correctness of some analysis method. This will increase the confidence in the automatically found security proofs of the protocols.