Lecture 6 (20 October, 1997) part 2

Scribe: Hiroaki Kikuchi

Formal Methods

1. Overview

The goal is to understand some previous works toward formal models using security protocol. Since all of these protocols is going to be sufficient, we make clear what limitations are in these protocols.

The secondary goal is to give the semantics of formal models. Last time we looked at the BAN logic from syntactic point of view. We learn a particular algebraic way to determine a given protocol is secure, and a way based on state machine to analyze security protocols.

Here is a list of approaches.

Dolev-Yao
Abadi-Tuttle
Others
- Meadows
- Heintze-Tygar
- Woo-Lam

2. Dolev-Yao: Algebraic Approach

Read "On the security of Public Key Protocols (IEEE Trans on Information Theory, 1983)" for details.

2.1 Overview

Approach: algebraic

Operations of principals and intruder (Z) are modeled by strings and examined in an algebraic way of the strings.

Protocols

Based on public key cryptography.

Ping-pong: two parties

Cascade protocol
Name-stamp protocol

Property

This approach determines whether a given protocol is "secure" or not. Where, "secure" means secrecy.

Efficient algorithms for checking is presented.

2.1.1 Public key Encryption Review

E_x	Encryption function for user X
D_x	Decryption function for user X

We assume a perfect public key encryption with a secure public-key database which contains all (X, E_x) pairs.
While, D_x is known only to X.

E_xD_x = D_xE_x = 1
knowing E_x(M) and the public directory does not reveal anything about the value of M.

2.1.2 Example 1

We assume that an active saboteur can impersonate another user, intercept and alter messages.
Consider the following ping-pong protocol. A -> B: (A, E_B(M), B)
B -> A: (B, E_A(M), A) This can be broken by an intruder Z by intercepting the first message and cheating A as follows;

A -> Z(B): (A, E_B(M), B)	% Z intercepts message from A
Z -> B: (Z, E_B(M), B)	% Z sticks Z in for A
B -> Z: (B, E_Z(M), Z)	% B follows its protocol
Z: decrypts E_Z(M) to get M

2.1.3 Example 2: variation of Needham-Schroeder

One way to overcome the attack is to encode the name of the sender together with the message.

a. A-> B: (A, E_B(MA), B)

b. B-> A: (B, E_A(MB), A)

(This will be proved to be secure.)

2.1.4 Example 3: Extra encryption is not always a good idea

a. A->B: (A, E_B(E_B(M)A), B)

b. B->A: (B,E_A(E_A(M)B), A)

It easy to break in the following way:

