OFMC
The open-source fixed-point model checker for symbolic analysis of security protocols. We introduce the open-source fixed-point model checker OFMC for symbolic security protocol analysis, which extends the on-the-fly model checker (the previous OFMC). The native input language of OFMC is the AVISPA Intermediate Format IF. OFMC also supports AnB, a new Alice-and-Bob-style language that extends previous similar languages with support for algebraic properties of cryptographic operators and with a simple notation for different kinds of channels that can be used both as assumptions and as protocol goals. AnB specifications are automatically translated to IF.par OFMC performs both protocol falsification and bounded session verification by exploring, in a demand-driven way, the transition system resulting from an IF specification. OFMC’s effectiveness is due to the integration of a number of symbolic, constraint-based techniques, which are correct and terminating. The two major techniques are the lazy intruder, which is a symbolic representation of the intruder, and constraint differentiation, which is a general search-reduction technique that integrates the lazy intruder with ideas from partial-order reduction. Moreover, OFMC allows one to analyze security protocols with respect to an algebraic theory of the employed cryptographic operators, which can be specified as part of the input. We also sketch the ongoing integration of fixed-point-based techniques for protocol verification for an unbounded number of sessions.
Keywords for this software
References in zbMATH (referenced in 27 articles )
Showing results 1 to 20 of 27.
Sorted by year (- Sattarzadeh, Behnam; Fallah, Mehran S.: Automated type-based analysis of injective agreement in the presence of compromised principals (2015)
- Adão, Pedro; Mateus, Paulo; Viganò, Luca: Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete (2014)
- Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia: State space reduction in the Maude-NRL protocol analyzer (2014)
- Backes, Michael; Bendun, Fabian; Unruh, Dominique: Computational soundness of symbolic zero-knowledge proofs: weaker assumptions and mechanized verification (2013)
- Chrétien, Rémy; Cortier, Véronique; Delaune, Stéphanie: From security protocols to pushdown automata (2013)
- Tounsi, Wiem; Cuppens-Boulahia, Nora; Cuppens, Frédéric; Garcia-Alfaro, Joaquin: Formal verification of a key establishment protocol for EPC Gen2 RFID systems: work in progress (2012)
- Basin, David; Caleiro, Carlos; Ramos, Jaime; Viganò, Luca: Distributed temporal logic for the analysis of security protocol models (2011)
- Gao, Han; Nielson, Flemming; Nielson, Hanne Riis: \ssfCaPiTo: Protocol stacks for services (2011)
- Backes, Michael; Maffei, Matteo; Mohammadi, Esfandiar: Computationally sound abstraction and verification of secure multi-party computations (2010)
- Escobar, Santiago; Meadows, Catherine; Meseguer, José: Maude-NPA: cryptographic protocol analysis modulo equational properties (2009)
- Hutter, Dieter; Monroy, Raúl: On the automated correction of protocols with improper message encoding (2009)
- Mödersheim, Sebastian; Viganò, Luca: The open-source fixed-point model checker for symbolic analysis of security protocols (2009)
- Armando, Alessandro; Compagna, Luca: SAT-based model-checking for security protocols analysis (2008)
- Backes, Michael; Berg, Matthias; Unruh, Dominique: A formal language for cryptographic pseudocode (2008)
- Backes, Michael; Pfitzmann, Birgit: Limits of the BRSIM/UC soundness of Dolev-Yao-style XOR (2008)
- Bertolotti, Ivan Cibrario; Durante, Luca; Sisto, Riccardo; Valenzano, Adriano: Efficient representation of the attacker’s knowledge in cryptographic protocols analysis (2008)
- Ceelen, Pieter; Mauw, Sjouke; Radomirovic, Sasa: Chosen-name attacks: An overlooked class of type-flaw attacks. (2008)
- Dojen, Reiner; Jurcut, Anca; Coffey, Tom; Gyorodi, Cornelia: On establishing and fixing a parallel session attack in a security protocol (2008)
- Basin, David; Kuruma, Hironobu; Miyazaki, Kunihiko; Takaragi, Kazuo; Wolff, Burkhart: Verifying a signature architecture: a comparative case study (2007)
- Lafourcade, Pascal; Lugiez, Denis; Treinen, Ralf: Intruder deduction for the equational theory of abelian groups with distributive encryption (2007)