000114775 001__ 114775
000114775 005__ 20190619003135.0
000114775 0247_ $$2doi$$a10.5075/epfl-thesis-4007
000114775 02470 $$2urn$$aurn:nbn:ch:bel-epfl-thesis4007-8
000114775 02471 $$2nebis$$a5471973
000114775 037__ $$aTHESIS
000114775 041__ $$aeng
000114775 088__ $$a4007
000114775 245__ $$aTheory and tool support for the formal verification of cryptographic protocols
000114775 269__ $$a2008
000114775 260__ $$bEPFL$$c2008$$aLausanne
000114775 300__ $$a278
000114775 336__ $$aTheses
000114775 502__ $$aDaniel Hirschkoff, Viktor Kuncak, Dale Miller
000114775 520__ $$aCryptographic protocols are an essential component of network communications. Despite their relatively small size compared to other distributed algorithms, they are known to be error-prone. This is due to the obligation to behave robustly in the context of unknown hostile attackers who might want to act against the security objectives of the jointly interacting entities. The need for techniques to verify the correctness of cryptographic protocols has stimulated the development of new frameworks and tools during the last decades. Among the various models is the spi calculus: a process calculus which is an extension of the pi calculus that incorporates cryptographic primitives. Process calculi such as the spi calculus offer the possibility to describe in a precise and concise way distributed algorithms such as cryptographic protocols. Moreover, spi calculus offers an elegant way to formalise some security properties of cryptographic protocols via behavioural equivalences. At the time this thesis began, this approach lacked tool support. Inspired by the situation in the pi calculus, we propose a new notion of behavioural equivalence for the spi calculus that is close to an algorithm. Besides, we propose a "coq" formalisation of our results that not only validates our theoretical developments but also will eventually be the basis of a certified tool that would automate equivalence checking of spi calculus terms. To complete the toolchain, we propose a formal semantics for an informal notation to describe cryptographic protocols, so called protocol narrations. We give a rigorous procedure to translate protocol narrations into spi calculus terms; this constitutes the foundations of our automatic translation tool "spyer".
000114775 6531_ $$acryptographic protocols
000114775 6531_ $$aprocess calculi
000114775 6531_ $$aspi calculus
000114775 6531_ $$abisimulations
000114775 6531_ $$aproof assistants
000114775 6531_ $$aprotocoles cryptographiques
000114775 6531_ $$acalculs de processus
000114775 6531_ $$aspi calcul
000114775 6531_ $$abisimulations
000114775 6531_ $$aassistants de preuve
000114775 700__ $$0241935$$g156069$$aBriais, Sébastien
000114775 720_2 $$aNestmann, Uwe$$edir.
000114775 720_2 $$aOdersky, Martin$$edir.$$g126003$$0241835
000114775 8564_ $$uhttps://infoscience.epfl.ch/record/114775/files/EPFL_TH4007.pdf$$zTexte intégral / Full text$$s1584849$$yTexte intégral / Full text
000114775 909C0 $$xU10409$$0252187$$pLAMP
000114775 909CO $$pthesis-public$$pDOI$$qDOI2$$pIC$$ooai:infoscience.tind.io:114775$$qGLOBAL_SET$$pthesis$$pthesis-bn2018
000114775 918__ $$dEDHP$$bIC-SIN$$cIIF$$aIC
000114775 919__ $$aLAMP1
000114775 920__ $$b2008$$a2008-1-25
000114775 970__ $$a4007/THESES
000114775 973__ $$sPUBLISHED$$aEPFL
000114775 980__ $$aTHESIS