### Citations

1012 | publications by the team in recent years - Major |

124 | Verifying privacy-type properties of electronic voting protocols: A taster
- Delaune, Kremer, et al.
(Show Context)
Citation Context ...on for Scientific and Technical Research). Other examples of indistinguishability properties that we have studied are privacy-related properties such as those appearing in electronic voting protocols =-=[5]-=- and offline guessing attacks [47]. In SECSI, we have been working on decision procedures, combination and composition results for such equivalence properties. In particular, decision procedures for m... |

59 | Computationally sound implementations of equational theories against passive adversaries
- Baudet, Cortier, et al.
(Show Context)
Citation Context ..., as part of the ARA SSIA Formacrypt project, whose members include Martín Abadi and Bruno Blanchet. A more recent French-Japanese also continues this research theme. One early paper on this topic is =-=[1]-=-. Laurent Mazaré, a PhD student of Yassine Lakhnech on these themes, spent 6 months as postdoc at SECSI and worked actively on the connection between formal and computational models in the presence of... |

55 | Cryptographic protocol analysis on real c code - Goubault-Larrecq, Parrennes - 2005 |

47 | Guessing attacks and the computational soundness of static equivalence - Abadi, Baudet, et al. - 2006 |

40 | Election verifiability in electronic voting protocols.
- Kremer, Ryan, et al.
- 2010
(Show Context)
Citation Context ...y has been introduced in electronic voting systems to achieve transparency: the voter should not have to trust the election authorities, the hardware or the software in order to trust the outcome. In =-=[35]-=- we present a formal, symbolic definition of election verifiability for electronic voting protocols in the context of the applied pi calculus. Our definition is given in terms of boolean tests which c... |

36 | Computational soundness of observational equivalence. - Comon-Lundh, Cortier - 2008 |

32 |
Attacking and fixing PKCS#11 security tokens
- Bortolozzo, Centenaro, et al.
- 2010
(Show Context)
Citation Context ... SATMC. If SATMC finds an attack, Tookan executes the attack directly on the token. Tookan is described in a paper published this year at the ACM Computer and Communications Security Conference (CCS) =-=[28]-=-. The paper discusses results from testing on 18 commercially available cryptographic devices: 10 were found to be vulnerable to attack. The commercialisation of Tookan is underway with the support of... |

25 |
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems
- Cortier, Kremer, et al.
- 2010
(Show Context)
Citation Context ...emer, Joe-Kai Tsay, Yusuke Kawamoto. In the past decade an impressive number of results have been obtained related to the use of symbolic techniques for computational proofs of security protocols. In =-=[16]-=- we survey these results. Even though a large number of results exist, they are still not satisfactory and using symbolic techniques for achieving computational proofs is still an active area of resea... |

21 | Computing knowledge in security protocols under convergent equational theories.
- Ciobaca, Delaune, et al.
- 2009
(Show Context)
Citation Context ...imulation conditions. 6.1.1. Static equivalence. As explained above, static equivalence is a cornerstone to provide decision procedures for observational equivalence. 10 Activity Report INRIA 2010 In =-=[13]-=-, Ştefan Ciobâcă, Stéphanie Delaune and Steve Kremer propose a representation of deducible terms to overcome the limitation of a procedure proposed by M. Baudet et al. in [49]. The procedure termina... |

21 | Deciding security properties for cryptographic protocols. Application to key cycles - Comon-Lundh, Cortier, et al. |

19 | Automating security analysis: symbolic equivalence of constraint systems.
- Cheval, Comon-Lundh, et al.
- 2010
(Show Context)
Citation Context ...The tool is able to decide the equivalence of such constraint systems, i.e. deciding whether two constraints systems have the same set of solutions. The algorithm implemented in ADECS is described in =-=[30]-=-. 6. New Results 6.1. Indistinguishability proofs Participants: Vincent Cheval, Ştefan Ciobâcă, Hubert Comon-Lundh, Stéphanie Delaune, Steve Kremer. Most existing results focus on trace properties l... |