1. B->Z(A): (B,E_A(E_A(M)B),A)	% Let M' = Ea(M)B
	% Z extracts E_A(M')
2. Z->A: (Z, E_A(E_A(M')Z),A)	% Z starts protocol with A
3. A->Z: (A, E_Z(E_Z(M')Z),Z)	% A responds accordingly.
	% Z now has E_z(M').
4. Z->A: (Z, E_A(E_A(M)Z),A)	% Z starts protocol with A again
5. A->Z: (A, E_Z(E_Z(M)Z),Z)	% A responds accordingly.
	% Z discovers M.

2.1.5 Summary of Dolev-Yao Results

Here is a summary of the results obtained in this approach.

1. Cascade Protocols (like Example 1) are secure iff

the messages transmitted between X and Y always contain some layers of encryption functions E_x or E_y.
in generating a reply messages, each participant A (=X, Y) never applies D_A without also applying E_A.

2. Name-stamp protocols (like Examples 2 and 3): There is polynomial-time (O(N⁸)) algorithm for checking whether it is secure.

2.2 Cascade Protocols

In the cascade protocols, the users employ only encryption-decryption operations.

2.2.1 Notations

Two parties, X and Y: - X does strings of E_x, E_y and D_x.
- Y does strings of E_x, E_y and D_y. A protocol is a series of strings of what X does and of what Y does: 1. X->Y: (what X does) M
2. Y->X: (what Y does)₁ (what X does)₁ M
3. X->Y: (what X does)₂ (what Y does)₁ (what X does)₁ M
....
Let G be a string of operators over E_s and D_s: G is the reduced form of G after applying algebraic laws: E_xD_x = D_xE_x = 1 _{(In original paper, G is expressed by over-line.)}

For example, consider the protocol:

(what X does) = E_yD_x
(what Y does) = E_xD_yE_xE_xD_y Protocol:

X->Y: E_yD_x M
Y->X: E_xD_yE_xE_xD_yE_yD_x M	% or simply E_xD_yE_xM

Then, the reduced forms of N_i(X,Y) (i = 1,2,...,t) are given as follows: N₁(X,Y) = E_YD_X
N₂(X,Y) = E_xD_yE_x Where, N_i() is a set of symbols which contains all possible encryption and decryption functions executable since i-th step. For example, N₁(X,Y) is {E_x, E_y, D_x}.

2.2.2 Definition of Secure

Let S* be the set of all finite sequences composed of symbols in S.
Define S(Z) = E cup {D_z}
S₂ = all string of what X does
S₃ = all strings of what Y does Where E is the set of all E_A, and "cup" is an operation to mean an union of two sets.

A protocol is insecure
if there exists some sting G in (S(Z) cup S₂ cup S₃)* such that

G N_i(X,Y) = empty string for some N_i(X,Y). A protocol is secure otherwise.

2.2.3 Example

Consider Example 1, again. A -> B: (A, E_B(M), B)
B -> A: (B, E_A(M), A) These normal operations are represented by: E_XD_YE_YM We know it is breakable in the following attack:

A -> Z(B): (A, E_B(M), B)	% Z intercepts message from A
Z -> B: (Z, E_B(M), B)	% Z sticks Z in for A
B -> Z: (B, E_Z(M), Z)	% B follows its protocol
Z: decrypts E_Z(M) to get M

The behavior of intruder is given by simple string Intruder: D_zE_zD_yE_yM = M This means there exist a string G in (S(Z) cup S₂ cup S₃)* such that D_zE_zD_yE_y = empty string.

2.3 Name-Stamp Protocols

In this model, principles are allowed to some operations such as addition or deletion in addition to encryption-decryption operations.

2.3.1 Overview

Let G be string such that G = head(G)tail(G), where tail(G) is a suffix of m bits.

A user Y can do any of these operations to a string G

a. encrypt E_x
b. decrypt D_y
c. append i_x:	i_x G = GX
d. name-match d_x:	d_x G = head(G) if tail(G)=x
e. delete d:	dG = head(G)

In this model, we have the following algebraic laws:

E_xD_x = D_xE_x = 1
d_xi_x = di_x = 1	% but i_xd_x is not equal to 1

2.3.2 Definition of Secure

Define S(Z) = {E_A, i_A, d_A, d | all A} cup {D_z}
S₂ = all strings of what X does (including new operations)
S₃ = all strings of what Y does (including new operations) A protocol is insecure if there exists some string G in (S(Z) cup S₂ cup S₃)* such that G N_i(X,Y) = empty string for some N_i(X,Y).
A protocol is secure otherwise.

2.3.3 Examples

Example 2: a. A->B: (A, E_B(MA),B)
b. B->A: (B, E_A(MB),A) It is represented by: N1(X,Y) = E_Yi_X
N2(X,Y) = E_Xi_Y There is no string to resolve empty string. Therefore, this protocol is secure.

Consider Example 3 again. It has the following sets of strings.

alpha(X,Y) = E_Yi_XE_Y
beta(X,Y) = E_Xi_YE_XD_Y d_XD_Y
beta(Z,X) = E_Zi_XE_ZD_Xd_XD_X Then, the attack is formalized in the following way:

GN2	= D_zdD_z E_zi_xE_z D_xd_zD_x E_xi_zd D_zdD_z E_zi_xE_z D_xd_zD_x E_xi_z E_xi_yE_x
	= D_zd i_xE_z D_xd_z i_zd D_zd i_xE_z D_xd_z i_z E_xi_yE_x
	= D_z E_z D_x d D_z E_z D_x E_xi_yE_x
	= D_x d i_yE_x
	= D_x E_x
	= empty string

3. Abadi-Tuttle: State Machine

Read "A Semantics for a Logic of Authentication (Proc. of ACM Symp on Principles of Distributed Computing, 1991)" for details.

3.1 Overview

It is "Standard" state machine model of distributed systems. It has constructs driven by what is needed to model in BAN logic
The meaning is based on possible world semantics a la Hintikka [1962] and logics of knowledge and belief.
It does not handle multiple runs of a protocol.

3.2 Model of Computation

Principals: P₁, .., P_n each with - local state
- a set of actions (state-transition relation that can change only P_i's local state and P_e's state.
- a local protocol, A_i, a function form P_i's local state to the next action P_i is to perform.
Special principal P_e: the environment
Global state: = (s_e, s₁, ...,s_n)
Protocol: = (A_e, A₁, ..., A_n)
run: = infinite sequence of global states
(r,k): = k-th point in time in run r (k an integer) - r(k) = global state at time k in run r
- r_i(k) = local state of P_i at time k in run r
- r(0) indicates first state of the current epoch (the first state of the current authentication). Call it the initial state.
- system = set R of runs (typically the set of executions of a given protocol)

3.3 State Variable

- For each Pi
- local history - sequence of all action Pi has ever performed - key set
- For P_e
- global history - sequence of actions any principal has ever performed - key set
- message buffers, one per P_i containing all messages sent but not yet deliver to P_i

3.4 Set of Actions per Principal

send(m,Q): This denotes Ps' sending of the message m to Q. Add m to Q's buffer.
receive(): This denotes P's receipt of a message, nondeterministically chosen from P's message buffer.
newkey(K): This denotes P's coming into possession of a new key. Adds K to P's key set.

- Each action also adds itself to local and global histories.
- Tag receive(m) by m for local and by m and P for global.

3.5 Syntactic Restriction on Runs

A principals key set never decreases.
A message must be sent before received.
A principal must possess keys it uses for encryption.
A system principal (not P_e) sets from fields correctly.
A system principal (not P_e) must see messages it forwards.

3.6 Semantics to Logic

Fix system R, and fix an interpretation I of primitive propositions that maps each p in Phi to set of points I(p) in R at which p is true.
By the induction of the structure of T, we define truth of T at (r,k), denoted (r, k) |= T We define (r,k) |= p iff (r,k) in I(p) for primitive p in Phi,
(r,k) |= T AND T' iff (r,k) |= T and (r,k) |= T'
(r,k) |= ~T iff (r,k) not |= T _{(Where "AND" and "~" are logical operators. Some symbols
are represented in different way to the original)}

Seeing: (r,k) |= P sees X
iff for some message M, at time k in r
1. receive (M) appears in P's local history, and
2. X in seen-submsgs_K(M), when K is P's key set.
Saying: (r,k) |= P said X
iff for some message M, at some time K' in r
1. P performs send(M,Q), and
2. X in said-submsgs_k,m(M), where K is P's key set and M is the set of messages P has received.
Jurisdiction: (r,K) |= P controls Phi
iff (r,k') |= says Phi implies (r,k') |= Phi for all K' greater than 0
Freshness: (r,k) |= fresh(x)
iff X is not in submesgs(M(r,0))
Shared keys: (r,k) |= P <-k-> Q

3.7 Possible Worlds Semantics

In any given world (at any point in time), a principal P considers a number of other world to be possible.
A world (point) is possible if the two points are indistinguishable to P, meaning that P has the same local state at both points.
This definition gives the standard possible worlds definition of knowledge.

3.8 Difference between logics of Knowledge and Belief

Knowledge logics have axiom: (P knows T) implies T Belief logics do not have the axiom: (P believes T) implies T P can believe in something (K is good) at the current point but where at a different point, indistinguishable to P (K still looks good to P), that something is not true (a malicious environment stumbled upon K so K is not really good).

According to [BAN89], knowledge and belief logics are incomparable.

- Erroneous initial beliefs are certainly not knowledge.
- Each principal knows all tautologies, but does not necessarily believe them.

3.9 Possible Worlds Semantics for Belief Logics

For BAN belief, the points a principal considers possible are those points of good runs that the principal considers indistinguishable form the current point after hiding the encrypted messages.

A good run is one in which initial beliefs are initially true.

4. Other Models

4.1 Meadows (NRL Protocol Analyzer)

It is based on Dolev-Yao term rewriting.
Protocol is specified as rules generating words in a term algebra. Model of computation is more similar to Abadi-Tuttle. It defines change-set instead of newkey.
The key sets can grow and shrink. Hence, it is non-monotonic logic.
It can explicitly model multiple simultaneous runs.

4.2 Heintze-Tygar

See N. Heintze and J. Tygar. "A model for secure protocols and their compositions. (IEEE Transactions on Software Engineering 1996)"

Model of computation is more general than Abadi-Tuttle

- nondeterministic communicating state machines, trace semantics
- partial order of events (no global clock; events are asynchronous).
- beliefs and nonces can expire

4.3 Woo-Lam

See T. Woo and S. Lam. "A semantic model for authentication protocols. (IEEE Symposium on Security and Privacy, 1993)

Syntax of protocols in terms of terms (as in Dolev-Yao)
Semantics in terms of state machines

- global and local states, state transitions, executions
Addresses not just secrecy, but correspondence
- the execution of the different principals proceeds in a look-step fashion
When an authenticating principal finishes its part of the protocol, the authenticated principal must have been present and participated in its part of the protocol. - want to assure that the authenticating principal is indeed "talking" to the principal it has in mind.