The scyther tool: verification, falsification, and analysis of security protocols. With the rise of the Internet and other open networks, a large number of security protocols have been developed and deployed in order to provide secure communication. The analysis of such security protocols has turned out to be extremely difficult for humans, as witnessed by the fact that many protocols were found to be flawed after deployment. This has driven the research in formal analysis of security protocols. Unfortunately, there are no effective approaches yet for constructing correct and efficient protocols, and work on concise formal logics that might allow one to easily prove that a protocol is correct in a formal model, is still ongoing. The most effective approach so far has been automated falsification or verification of such protocols with state-of-the-art tools such as ProVerif [1] or the Avispa tools [2]. These tools have shown to be effective at finding attacks on protocols (Avispa) or establishing correctness of protocols (ProVerif).

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Baelde, David; Delaune, Stéphanie; Hirschi, Lucca: A reduced semantics for deciding trace equivalence (2017)
  2. Cheval, Vincent; Comon-Lundh, Hubert; Delaune, Stéphanie: A procedure for deciding symbolic equivalence between sets of constraint systems (2017)
  3. Kassem, Ali; Falcone, Yliès; Lafourcade, Pascal: Formal analysis and offline monitoring of electronic exams (2017)
  4. Mansor, Hafizah; Markantonakis, Konstantinos; Akram, Raja Naeem; Mayes, Keith; Gurulian, Iakovos: Log your car: reliable maintenance services record (2017)
  5. Chadha, Rohit; Cheval, Vincent; Ciob^acă, Ştefan; Kremer, Steve: Automated verification of equivalence properties of cryptographic protocols (2016)
  6. Fröschle, Sibylle: Causality, behavioural equivalences, and the security of cyberphysical systems (2015)
  7. Sun, Chang-Ai; Wang, Zuoyi; Wang, Guan: A property-based testing framework for encryption programs (2014) ioport
  8. Cheval, Vincent; Cortier, Véronique; Delaune, Stéphanie: Deciding equivalence-based properties using constraint solving (2013)
  9. Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella: Computer-aided security proofs for the working cryptographer (2011)
  10. Basin, David; Caleiro, Carlos; Ramos, Jaime; Viganò, Luca: Distributed temporal logic for the analysis of security protocol models (2011)
  11. Cremers, Cas J.F.: Session-StateReveal is stronger than eCKs EphemeralKeyReveal: using automatic analysis to attack the NAXOS protocol (2010)
  12. Cremers, Cas J.F.; Lafourcade, Pascal; Nadeau, Philippe: Comparing state spaces in automatic security protocol analysis (2009)
  13. Mödersheim, Sebastian; Viganò, Luca: The open-source fixed-point model checker for symbolic analysis of security protocols (2009)
  14. Cremers, Cas J.F.: The Scyther tool: Verification, falsification, and analysis of security protocols. Tool paper (2008) ioport