OFMC: A symbolic model checker for security protocols

By David A. Basin, Sebastian Alexander Mödersheim, Luca Viganò. International Journal of Information Security, 2005

544 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

A Secure Biometrics-Based Multi-Server Authentication Protocol Using Smart Cards (2015, methodology): “We have simulated our scheme using the widely-accepted OFMC backend [48] for the formal security veriﬁcation, and the results are shown in Figure 1.”
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016, methodology): “, 2014) for bounded attack depth (which implies bounded sessions and messages), Cl-AtSe (Turuani, 2006) and OFMC (Basin et al., 2005; Mödersheim and Viganò, 2009) for bounded sessions, and TA4SP (Boichut et al.”
Automated Security Protocol Analysis With the AVISPA Tool (2006, methodology): “All the four backends are able to carry out the analysis with respect to the typed model, and CL-AtSe and OFMC are also able to adopt the untyped model.”
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications (2005, methodology): “P A T P A T P A TE TS UMTS_AKA 3 3 0 0,02 3 0 0,01 3 0 0,11 0,00 AAAMobileIP 7 7 0 0,75 7 0 0,20 7 0 1,32 0,01 ISO-PK1 1 1 1 0,02 1 1 0,00 1 1 0,05 0,00 ISO-PK2 1 1 0 0,05 1 0 0,00 1 0 1,62 0,00 ISO-PK3 2 2 2 0,04 2 2 0,01 2 2 0,27 0,00 ISO-PK4 2 2 0 0,54 2 0 0,03 2 0 1.153 1,16 LPD-MSR 2 2 2 0,02 2”
Scyther : semantics and verification of security protocols (2006, methodology): “The On-the-Fly Model Checker (OFMC, [14]) is part of the AVISPA tool set [7], and is a model checker for security protocols.”