Protocol Analysis

Question 1

What is known as a Dolev-Yao intruder?

Answer 1

Consider a public key system in which for every user X, there is a public encryption function Ex, which may be used by any user, and a private encryption function Dx, which only X may use.

A Dolev-Yao intruder is a thought experiment where we consider an intruder on a network that:
..exists as a user,
..can use any user’s public encryption function Ex,
..and may encrypt any message with its own private encryption function Dz.

Question 2

What are Dolev-Yao closures?

Answer 2

Dolev-Yao closures are a mathematical proof operation used to test the security of network protocols.

We consider a set of terms M, and define DY(M) as the least closure of M, where DY(M) is information the intruder can trivially compute starting from an initial set of known data M.

Question 3

What does the axiomatic rule of a Dolev-Yao closure represent?

Answer 3

The axiomatic rule states that given a message m, if the intruder knows m and m itself, we still know m.

It represents the idea that an intruder may derive or maintain knowledge about data it has intercepted.

Question 4

What does the algebraic rule of a Dolev-Yao closure represent?

Answer 4

The algebraic rule states that the intruder may compute an algebraic expression consisting of values they know.

It represents the idea that an intruder may be able to manipulate or composite messages they have seen in the past.

This may be used in order to shift around variables - for example, turning exp(exp(x, y), z) into exp(exp(x, z), y).

Question 5

What does the composition rule of a Dolev-Yao closure represent?

Answer 5

The composition rule states that the intruder may compute any function within the logical model of a set of values they know.

In other words, if the intruder knows a function, it may use that function.

Question 6

What does the projection rule of a Dolev-Yao closure represent?

Answer 6

The projection rule states that the intruder, given a pair of values {x, y}, may separate x as a single atomic fact.

In other words, given a pair of values, we know one of them.

Question 7

What does the decryption of symmetric rule of a Dolev-Yao closure represent?

Answer 7

The DecSym rule states that if the intruder knows a symmetrically encrypted ciphertext, and the key used to encrypt it, they can find out the corresponding plaintext.

Question 8

What does the decryption of asymmetric rule of a Dolev-Yao closure represent?

Answer 8

The DecAsym rule states that if the intruder knows a public key encrypted ciphertext, and the corresponding private key, they can find out the corresponding plaintext.

Question 9

What does the open signature rule of a Dolev-Yao closure represent?

Answer 9

The OpenSig rule states that if the intruder knows the signature of a message digest, they can compute the message digest.

Question 10

What are agents in a protocol?

Answer 10

An agent is a software module that carries out a role placed on it by the network protocol in use.

Question 11

What is a role in a protocol?

Answer 11

A role is a set of instructions to be carried out by an agent on the network when executing a network protocol.

Question 12

What is a nonce in protocol design?

Answer 12

A nonce (number used once) is a unique number randomly generated by an agent to prove the freshness of a message.

Question 13

What could go wrong if we use a nonce that is not freshly generated?

Answer 13

A non-fresh nonce opens up the protocol to attacks via replay, where an attacker waits for a certain gap in the protocol, then sends the message.

Normally, a nonce solves this, by ensuring that the communication is fresh. However, if the nonce is not always updated, a keen intruder may simply replay an older message and convince an agent that they are someone they aren’t.

Question 14

Why do we encrypt our messages?

Answer 14

As seen in Scenario, Version 1 in 10 - Protocol Design:

Without using encryption, the intruder can merely intercept the message and read the message in plaintext.

Question 15

What is a nonce used for?

Answer 15

As seen in Scenario, Version 4 in 10 - Protocol Design:

Without a nonce, protocols become susceptible to replay attacks, where the intruder simply waits for a bit before “replaying” the same message later, allowing them to reinitiate conversation as “Alice” and update or retransmit their keys, when they are in actuality the intruder.

Question 16

How may we stop an intruder pretending to be someone they aren’t?

Answer 16

One way we may do this is by including the agent that sent the message within the encrypted “walls”, so to speak.

This way, if an intruder has ever intercepted the message, the sender or recipient will be able to tell, as the agent will be modified.

Question 17

What is a common protocol attack that means “to intercept and relay the communication, taking data while it has it”?

Answer 17

Person/Man-in-the-Middle

Question 18

What is a common protocol attack that means “to reuse parts of previous messages”?

Answer 18

Replay

Question 19

What is a common protocol attack that means “to pretend to be another principal”?

Answer 19

Masquerading

Question 20

What is a common protocol attack that means “to send transmitted information back to its sender”?

Answer 20

Reflection

Question 21

What is a common protocol attack that means “to take advantage of normal protocol responses as encryption and decryption services”?

Answer 21

Oracle

It means to use a sort of ‘Oracle’ like a weakness or a software as a way to test how close the attacker is to breaking the protocol, sort of like a side-channel attack.

Question 22

What is a common protocol attack that means “to use messages in a different context than intended”?

Answer 22

Binding

Question 23

What is a common protocol attack that means “to substitute a different type of message field”?

Answer 23

Type Flaw (e.g. Heartbleed)

Question 24

What is the Halting problem?

Answer 24

The Halting problem is a problem that asks whether it is possible, given a program P, to write a function halt(P, x) which determines if P for a specific input x terminates or not.

The Halting problem is famously undecidable, meaning that it cannot possibly exist, but cannot be refuted otherwise.

Question 25

Why is the creation of an automated verification tool considered undecidable?

Answer 25

Because the state space is infinite.

This is due to many reasons, including:
..the intruder’s ability to create arbitrarily complex messages
..the lack of a bound of the number of executions on the protocol
..or the infinite number of nonces generated in an unbounded number of sessions.

Question 26

What are implicit and explicit destructor rules?

Answer 26

Destructor rules are rules that state that the intruder has the ability to “destruct” or decrypt any encrypted message it intercepts - like DecAsym or DecSym.

An implicit rule may be represented like it is in the Dolev-Yao closure, where we have data above the line and inferred data below that line.

An explicit rule is one where we explicitly define the closure as an algebraic sequence. e.g. {{m}_k}_inv(k) = m

Question 27

What is Alice and Bob notation?

Answer 27

Alice and Bob notation aims to make it easy to translate message charts into text-based syntax.

Alice and Bob notation is most “”"”famously”””” used in verification tools like OFMC.

Question 28

What is a protocol?

Answer 28

A protocol is a set of rules that determine the exchange of messages between two or more principals.

Security protocols, in particular, use cryptographic mechanisms to achieve security objectives, such as entity or message authentication.

Question 29

How do you break the Needham-Schroeder protocol?

NSPK:
A -> {NA}_pk(B)
B -> {NA, NB}_pk(A)
A -> {NB}_pk(B)

Answer 29

An intruder Eve can break the NSPK by intercepting the first message and acting as Alice. Bob will encrypt the message for Alice, but when Alice tries to send NB back to Bob, she will encrypt it with Eve’s public key instead, allowing her to find out Bob’s nonce.

Eve can then carry on using that nonce to read unintended messages.

Question 30

How can you fix Needham-Schroeder?

Answer 30

A fix to NSPK is called Lowe’s fix, where Bob simply has to respond saying that he is Bob.

Instead of {NA, NB}_pk(A)..
..we send {NA, NB, B}_pk(A).

Alice can then be sure that the message being sent is definitely from Bob.

This result is now colloquially called the Needham-Schroeder-Lowe protocol.