Sciweavers

Share
FOSAD
2009
Springer

The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols

9 years 9 months ago
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 Onthe-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. 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 constr...
Sebastian Mödersheim, Luca Viganò
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FOSAD
Authors Sebastian Mödersheim, Luca Viganò
Comments (0)
books