My motivation for writing this book:
The cipher Rijndael will certainly become a global standard
for symmetric encryption software and hardware and it will be found in
a full range of computational objects, from smartcards to mainframes.
At the time of publication, this text is likely to be among the first ones
that include a full exposition of this cipher.
The inclusion of an optimal public-key cryptosystem using RSA
transforms RSA from its textbook version to a practical, yet still
rigorous and secure implementation. To my knowledge, the discussion of
such an important practical realization of RSA is absent from other
textbooks on this subject. (I acknowledge a reviewer
who made me aware of this and who suggested to include this material.)
This practical discussion is complemented by a proof of exact security
results in the random oracle model.
Another principal contribution that sets this text aside from all the
existing ones is the elementary description and well motivated design
of tools built for formally reasoning about security protocols. Most
texts consider mathematical and often sophisticated techniques for
assessing the strength of, say, a particular block cipher encryption
algorithm, as their analysis component. While these techniques are
important, they are meant for the specialist whose task it is to
design new, and attack existing, cryptographic algorithms. This text
therefore delegates such specialized topics to the references, but
emphasizes the analysis of specified security protocols as a major
task in avoiding the corruption of secrecy, integrity, and anonymity
(if so desired) in a communication network. I base this choice on the
fact that inherent design flaws in protocols are, next to
implementation flaws or implementation compromises, the most likely
cause for a cryptographic system to be broken. Moreover, the detection
of such design errors is typically as hard as the discovery of bugs in
ordinary synchronous or asynchronous concurrent systems. For the
latter, automated (e.g. the model checker SMV) and semi-automated
(e.g. the theorem prover PVS) tools and specification frameworks have
been developed and are already being embraced by research and
development labs. The tool I feature is a model checker combined with
a natural deduction engine modeling an attacker, due to W. Marrero,
E. Clarke and S. Jha.
As another more applied component, I discuss D. Denning's classical
work on program certification for secure information flow,
but present it in a contemporary and rigorous
framework of a type-inference system. This treatment allows for a
formal proof that this analysis of secure information flow in programs
satisfies a non-interference property that can be used to guarantee
secrecy or integrity of information flow. I then present a semantic
approach to secure information flow in programs, due to
R. Joshi and K. R. M. Leino,
that uses weakest predicate transformers and partial correctness
proofs for its refutation and validation of program security. This
material, as well as the analysis part of the optimal RSA encryption,
constitute the more advanced part of this text and are likely to be
covered in a graduate course or presented by talented undergraduate
students in class.
Formal methods for the analysis of cryptographic systems and the secure
flow of information in programs, or their secure execution,
are currently a vibrant research area, and their fruitful
development should be a vital step toward the establishment of sound
methodologies for ``cryptographic engineering'', just as such working
standards have already emerged in conventional software
engineering. The education of future security engineers in such tools
may also help in addressing the next set of challenges in security
engineering on the internet. For example, how can one establish and
reason about a dynamically evolving ``network of trusted nodes'', what
are sound methodologies for the verification of complex specifications
within multi-party protocols (e.g. electronic cash flow between
consumers, merchants, and banks; broadcasting and multi-casting
communication sessions; etc.), and how can we realize efficient but
reliable platforms for the definition, verification, and certification of
safety policies for mobile code?
Cryptography and the certification of (mobile) code are certainly only
two requirements for the establishment and maintenance of a reliably
functioning digital society. Yet, considering that an alarming
percentage of the current cryptographic products make poor, or
sometimes even unprofessional, design decisions (choice of algorithm,
key length, protocol, etc.), it seems evident that students ought to
know the ``do and don't'' of this area. While this text is not meant to
become a standard monograph or a standard reference text, I
believe that it can well become the preferred choice of instructors
who, while not necessarily being experts in this field themselves,
mean to effectively teach students, whose background necessitates a
delicate and careful presentation and development of non-trivial
mathematical concepts and who need to see these concepts applied in a
concrete context they can relate to; this I hope to accomplish
through the inclusion of small programming exercises and larger
implementation projects. Although competing texts present more
cryptographic topics and at a more advanced level, instructors may
decide to use this text, since it also reasons about the secure
behavior of programs, noting that a framework for trusted
(mobile) code cannot be implemented with cryptographic techniques
alone: we can use cryptography to authenticate the origin of mobile
code, or to ensure the fact that this code has not been tampered with
in transit. But even if all of that has been established, we know
nothing about the actual behavior of the program when it is being
executed locally.
This text contains more material than one could cover in a 12-15 week
course. Beyond a common backbone of fundamentally important sections,
instructors will be free in omitting or emphasizing certain topics as
they deem it fit for their individual course objectives. I took great
care in presenting almost all key issues, even though some may be
condensed or confined to the exercises. At the same time, I strove for
the creation of a relatively compact, but highly interconnected and
reasonably self-contained, text. The provided links to online
research papers, tutorials, and cited reference texts should enable
instructors and students alike to extend the breadth and depth of this
text appropriately.
So far, I taught two interdisciplinary courses based on a draft of
this text in three phases. The first phase was conducted in a
``traditional'' lecture style, where I made heavy use of this text in
discussing the basics of symmetric and public cryptosystems, and
security protocols. During that time, I assigned additional reading
and exercises from drafts of this book. In the second phase, I let
student teams ``implement'' various standards (e.g. SHA-1, DSA, DSS,
and triple-DES) in a language of their choice. In the third phase,
students had to make use of the more advanced part of this text or
consult online resources to identify papers and/or tools they chose to
present in class. Student feedback regarding these three phases,
their mode, and contents was extremely positive. Generally, people
felt that the implementation work helped them solidify the
mathematical underpinnings of the utilized techniques.
The supplementary material of this text is collected on the web
site
In the past ten years, the dramatic growth of the internet has had a
profound and lasting impact on the way in which organizations and
individuals communicate and conduct their public and private
affairs. Tax forms are available online, students may submit their
exams electronically to a, possibly remote, campus network, and
companies may use the internet as a public channel for linking up
internal computing facilities or processes; e.g. an employee may dial
into a company's intranet from a hotel room, or her home, through a
public internet service provider. Since the internet protocol in and
of itself does not provide sufficient mechanisms for ensuring the
privacy, authenticity, integrity and (if desired) anonymity of data
that are processed through a usually dynamically determined chain of
computers, there is a need for tools that guarantee the
confidentiality and authenticity of data as well as that of their
communication sources and targets. Cautious consumers of mobile or
foreign code prefer to verify that downloaded programs, such as Java
applets, abide by a formal set of safety rules, possible defined by
the individual consumer. These needs appear to be even more pressing
in the recent evolution of electronic commerce, where the
actual act of selecting and purchasing a product happens online.
While online companies are still waiting to reap their first real
profits, it is evident that companies at large need to offer this mode
of business in order to survive in a new economy which is global and
strengthens regional identity at the same time.
The design and analysis of cryptographic systems, security protocols,
and programs that process secret or confidential information and the
safety analysis of, possibly foreign, code, are important tools for
establishing a sufficient level of security and confidentiality
between human agents, social groups, and machines that communicate
over a public, and therefore untrusted, medium. Alas, current computer
science and information-technology degree programs typically only
touch upon these topics in a course on operation systems or
telecommunication systems within the larger context of ``computer
security''. As more and more working computer professionals are
actively confronted with the use, maintenance, or customization
of cryptographic components and program certification mechanisms, I see
a pressing need for a textbook, aimed at the advanced undergraduate
and beginning graduate level, that teaches ``what every computer
scientist ought to know about cryptographic systems, security
protocols, and secure information flow in programs''. This book
presents public-key cryptosystems, stream and block ciphers, certain
secure communication protocols, etc that are usually covered in
similar texts. However,
this text distinguishes itself, and goes
beyond most existing books, in several important ways:
and includes the Java source code of some of the programs featured in this text; and links to research papers, repositories, tutorials, public and private standards, articles, and companies that promote their security products. This site also features a current list of errata for this text. Readers are kindly asked to report errors not found in that list to huth@cis.ksu.edu.