| dc.description.abstract | Real-Time Maude extends the rewriting logic-based Maude tool to
support formal specification, simulation, and further formal analysis
of real-time systems. The specification language of Real-Time Maude
emphasizes expressiveness and ease of specification. The
high-performance Real-Time Maude tool provides a range of analysis
capabilities, including (timed) rewriting for prototyping,
(time-bounded) explicit-state breadth-first search for reachability
analysis, and time-bounded linear temporal logic model
checking. Real-Time Maude has previously been used to model and
analyze a set of advanced real-time systems, such as large
communication protocols, complex wireless sensor networks, and
scheduling algorithms. Each of these studies shows that Real-Time
Maude has much to contribute in the modeling and analysis of
distributed real-time systems. This master's thesis explores the use
of Real-Time Maude to model and analyze time-dependent security
protocols. I have modeled and analyzed two well known time-dependent
cryptographic protocol: the benchmark Wide-mouthed-frog
protocol, and the larger "commercial" Kerberos protocol.
To analyze the protocols in a hostile environment, we need to model
intruders. I have first defined a very general "Dolev-Yao" intruder,
which can perform any number of actions in zero time. This leads to
"Zeno" behaviors, and nontermination of our time-bounded analysis
commands within reasonable time and space constraints. In this thesis,
I have suggested to avoid such Zeno behaviors by restricting the
intruders to perform at most n actions per time unit. The advantage
of such a restricted intruder model is that the model is more
intuitive and does not lead to "Zeno" behaviors, and that time-bounded
search and model checking commands are guaranteed to terminate.
Furthermore, since the analysis commands terminate, we can define a
strategy that increases the intruder capacity after each "failed"
command. In this way, all possible intruder behaviors are still
"covered". Although such a strategy should be easy to implement, I
have not had the time to do so.
Instead, I gradually increased "by hand" the intruder capacity after
analysis commands that did not find errors, and was able to discover
all known flaws as well some new flaws that, to the best of my
knowledge, have not been described previously. The models of
Wide-mouthed frog and Kerberos in Real-Time Maude seems more
intuitive, easier to understand, and more natural than other published
work. Furthermore, we expressed advanced properties of the systems
quite easily using Real-Time Maude' search commands or its model
checker commands. | nor |