From Formal to Computational Authenticity: An approach for reconciling formal and computational authenticity
Author
Garde, Michael
Term
4. term
Education
Publication year
2013
Submitted on
2013-06-11
Pages
40
Abstract
Kryptografiske protokoller er sæt af regler, der beskytter kommunikation. De skal typisk sikre to ting: hemmeligholdelse (at kun de rette kan læse indholdet) og autenticitet (at beskeder virkelig stammer fra den rette afsender og ikke er ændret). Forskere undersøger sådan sikkerhed på to hovedmåder. I den formelle (symbolske) tilgang bruger man forenklede modeller og logiske beviser. I den beregningsmæssige tilgang beskriver man angribere og sikkerhed i forhold til algoritmer og beregningssværhed. Disse to tilgange har længe udviklet sig hver for sig, og det første forsøg på at bygge bro kom i 2001. Området er stadig meget aktivt, og trods mange fremskridt er forholdet mellem formel og beregningsmæssig autenticitet ikke fuldt afklaret. I dette arbejde giver vi et overblik over, hvordan hemmeligholdelse og autenticitet forstås i begge tilgange, og vi skitserer en fremgangsmåde, der kan vise, at autenticitet i den formelle tilgang indebærer autenticitet i den beregningsmæssige tilgang.
Cryptographic protocols are sets of rules that protect communication. They aim to provide two core guarantees: secrecy (only the intended parties can read the content) and authenticity (messages truly come from the claimed sender and are not altered). Researchers study such security in two main ways. In the formal (symbolic) paradigm, they use simplified models and logical proofs. In the computational paradigm, they reason about attackers and security in terms of algorithms and computational hardness. These lines of work long developed separately, and the first attempt to bridge them appeared in 2001. The area remains active, and despite many advances, the relation between formal and computational authenticity is not fully settled. In this paper, we survey how secrecy and authenticity are treated in both paradigms and outline an approach intended to show that authenticity in the formal paradigm implies authenticity in the computational paradigm.
[This abstract was generated with the help of AI]
Keywords
Documents