Advanced cryptography: Symbolic methods for security analysis

Instructor:Daniele Micciancio

Cryptographic Protocols

The invention of public key cryptography in the mid 70's attracted the attention of many researchers that recognized the importance of cryptographic techniques in securing distributed computer applications. Following the publication of [DH] and [RSA], there was an outburst of cryptography papers suggesting the use of (both symmetric and public key) cryptographic functions to address a variety of security problems arising in distributed computer applications. At first encryption and decryption was performed right before or after sending or receiving a message, and we even find proposals to locate the (hardware or software) implementation of the cryptographic functions on the network interface card. However, people came pretty soon to the realization that cryptographic functions can be put to use in more creative ways to design security protocols that do more than just sending or receiving messages in encrypted form. For example, one can use cryptography to store sensitive information in encrypted form on insecure media, forward ciphertexts to other parties without necessarily knowing the encryption/decryption key, etc.

One of the earliest papers in cryptographic protocol design is

[NS] Needham, Schroeder. Using encryption for authentication in large networks of computers, CACM 21(12):993-999 (1978)

This paper, which followed almost immediately the publication of [RSA], proposes several protocols based both on symmetric and asymmetric cryptography, some of which were the basis for the development of subsequent work, e.g., the Kerberos authentication protocol. Informally, the security goals addressed by the protocols in [NS] are:

1. Establishment of authenticated interactive communication. This is similar to initiating a conversation over the phone: after few greeting messages, both parties know who they are talking to.
2. One-way authentication. This is similar to the mail system, and provides for authenticated (one way, non interactive) communication in situations where both parties cannot be available at the same time.
3. Signed communication. The difference between (3) and (2) is that (3) has a nonrepudiation feature, by which the recepient can prove to a third party that the message originated from the claimed sender.

All definitions are very informal, but the paper brings up several important issues in the design of authentication protocols:

• The adversary attacking a network protocol can do more than just listening and try to decipher messages. It can actively interfere with the execution by interposing in all communications, eavesdropping, altering, dropping, duplicating, rerouting, or rearranging messages. This paper explicitly proposes an execution model with an active adversary.
• Achieving authenticated communication in the presence of active adversraries in a large communication network is not a simple problem, and requires carefully designed protocols. Encryption is a basic tool for the construction of protocols, but it needs to be used properly in order to achieve the security goal.
• One can design protocols based on either symmetric key cryptography, or public key encryption, still achieve a common security goal. For example, [NS] describes a protocol to emulate digital signatures using symmetric cryptography using the help of a trusted third party. Security goal can be (and should be) defined independently from the underlying techniques used in the solution. E.g., it does not make much sense to require, as a security goal, that all communications be encrypted. (E.g., the security goal may be to achieve privacy, but if messages are encrypted under a key known to the adversary, then communication is not private.)
• Recognize the need for techniques for the verification and analysis of security protocols. The authentication protocol described in [NS] has been subsequently used as a test case for many formal methods for security analysis. The paper concludes by saying that "protocols such as those developed here are prone to extremely subtle errors that are unlikely to be detected in normal operation. The need for techniques to verify the correctness of such protocols is great, and we encourage those insterested in such problems to consider this area."

Cryptographic operations and messages

The protocols described in [NS] employ the following kinds of operations and primitives:

• Encryption: E_k(m) , also written {m}_k. Represents the encryption of m under key k. Encryption is assumed to have nonmalleability and binding properties, i.e., it is hard to change E_k(m) into the encryption of a related message E_k(m) without knowing the decryption key. Similarly, encryption can be applied to compund messages E_k(m1;m2;m3), and computing E_k(m1;m2;m3) from the encryption of the components E_k(m1), E_k(m2), E_k(m3), or vice versa, requires knowledge of the decryption key.
• Decryption: D_k(c). This operation is often represented implicitly, by specifying that a party received the message {m}_k. Formally, this means that the party receives a ciphertext, attempt to decrypt it using key k (or its private counterpart for the case of public key cryptography), and set m to the result of decryption. If decryption fail, the party will detect the error and abort. Parties can still receive ciphertexts c=E_k(m) without knowing the decryption key. The party can still forward the ciphertext to somebody else, but cannot check that c has the propert form, i.e., it is the encryption under k of a message with a specific structure.
• Identities: A,B ,.... It is assumed that every party has a unique name, which can be used for identification and routing. Naming is an important component of authentication protocols. How can you claim you know who you are talking to, without knowing their name? Stat rosa pristina nomine, nomina nuda tenemus.
• Nonces: n1, n2, .... These are typically implemented as random numbers and are used to prove freshness of messages. E.g., if I pick a numner n at random from a large set, then any message that contains n must have been composed after I first transmitted n.

In general, it is possible to describe the set of possible messages sent by this and similar protocols using formal expressions built up from identifiers, nonces and keys, using concatenation and encryption operations. This gives a precise formal syntax to describe protocol messages. We will get back to this later in the course.

Protocols

