Výsledky vyhledávání - "Blanchet, Bruno"

Report

CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)

Autor: Blanchet, Bruno

This document presents the security protocol verifier CryptoVerif.CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy, correspondence (which include authentication), and indistinguishabili

Externí odkaz: http://arxiv.org/abs/2310.14658

Zobrazit plný text záznamu

Kniha

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. [elektronicky zdroj]

Autor: Blanchet, Bruno

Externí odkaz: Kolekce e-knih KNAV Registrovani uzivatele: plny text online 5 minut, dalsi pristup na vyzadani. Registered users: full text online 5 minutes, further access on request.

Report

The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm

Autor: Blanchet, Bruno

Publikováno v: EPTCS 373, 2022, pp. 14-22

ProVerif is a widely used security protocol verifier. Internally, ProVerif uses an abstract representation of the protocol by Horn clauses and a resolution algorithm on these clauses, in order to prove security properties of the protocol or to find a

Externí odkaz: http://arxiv.org/abs/2211.12227

Zobrazit plný text záznamu

Report

The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication

Autor: Abadi, Martín, Blanchet, Bruno, Fournet, Cédric

We study the interaction of the programming construct "new", which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work,

Externí odkaz: http://arxiv.org/abs/1609.03003

Zobrazit plný text záznamu

Report

Automatic Verification of Correspondences for Security Protocols

Autor: Blanchet, Bruno

We present a new technique for verifying correspondences in security protocols. In particular, correspondences can be used to formalize authentication. Our technique is fully automatic, it can handle an unbounded number of sessions of the protocol, a

Externí odkaz: http://arxiv.org/abs/0802.3444

Zobrazit plný text záznamu

Report

A Static Analyzer for Large Safety-Critical Software

Autor: Blanchet, Bruno, Cousot, Patrick, Cousot, Radhia, Feret, Jerôme, Mauborgne, Laurent, Miné, Antoine, Monniaux, David, Rival, Xavier

Publikováno v: PLDI: Conference on Programming Language Design and Implementation (2003) 196 - 207

We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a gener

Externí odkaz: http://arxiv.org/abs/cs/0701193

Zobrazit plný text záznamu