Security is an active topic of research in the international arena. There are too many projects to mention here, looking at the issues from various different angles. For instance, the oxygen project at the famous Massachusetts Institute of Technology (MIT) addresses a world in which one is surrounded by large numbers of electronic devices. To the human, their collective functions are present as an ambient intelligence, although the individual ones are no longer always recognizable as such. Ron Rivest's group is studying the security issues associated with this setting. Protection of privacy, trust, etc. are key aspects. The project is pioneering, also in the sense that for many of these issues the mathematical framework is not yet mature.
In the countries surrounding the Netherlands, France and Germany
operate national programs with a mission that is almost identical to
the SENTINELS mission (see http://acisi.loria.fr for the
French program and http://www.iig.uni-freiburg.de/telematik/spps for
the German program). This indicates that also for the Netherlands
national funding for security is essential: in such a strategic
area we should not stay behind. At this moment, Belgium and the UK do
not have coherent security research programs.
Internationally, France is leading both in deployment of smart cards
and in industrial R&D. The Netherlands is strong in fundamental smart
card research (KUN & UT) and is leading in smart card
hardware security evaluation (TNO). Over the past years, industrial
R&D has weakened. Deployment of smart cards is still an emerging
field, where the telecom and financial sectors play a leading
role. But recent international developments provide a new impetus for
the use of smart cards as national citizen identity cards. Hartel and
Jacobs are the academic contributors to the plans for 6th Framework
program of the European Commission in the area of smart card
research [13].
Biometrics research is predominantly performed in the US and Israel.
In the Netherlands, TNO, CWI and UT are active in this area.
Below, we provide some more detail on one important topic: protocol
verification. Three active and important areas of research in protocol
verification are distinguished: verification, formalisms and
abstractions. In all of these the position of the Netherlands must be
strengthened.
Several methods have been developed for analyzing security protocols. The best-known method is the BAN Logic of Authentication [8]. Protocols are specified in a rather idealized way which allows one to deduce facts about the beliefs of agents involved in a protocol with the help of specialized deduction rules. However, BAN logics do not cover all security aspects of protocols (there is, for instance, no modeling of an intruder) and are incapable of detecting particular kinds of flaws. Also, there are no satisfactory semantics for BAN logics. However, BAN logic still seems to provide the most cost-effective ways of discovering flaws in security protocols.
Model checking techniques [32] analyze protocols by building models of finite instantiations of the protocol, along with a model of the most general intruder who can interact with that protocol, and using a model checker to explore the state space looking for insecure states. These techniques have been successful at finding new attacks, however, they are restricted to finite instantiations of a protocol. A failure to find an attack does not, in general, imply that there are no attacks on larger instantiations. In [27], Lowe showed that for a particular class of protocols, if there are any attacks on the protocol, then there are attacks upon a particular small instantiation, and so model checking this instantiation is enough to verify the protocol.
Several general-purpose theorem provers, like for instance ISABELLE,
COQ or SPASS, have been used to analyze and evaluate the security
goals of protocols. These theorem provers are special computer
programs (``logical calculators'') that aid in complex logical
reasoning involving many possible case distinctions (which is
difficult for humans).
For instance, Paulson's
approach is based on an explicit representation of agents and intruders
and the knowledge they gain from inspecting a (partial) run of a
protocol. As traces and also the functions concerning the knowledge of
agents are defined by recursion, most proofs involve induction.
Applications of this approach to commercial protocols are given
in [5,30]. Z/Eves [33] has been used by ORA (Canada)
to analyze Public Key Infrastructures, authentication protocols,
security standards such as FIPS 140-1 and the Common Criteria.
There has been significant work on developing formal models of security protocol behavior. Thayer et al. use ordered graphs called strand spaces to model protocol runs. Security properties can be reduced to properties on graphs. Song et al. have automated this verification.
Abadi and Gordon developed the Spi Calculus, extending the Pi Calculus with cryptographic primitives. This has been used as the formal underpinning for a number of other pieces of work. For example, Abadi has developed typing rules that allow secrecy properties to be proven of security protocols; and Gordon and Jeffrey have extended this to authentication properties.
Cervesato et al. have developed a meta-notation for protocol analysis based upon multi-set term rewriting, and Durgin et al. have used this to prove decidability results of protocols.
Commercial protocols are larger than the protocols typically appearing in the academic literature and it is an open question how developed verification methods scale up in practice. Hui and Lowe have developed simplifying transformations that have the property of preserving faults, which means that a protocol is secure if its simplified version is secure. These transformations can be used to simplify a commercial protocol to the point that standard analysis techniques can be applied.
There has been a limited amount of work on the methodology to develop secure protocols. Abadi and Needham [1] have proposed a list of prudent engineering principles for protocol design, which, if followed, prevent most attacks upon protocols. Type flaw attacks are attacks where a field of one type is misinterpreted as being of another type; Heather et al. have developed an implementation technique that prevents all type flaw attacks.
Log in
Sentinels
General info