17 | Modeling and Verifying Ad Hoc Routing Protocols, in:
- Arnaud, Cortier, et al.
- 2010
(Show Context)
Citation Context ... Secure routing protocols use cryptographic mechanisms in order to prevent a malicious node from compromising the discovered route. Mathilde Arnaud, Véronique Cortier and Stéphanie Delaune present in =-=[26]-=- a calculus for modeling and reasoning about security protocols, including in particular secure routing protocols. Their calculus extends standard symbolic models to take into account the characterist... |

14 | The ORCHIDS Intrusion Detection Tool. - Olivain, Goubault-Larrecq - 2005 |

14 | Protocol composition for arbitrary primitives
- Ciobâcǎ, Cortier
- 2010
(Show Context)
Citation Context ...col, relying on a shared key, guarantees a given property then these protocols can be composed sequentially. This allows to implement the shared key assumption by any secure key exchange protocol. In =-=[31]-=-, Ştefan Ciobâcă and Véronique Cortier show that if two protocols use disjoint cryptographic primitives, their composition is secure if the individual protocols are secure, even if they share data. ... |

12 | Associative-commutative deducibility constraints - Bursuc, Comon-Lundh, et al. - 2007 |

11 | Formal analysis of PKCS#11 and proprietary extensions - Delaune, Kremer, et al. - 2010 |

11 | Formal Analysis of Privacy for Vehicular MixZones. In
- Dahl, Delaune, et al.
- 2010
(Show Context)
Citation Context ...econd raises privacy issues. Mixzones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem. 12 Activity Report INRIA 2010 In =-=[32]-=-, Morten Dahl, Stéphanie Delaune and Graham Steel describe a formal analysis of mix-zones. They give a set of necessary conditions for any mix-zone protocol to preserve privacy and they analyse a part... |

10 | M.: Towards automatic analysis of election verifiability properties
- Smyth, Ryan, et al.
- 2010
(Show Context)
Citation Context ...nd signatures, homomorphic encryption and mixnets. We demonstrate the applicability of our formalism by analysing three protocols: FOO, Helios 2.0, and Civitas (the latter two have been deployed). In =-=[36]-=-, we presented a stronger definition of verifiability: it had the advantage of automated tool support for porving the property, but it was too strong for a variety of protocols in the literature. 6.6.... |

9 |
G.: A Formal Analysis of Authentication
- Delaune, Kremer, et al.
- 2010
(Show Context)
Citation Context ... that lacks a definite security policy. In a paper at FAST (also presented at the SecCo workshop), we discussed a basis for a security policy based around formally specified correspondence properties =-=[33]-=-, [38]. We showed how these properties can be checked using the protocol analysis tool Proverif, and showed examples of commands in the API that fail to assure such security. We showed how the standar... |

8 | Decidability and combination results for two notions of knowledge in security protocols
- Cortier, Delaune
(Show Context)
Citation Context ...of trapdoor bit commitment encountered when studying electronic voting protocols. The algorithm has been implemented in the KiSs tool. This work is a journal version of the work presented in [56]. In =-=[15]-=-, Stéphanie Delaune, in collaboration with Véronique Cortier (LORIA, France), shows that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility ... |

6 | De Groot duality and models of choice: angels, demons and nature - Goubault-Larrecq |

5 | On Noetherian Spaces, in "Proceedings of the 22nd Annual - GOUBAULT-LARRECQ - 2007 |

5 | K.: Choquet-Kendall-Matheron theorems for nonHausdorff spaces
- Goubault-Larrecq, Keimel
- 2011
(Show Context)
Citation Context ...(U. Darmstadt) informed Goubault-Larrecq that this was a definite improvement over a series of results in mathematics due to Choquet in the 1950s, then to Kendall and Matheron in the 1970s. The paper =-=[22]-=- is probably the ultimate result in this direction, showing that, up to a bijection, continuous credibilities are the same thing that continuous valuations (essentially, measures) over the Smyth hyper... |

5 | Computationally sound analysis of protocols using bilinear pairings - Kremer, Mazaré - 2010 |

