|
The talk about verifying security protocols. The presenter
demonstrated an example of a security hole in X.509 (then draft)
protocol: verifying recency of messages.
The protocol analyser tries to determine if user-specified insecure
states are reachable. The analyser does generate and test. One part
of the analyser generates states, and the other part tests to see if
the state belongs to a set of insecure states. The protocol is
specified in terms of communicating state machines, in terms of
constant and universally quantified variables. The user specifies
insecure states in terms of constants and existentially quantified
variables (there exists x such that ...). The analyzer uses inductive
techniques to prune out the infinite number of states (if it can prove
by induction that all states in a particular infinite set of states
are secure). The analyzer uses lost of tricks to constrain state
explosion: common tricks such as memoization and many specific tricks.
The analyzer is written in a compiled Prolog.
The largest analyzed protocols: IKE (Internet Key exchange, from IETF)
and the drafts of the IETF domain authentication protocol. The author
is involved with IETF working groups, so she can test draft
protocols. She did find errors (e.g., in early IKE drafts), which were
fixed in the later drafts. The speed wasn't great (it may take from
seconds to a day) but the protocol analyzer turns out rather scalable.
-- Oleg
|
Using a Language to Build an Experimental Analysis Tool