Educational Outcomes for CSE 774
This is an analytical course that uses predicate
calculus, higher-order logic, and specialized logical systems to describe,
specify, and verify the correctness and security properties of network
security protocols, algorithms, and implementations. Areas that are rigorously
analyzed using formal logic include cryptographic algorithms, key distribution
protocols, delegation, access control, electronic mail, and networks of
certification authorities.
The specific educational outcomes at several levels
of knowledge are:
Comprehension
You will be able to:
-
Define the meaning of security services such as confidentiality, integrity,
non-repudiation, and authentication.
-
Describe the characteristics of private key and secret key cryptographic
systems.
-
Describe cryptographic algorithms for encryption, hashing, and signing.
-
Describe cryptographic protocols for session-based security such as Kerberos,
and store-and-forward security such as Privacy Enhanced Mail.
-
Describe basic principles of trust topologies and networks of certification
authorities.
Application
-
When given a block diagram or functional description of an implementation,
you should be able to represent the implementation using predicate calculus.
-
When given protocol descriptions and trust hierarchies, you should be able
to use specialized security calculi such as the logic of authentication
for distributed systems to describe the protocol and trust relationships.
-
When given a trust topology, determine the necessary certificates for establishing
trust in a key.
Analysis
-
When given a set of assumptions and a security goal to prove, you should
be able to prove, using formal inference rules, if the security goal is
true or not.
-
When given a set of certificates, you should be able to formally derive
whether a key is associated with a particular principal.
Synthesis
-
When given a description of a system or component and its specification
and security properties, you should be able to construct a theory that
describes both, and show if the security properties are supported.
-
When given a description of a trust topology, you should be able to create
a formal description of the certificates and trust relationships for the
certification authorities.
Evaluation
-
When given a theory, inference rules, and a proof, you should be able to
judge if the proof is correct.
-
When given a specification and implementation, you should be able to judge
whether the implementation satisfies its specification.
Back to Table of Contents