We concentrate on the symmetric key protocols of [NS], as the asymmetric cryprography protocols of [NS] are strightforward application of public key cryptography.

NS Symmetric Key Authentication

There are three parties: A, B and S, where A wants to establish a secure channel with B with the help of the server S. The server shares a key ka, kb, etc. with every player in the network. The protocol goes as follows:

1. A -> S: (A,B, na)
2. S -> A: {na, B, k, {k, A}_kb}_ka
3. A -> B: {k,A}_kb
4. B -> A: {nb}_k
5. A -> B: {nb'}_k

where na, nb are nonces chosen at random by A and B, nb' is a modified version of nb (e.g., nb - 1) such that {nb'}_k cannot be easily computed from {nb}_k without knowing k, and k is a random key chosen by S. Informally, the security of the protocol can be argued as follows:

1. A tells S that she wants to talk to B, and include a nonce na to identify its request
2. S replies to A encrypting its response under ka so that A is assured the message came from S. (This is because ka is known only to A and S, and A didn't send the message. When two people are in the elevator, and one farts, everybody knows who did it.) The message from S includes the query identifier na and intended respondent name B. These are both necessary for the following reasons: if na is not included, then the adversary may replay an old message and let A use an old key, even worse if B is not included the adversary can change B to C in message (1) and let A talk to C without knowning it. The message also includes a fresh key to be used by A and B to authenticate and communicate, and an undecipherable ciphertext c = {k,A}_kb (the "ticket" using Kerberos terminology) to be forwarded to B
3. A recover and forward ciphertext c to B. Since the ciphertext is encrypted under key kb (shared by S and B), B can decrypt it and be assured that the message comes from S. At this point both A and B know the secret key k. The ticket c included A's name beside the key k so that B knows who he is talking to.
4. The last to messages are a handshake used to verify that the key was successfully distributed and the key is fresh. The server S is trusted to choose a fresh random key k for any request, so A knows that the key k is fresh because of the nonce na. However, from B's point of view, message (3) might be a replay from a previous interaction containing an old key. In order to avoid this, B will interact with A to make sure the key k he just received is currently being used by A. Specifically, B sends a nonce nb as a random challenge to A. This also proves to A that B received the key, as A, B and S are the only parties that can possibly know k, and S is trusted not to use k for encryption.
5. A decrypts, modifies, reencrypt and transmit the challenge to B to prove that she knows the key and she knows that B knows the key.

Remark: that the NSSKA protocol has the following property: the key k is used in two stages

1. Steps 1,2,3: Key distribution stage, during which k is used as a message, but not as an encryption key
2. Steps 4,5: Key deployment stage, during which k is used to encrypt, but not as a message

This is a common scenario in key distribution protocols, and we will see later in the course that this two-staged usage of keys can play an important role in the computational analysis of cryptographic protocols.

Protocols and local programs

The protocol is described by a sequence of messages, namely the messages exchanged by the parties when no adversary is present. The protocol implicitly represents a set of programs run locally by A, B and S. The programs represented by the above protocol are:

Initiator(A,B,S) (This is the program invoked by A to initiate communication with B with the help of server S):

1. Choose random nonce na, and send (A,B,na) to the server S.
2. Wait until a message c is received from S, and try to decrypt c using the shared key ka.
3. If decryption is successful, and D(ka,c) = (na,B,k,c') for some k and c', send c' to B. Otherwise abort the protocol.
4. Wait until a message c'' is received from B
5. Attempt to decryption using k: D(k,c'') = m. If decryption is successful send E(k,m') to B.

Responder(B,S) (Notice that the responder does not know the identity of the initiator.)

1. Receive a message m (from A)
2. Try to decrypt m under kb and D(kb,m) = (k,A), do the following (otherwise fail)
3. Choose random nonce nb and send {nb}_k to A
4. Wait for another message m' from A, try to decrypt with k and check if D(k,m') = nb'

Server(S)

1. Accept messages of the form (A,B,n)
2. In response to (A,B,n), choose a random key k, and send {n,B,k,{k,A}_kb}_ka to A.

The distinction between protocol description and programs is very important in the context of security. In the real world, only local programs exit and are run by the parties. Since the adversary is active, there is no guarantee that the programs will interact as described by the protocol. The protocol language is a convenient way to represent several programs at the same time, and it gives a clearer picture of how the different programs interact. However, you should keep in mind that the protocol is just an implicit description of a set of programs which will be run in an adversarial environment.

NS Symmetric key "signatures"

[NS] proposes an interactive protocol based on symmetric cryptography that achieves a goal similar to digital signatures. The interaction is only between parties and a trusted server. The communication between the parties is unidirectional, from the signer to the signature recepient, as in public key signatures. The trusted party S is used to produce and verify signatures. The protocol described in [NS] considers the common practice of hashing the message to be signed to a short digest to which the signature algorithm is applied. Here for simplicity, we skip the hashing function, and consider the direcly the digest as the message to be signed.

There are three parties A (signer), B (recepient), and S (trusted server). A and B shares keys ka and kb with S. These keys are used to securely communicate with S. S has also a key ks known only to S.

Since signatures are non interactive, we distinguish varius stages:

1. Signing:
   1. A -> S: A,{m}_ka
   2. S -> A: {A,m}_ks
2. Signature transmission:
   1. A -> B: m,{A,m}_ks
3. Signature verification:
   1. B -> S: B,{A,m}_ks
   2. S -> B: {A,m}_kb

As before, the protocol represents the description of various programs, run locally by A, B and S. The protocol is easily explained:

1. During the signing stage, A requests S to produce a signature for m on her behalf. The message m is sent to S encrypted under ka so that S is assured A really wants to sign the message. S replies with a "signature", consisting of the signer identity and the message combined and encrypted under S's secret key. A cannot verify that the signature is correct at this point, as signature verification requires interaction with S. (See stage 3.)
2. Signatures can be transmitted to any other party, together with the message being signed (this is not really important here because the message can be recovered from the signature, but it is crucial when the signature algorithm is applied to the hashing of the message).
3. B verifies the signature sending it to S, which decrypts it and reencrypt it under B's key. B can now recover (A,m), check that m is the (hash of the) right message, and A is the claimed signer identity.

Attacking the NS protocol

The following is an "attack" to the NS secret key authentication protocol pointed out in

[DS] Denning, Sacco, Timestamps in key distribution protocols, CACM 24(8):533-536 (1981)

The NSSKA protocol puts lot of care to ensure the session key k sent by S to A for communication with B is fresh. That's why A uses a nonce na in its first message, and checks that S's reply contains that nonce. The reason is that session keys are considered more susceptible to compromise for a variety of reasons: they are used to encrypt a much larger number of messages than the user secret keys, they may be shorter than user secret keys for efficiency reasons, a user may deliberately disclose a session key to open up a conversation when its content is no longer confidential, etc.

The secrecy of users private keys (shared with S) is necessary, as leakage of ka allows anybody to impersonate A. [NS] even considers as an extra security measure to protect identifying keys ka, kb: whenever a message m needs to be encrypted under ka, generate a temporaty (one-time) key and send ({t}_ka, {m}_t). This way, the adversary only gets to see the encryption of unknown random messages under ka, and potentially known messages m are encrypted under keys t that are used only once. On the other hand, for the session key k, the potential damage caused by key compromise is much smaller. Recovering k allows to decrypt the content of a specific (past) conversation, but it does not allow to impersonate A. Freshness of the key k is required, so that the key cannot be used to impersonate A when authenticating with B, and this is what the nonce na, and handshake {nb}_k, {nb'}_k is supposed to achieve.

[DS] considers a scenario where a past session key is leaked to the adversary, and show that the final handshake does not really guarantee the freshness of k. The attack is trivially simple:

1. The adversary intercept the ticket t = {k,A}_kb from a past communication, and subsequently recovers key k somehow.
2. At any time in the future (when k is not fresh anymore), the adversary impersonates A and successfully authenticates with B as follows:
   1. The adversary sends the old ticket t to B
   2. B decrypts t to recover k and A, and sends a random challenge {nb}_k to A.
   3. The adversary intercepts the message, decrypts it using k, and replies with {nb'}_k
3. After the interaction, B believes that A is currently using k, and can be used to securely communicate with A. The adversary can intercepts all messages, and produce replies encrypted under k. This is a break both to privacy (as B will reveal to the adversary information that was intended for A only), and authenticity (B will take the adversary's messages as coming from A.)

[DS] suggests to solve this problem using timestamps, i.e., including in the messages and tickets information about the time when the ticket was produced. This is not always convenient or possible because it requires a common clock available to all parties, and opens the protocol to the threat of subtle timing attacks that exploit small difference in the local clocks of the partecipants. The attacks can be avoided introducing some slackness and delays in the protocol, but this is not the best choice for security or efficiency.

A variant of the [NS] protocol without timers that addresses the same weakness pointed out in [DS] is suggested in

[OR] Otway, Rees. Efficient and timely mutual authentication, OS Review 21(1):8-10 (1987)

Both in [NS] and [OR] security is addressed only at a very informal level. No security proof of sort is given. In fact, there is not even a formal specification of the execution model and security claim, although one can probably be extracted somehow from the papers. The need for a formalization of adversarial execution models and security definitions is already recognized in [NS], but the first such formal model is presented only in the paper

[DY] Dolev, Yao, On the security of public key protocols, IEEE TIT 29(2):198-208 (1983)

which we will discuss next time. Reading assignments for the next couple of lectures include [DY] as well as the following related papers:

[DEK] Dolev, Even, Karp, On the security of ping-pong protocols, Inform.and Control 55:57-68 (1982)

[EG] Even, Goldreich, On the security of multi-party ping-pong protocols, FOCS 1983: 34-39

[EGS] Even, Goldreich, Shamir, On the security of ping-pong protocols when implemented using the RSA, CRYPTO 1985