saag-1----Page:8
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
|
The Back-ends The On-the-fly Model-Checker (OFMC) performs protocol analysis by exploring the transition system in a demand-driven way. The Constraint-Logic-based Attack Searcher (CL-AtSe) applies constraint solving with powerful simplification heuristics and redundancy elimination techniques. The SAT-based Model-Checker (SATMC) builds a propositional formula encoding all the possible attacks (of bounded length) on the protocol and feeds the result to a SAT solver. TA4SP (Tree Automata based on Automatic Approximations for th Analysis of Security Protocols) approximates the intruder knowledge by using regular tree languages. |