5 | Reducing Equational Theories for the Decision of Static Equivalence
- KREMER, MERCIER, et al.
(Show Context)
Citation Context ... journal version of the works presented in [46], [66]. Steve Kremer and Antoine Mercier, in collaboration with Ralf Treinen (PPS, France), have obtained a combination result for non-disjoint theories =-=[24]-=-. Their method allows one to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equati... |

4 | Some Ideas on Virtualized Systems Security, and Monitors
- BENZINA, GOUBAULT-LARRECQ
(Show Context)
Citation Context ...llaboration with Bertin technologies in the setting of the PFC, System@tic project. 5.4. The RuleGen tool Participant: Hedi Benzina [in charge]. The RuleGen tool implements the algorithm described in =-=[27]-=-. The idea is that the system administrator can write security policies using simple LTL (Linear Temporal Logic) formulas. RuleGen permits an automatic generation of attacks signatures from these form... |

3 | Tree Automata with One Memory, Set Constraints and Cryptographic Protocols, in "Theoretical Computer Science - COMON-LUNDH, CORTIER - 2005 |

3 |
ωQRB-Domains and the Probabilistic Powerdomain
- GOUBAULT-LARRECQ
- 2010
(Show Context)
Citation Context ...ional languages with polymorphic choice, except for the trivial one where types are interpreted as mere dcpos—not necessarily continuous, hence with possibly strange properties. Jean Goubault-Larrecq =-=[34]-=- proposed to look at the question under a different angle, obtaining the first significant progress on the question since Jung and Tix’s 1998 paper. By replacing continuous dcpos by socalled quasi-con... |

2 |
Finite Models for Formal Security Proofs, in "Journal of Computer Security
- GOUBAULT-LARRECQ
- 2010
(Show Context)
Citation Context ...ls. It was shown by the author at the CSF’08 conference how h1mc, the model-checker of the suite, could be used to produce Coq proofs of security, in an automated way. Since then, the journal version =-=[20]-=- lists additional case studies, and makes a thorough analysis of the algorithmic details behind h1mc. 5.3. ORCHIDS modules Participant: Hedi Benzina [in charge]. The Auditd sensor was implemented as a... |

2 | Musings Around the Geometry of Interaction - GOUBAULT-LARRECQ - 2010 |

2 | Model checking concurrent programs with nondeterminism and randomization.
- Chadha, Sistla, et al.
- 2010
(Show Context)
Citation Context ...lso the proofs are considerably simpler, using a very simple case of Groemer’s integral theorem. The problem of model checking concurrent, randomized and nondeterministic programs was investigated in =-=[29]-=-. Usually, such programs are modeled as finite-state Markov Decision Processes (MDPs). A program P is said to satisfy a linear-time property Spec with probability greater than the threshold x if under... |

2 | A Generalization of P-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs
- BOUISSOU, GOUBAULT, et al.
- 2010
(Show Context)
Citation Context ...ract Interpretation of Numerical Programs Participant: Jean Goubault-Larrecq. 14 Activity Report INRIA 2010 As part the ANR programme blanc CPP project, Bouissou, Goubault, Goubault-Larrecq and Putot =-=[37]-=- showed how to extend a precise abstract interpretation framework based on so-called zonotopes (i.e., polytopes that are symmetric around a given point called its center) to programs that take some in... |

1 | Analyse statique de programmes multi-thread pour l’embarqué, Laboratoire Spécification et Vérification - CARRÉ - 2010 |

1 | Symbolic bisimulation for the applied pi calculus, in "Journal of Computer Security - DELAUNE, KREMER, et al. - 2010 |

1 |
A Formal Analysis of Authentication in the TPM (short paper
- DELAUNE, KREMER, et al.
(Show Context)
Citation Context ...lacks a definite security policy. In a paper at FAST (also presented at the SecCo workshop), we discussed a basis for a security policy based around formally specified correspondence properties [33], =-=[38]-=-. We showed how these properties can be checked using the protocol analysis tool Proverif, and showed examples of commands in the API that fail to assure such security. We showed how the standard coul... |