See veebileht kasutab küpsiseid kasutaja sessiooni andmete hoidmiseks. Veebilehe kasutamisega nõustute ETISe kasutustingimustega. Loe rohkem
Olen nõus
"Eesti Teadusfondi uurimistoetus (ETF)" projekt ETF9171
ETF9171 "ProveIt - arvutipõhine krüptograafiliste tõestuste verifitseerija (1.01.2012−31.12.2012)", Dominique Peer Ghislain Dr Unruh, Tartu Ülikool, Matemaatika-informaatikateaduskond.
ETF9171
ProveIt - arvutipõhine krüptograafiliste tõestuste verifitseerija
ProveIt - Computer-Aided Verification of Cryptographic Proofs
1.01.2012
31.12.2012
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus (ETF)
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
PerioodSumma
01.01.2012−31.12.20128 496,00 EUR
8 496,00 EUR

Kaasaegse krüptograafia üheks peamiseks eesmärgiks on anda erinevatele krüptograafilistele skeemidele ja protokollidele ranged turvatõestused, mis põhinevad vaid hästi läbi uuritud turvaeeldustel (näiteks suurte täisarvude tegurdamise arvutuslik keerukus). Ilma selliste tõestusteta on üsna tõenäoline, et protokollides võib olla ootamatuid nõrkusi. Formaalne tõestus tagab selliste rünnete puudumise (tingimusel, et tehtud turvaeeldused kehtivad). Praktikas pole olukord nii lihtne, kuna krüptograafiliste skeemide turvatõestused kipuvad olema suhteliselt keerukad. Käsitsi kirja pandud tõestustes on tihti palju väikseid vigu, lihtsustusi ja läbi vaatamata variante. Halvematel juhtudel on kulunud aastaid enne, kui krüptograafid on suutnud tuvastada olulisi vigu tõestustes ning avastada ebakorrektseid tulemusi. Turvakriitiliste protokollide korral pole selline olukord vastuvõetav: olemasolev turvatõestus peaks alati tagama protokolli turvalisuse. Seetõttu on oluline tagada, et turvatõestused ei sisalda vigu. Ühe võimalusena võib kasutada tõestusassistente, kus kasutaja koostab tõestuse ning arvutiprogramm kontrollib selle korrektsust. Selle tulemusena saadud tõestus on palju usaldusväärsem, sest isegi pikkade ning keerukate tõestuste korral ei aktsepteeri arvutiprogramm ebakorrektseid tõestusamme. Pikemas perspektiivis vähendavad arvutipõhised turvatõestused nõrkuste arvu turvakriitilistes rakendustes ning seega ka kulusid, mis tulenevad juba standarditud ning juurutatud krüptograafiliste lahenduste väljavahetamisest. Antud projekti eesmärgiks on luua raamistik ning keskkond arvutipõhiste tuvatõestuste loomiseks ning verifitseerimiseks. Arenduses järgime järgnevaid disainieesmärke: * Tõestus esitub niiöelda "mängude jadana". Krüptograafias peetakse selliseid tõestusi kõige selgemaks ning formaalsemaks viisiks esitada krüptograafilisi tõestusi. * Enamik krüptograafe peaks suutma kasutada meie töövahendit, st. rakenduse kasutamine ei tohi eeldada spetsiifilisi eelteadmisi arvutipõhistest tõestussüsteemidest. * Rakenduse abil saadud tõestused peavad olema korrektsed arvutuslikus mudelis, st. tõestus ei tohi põhineda sümbol-abstraktsioonidel nagu Dolev-Yao mudel. * Kasutusefektiivsus on üks meie peaeesmärkidest: kasutajaliides peab toetama tõestuste efektiivset loomist ja muutmist nii hästi kui võimalik.
One for the main paradigms of modern cryptography is the need to rigorously prove the security of cryptographic schemes and protocols, based only on simple and well-understood assumptions (such as, e.g., the difficulty of factoring large integers). Without such proofs, it is very likely that protocols are developed and deployed that still offer unexpected vulnerabilities. A security proof guarantees the absence of such attacks (unless the underlying assumptions are false, of course). In reality, however, the situation is not as simple. Security proofs of cryptographic schemes tend to be quite complex. A hand-written proof is likely to contain a variety of small mistakes, simplifications, and overlooked cases. In some cases, incorrect results have been well-known to the cryptographic community for years until their proofs have been discovered to be flawed. For security-critical protocols, this situation is hardly acceptable: the whole point of a proof is to enable a high level of trust in the protocol. Therefore, we need a way to ensure that security proofs do not contain mistakes. This can be achieved by computer-aided verification: the security proof is developed by a human, but the proof is checked by the computer. The computer will not, even in long and complex proofs, inadvertently accept incorrect reasoning steps. This produces a much higher level of trust in security protocols than hitherto possible. On the long run, computer-aided verification avoids exploitable security vulnerabilities in critical applications, and unnecessary costs when already standardized and deployed cryptographic schemes have to be modified. In this project, we will develop a framework and tool that permits us to develop security proofs of cryptographic schemes and protocols and have to them verified by the computer. Our development will follow the following design principles: * Proofs are structures as so-called "sequences of games". This is commonly accepted by cryptographers to be the cleanest and most rigorous way of formulating cryptographic proofs. * The tool should be accessible for cryptographers (i.e., no specialized knowledge in computer-aided verification should be necessary). * The tool should produce proofs that are sound in the so-called "computational model" (i.e., it should not symbolic idealizations such as "Dolev-Yao models"). * The tool should focus on productivity: the user interface should support development and editing of the proof as far as possible.