Information security is central to the proper functioning and acceptance
of a wide spectrum of modern systems. Unfortunately, constructing
secure systems is difficult as developing secure building blocks "in the
small" and their composition to systems "in the large" are both
error-prone activities. In this talk, I will show how
formal methods --- in particular the use of formal models combined with
symbolic computation --- can be employed to tackle both kinds of
problems. As examples, I present results on analyzing security
protocols, and the automatic generation of secure software-architectures
for middleware-based distributed systems from high-level models.