�ݺ�ߣ

Formal Analysis of TESLA protocol in the Timed
OTS/CafeOBJ method

Petros Stefaneas

Lecturer
School of Applied Mathematics and Physical Sciences
National Technical University of Athens

Joint work with I. Ouranos (HCAA) and K. Ogata (JAIST)

Introduction

?Project: Explore the applications of Algebraic Specifications and
especially of behavioral specifications to modeling and verification of
different systems/protocols.
? This paper: How to model authentication protocols with timing
properties �C TESLA protocol (source authentication in multicast
settings).
? We have formally verified that basic TESLA protocol has desired
properties with CafeOBJ, an algebraic specification language/system.

Outline

? Formal Methods & Algebraic Specifications
? CafeOBJ algebraic specification language/system
? Timed Observational Transition Systems and CafeOBJ (TOTS/CafeOBJ
method)
? Timed Efficient Stream Loss-tolerant Authentication protocol (TESLA)
? Verified properties

Outline

? Modeling
1) Assumptions 2) Formalization of messages and network
3) Real time issues 4) Formalization of trustable principals
5)Formalization of the Intruder
? Verification
1) Formalization of Properties 2) Verification Outline
? Lessons Learned

Formal Methods and Algebraic Specifications

? Algebraic Specification Languages/Systems: Formal methods which
are based on mathematical logics/combination of logics.
? Algebraic Modeling/Verification: Describe a system and its desired
properties
1. Defining signature for a real problem
2. Expressing the problem in equations
3. Verify properties of the specification (design level)

Introducing CafeOBJ

? CafeOBJ is an algebraic formal specification language.
? CafeOBJ is a formal language for writing formal models and reasoning
about them with rewritings/reductions.
? CafeOBJ is a successor of OBJ and developed by an international
team in Japan.
? Related algebraic specification languages:
1. Maude (USA) �C Another successor of OBJ
2. CASL (Europe) �C Attempt of developing a common algebraic
specification language

Formal Models in CafeOBJ

1. Abstract data types (ADT) with tight semantics (e.g. integers)
? Initial algebra semantics
? Induction based reasoning
2. Abstract state machines (ASM) with loose semantics (e.g. objects)
? Coherent hidden algebra semantics
? Co �C induction based reasoning

�� CafeOBJ can provide unified specification style both for
static and dynamic systems ��

CafeOBJ Syntax and Notation

Two kinds of sorts:
? Visible sorts representing ADTs.
? Hidden sorts representing set of states of an ASM.
Two kinds of operations to hidden sorts:
? Actions that can change a state of an ASM (or object). Takes a
state and zero or more data and returns another or the same
state.
? Observations that are used to observe the value of a data
component of an object. Takes a state and zero or more data and
returns the value of a data component in the object.

CafeOBJ Syntax and Notation

Operator declaration:
? (action)
bop action_name : v_sort1 v_sort2 �� v_sortn h_sort h_sort
? (observation)
op observation_name : v_sort1 �� v_sortn h_sort v_sort

Operator definition with equations:
eq term1 = term2 .
In case of conditional equation:
ceq term1 = term2 if cond1 .

Observational Transition Systems

OTS S: A kind of transition system specified in terms of behavioural
specification. It consists of < O, I, T > such that:

Observational Transition Systems

An execution of S is an infinite sequence u0, u1,�� of states satisfying:

Timed Observational Transition Systems

Timed OTS S : OTS evolved by introducing special clock observers and
transition tickr to deal with timing.
Clock observers
1. now : Y R+. It serves as the master clock and returns the time
amount after starting the execution of S. Initially returns 0.
2. For each transition �� :
? l�� : Y R+. Returns the lower bound of ��.

? u�� : Y R+. Returns the upper bound of ��.
They are used to force �� to be executed between the lower and the upper
bound.


Clock transition tickr

Time advancing transition where r R+.
Effective condition: now(u) + r u�� (u), for a state u.

now(tickr(u)) = now + r if the effective condition holds in u.

Delays of ��

Functions d��min , d��max which give the minimum and maximum
delays of �� and have the same type as l��, u��. Their definition is as
following:

OTSs and CafeOBJ

OTSs are written in CafeOBJ to model distributed concurrent systems, as
following:

TOTSs and CafeOBJ

A TOTS is written in CafeOBJ as an OTS but we also need a module called TIMEVAL
that specifies non-negative real numbers and their properties.

Signature

TOTSs and CafeOBJ

Equations

Timed OTS /CafeOBJ

The method includes the following steps:
? A system is modeled as a TOTS.
? The TOTS is written in CafeOBJ.
? Properties to be proved are expressed as CafeOBJ terms.
? Proofs or proof scores showing that the TOTS has properties are written in
CafeOBJ.
? The proof scores are verified by executing them with the CafeOBJ system.

TESLA Protocol

? Source authentication protocol in multicast environments
? Although uses symmetric cryptography achieves asymmetric
properties
? Use of timing �C loose synchronization (real time
authentication)
? We are going to formally analyze basic TESLA using the
TOTS/CafeOBJ method

Basic TESLA

Init message: R S : nR
Reply message: S R : {f(k1), nR }SK(S)
Message 1: S R : d1, f(k2), MAC(k1,d1, f(k2))
Message n: S R : dn, f(kn+1), kn-1, MAC(kn,dn, f(kn+1), kn-1), n>1

? Node R sends a nonce to S (message init)
? On receipt of the init message, S obtains nR and sends it back encrypted with its
secret key along with a commitment to the key k1.
? After the initial authentication, S sends data packet d1, a commitment to the second
key f(k2) and a MAC which encrypts d1 and f(k2) with k1.
? Message n consists of the nth data packet, the commitment to the key that will be
used at the next encryption, the key that was used in the previous encryption and a
mac which encrypts dn, f(kn+1) and kn-1 with kn.

Basic TESLA

A receiver can authenticate the nth packet m when:
? the packet has been received
? either the packet is the digitally signed initial packet (Reply message),
or else the preceding packet m-1 and succeeding packet m+1 have been
received, and the following hold:
? applying the MAC function to the key revealed in m+1 and the
content (other than the MAC) of packet m yields a value equal to
the MAC component of m,
? the key revealed in m+1 is the committed to in m-1,
? m-1 can be authenticated and

Basic TESLA

Security Condition : ArrTm < Tm+1,

The receiver R will not accept packet m if it arrives after the sender might
have send message m+1, otherwise an intruder can capture message m+1 and
use the key kn from within it to fake message m.

Requirement: Loose Synchronization of agent��s clocks (real time property)

Invariant Property

A safety property of TESLA which is an invariant is:

��The receiver does not accept as authentic any message mi unless mi was actually
sent by the sender��

We are going to prove this very critical property of the protocol
using the TOTS/CafeOBJ method.

Modeling TESLA (Datatypes)

Assumptions made for data types
? The cryptosystem used is perfect.
? There exist an arbitrary number of trustable nodes
? There exist malicious nodes; the combination and cooperation of them is modeled
as the most general intruder:
- Eavesdrop any message flowing in the network
- Glean any quantity from the message; however, the intruder can decrypt an
encrypted text only if he/she knows the key to decrypt.
- Fake and send messages based on the gleaned info; however, the intruder can
encrypt and/or sign something only if he/she knows the key to encrypt and/or sign,
and cannot guess unknown secret values.


Formalization of Messages

op im : Receiver Receiver Sender Nonce -> Msg
op rm : Sender Sender Receiver Nonce Prf Sign -> Msg
op m1 : Sender Sender Receiver Data Prf Mac1 -> Msg
op mn : Sender Sender Receiver Data Prf Key Mac2 Int -> Msg

Suppose that a message denoted by
mn (p1, p2, p3, d, p, k, mc2, i)
exists in the network.
? It is true that p1 has sent the message to p3.
? If p2 is different from p1, then p1 is the intruder and the message has been faked
by the intruder.
? If p3 receives the message, p3 just believes that the message seems to come from
p2 but cannot check who has really sent the message.


Formalization of Messages (cont.)
The rest is the packet content.
For modeling reasons we have added the id of the packet varying
over an integer number as part of the packet.

All sorts used such as Receiver, Sender, Nonce, Data, Prf, Sign, Key, Mac1 and Mac2
have been specified beforehand and are used by the MESSAGE
module.


Formalization of the Network
? The network is modeled as a bag (multiset) of messages.
? Given the network (a bag of messages), data values available to the intruder are
determined.

Suppose that the message mn(p1, p2, p3, d, p, k, mc2, i)

exists in the network. The data values available to the intruder from the
message:
- d (data of the packet), p (encrypted commitment for key ki), k (key ki-1),
mc2 (MAC of the second type), and index i.

Modeling TESLA (System��s behaviour)

Assumptions made for modeling protocol��s behaviour
? Time constraints for sending �C receiving messages m1 and mn.
? Ordering of packets using an integer packet id (im and rm have id=0,
m1 has id = 1 and mn has id = n.
? One sender �C one receiver (Basic Scheme)
? Boolean flag-s is set to true if the sender has received the message im.
? Boolean flag-r is set to true if the receiver has sent the message im.
? Boolean received? Is used to check the reception of a message by the receiver.
Since the message is not deleted from the network, when received the boolean
is set to true in order not to be received again by the same receiver.
? Observation next returns the id of the packet to be received by the client.

Modeling TESLA (System��s behaviour)

Real time issues

? Security condition (see �ݺ�ߣ 22)
? Clock observers
? now(t) : returns the time at state t.
? l-sdm2 (t) (l-sdmn(t)): the lower bound of sending message m2 (mn) at
state t.
? u-rcvm1(t) (u-rcvmn(t)): the upper bound of receiving message m1
(mn) at state t.
? Constants
? init: initial state
? d1: the lower bound of sending a message mn
? d2: the upper bound of receiving message m1
? d3: the upper bound of receiving message mn.
with
d2 < d1, d3 < d1, d1 > 0, d2>0, d3 >0
? Transition
tick (t,r) advances the time by r time units at state t.

Modeling TESLA

Formalization of trustable nodes
? The network is modeled as a bag (multiset) of messages.
? Given the network (a bag of messages), data values available to the intruder are
determined.
? The behavior is modeled with 5 send and 4 receive transitions. Each transition
has effective condition with timing and non-timing part.
? Transitions with timing part are sdm1, sdm2 and sdmn.
Example
sdmn(t,m,J) corresponds to that: if a message m of type mn with id = J, J > 2 that
has been sent by server to client exists in the network, agent server makes
1. The data d(a, J+1) ,
2. The pseudorandom f(k(server, client, J+2))
3. The key k(server, client, J)
4. The MAC mac(k(server, client, J+1), d(server, J+1),f(k(server,client, J+2),
k(server, client,J))

and sends it in a message mn with the id J+1 of the message provided that
l-sdmn (t) <= now (t)

Modeling TESLA

Formalization of the intruder
? Tries to glean information from the messages flowing in the network,
? create and send messages based on it
? Gleaned quantities are nonces, data, commitments, keys, macs1, macs2,
signatures
? The intruder��s fake messages follow the format of the messages of the protocol.
There are 18 transitions model the behavior of an intruder.

Example
fkmn7(t,k,k��,k��,i) corresponds to that the enemy fakes
mn(enemy,server,client,d(enemy,i),f(k),k��,mac2(k��,d(enemy,i),f(k),k��),i) and puts
it into the network.

Verifying TESLA

Formalization of invariant property

The property that the original protocol satisfies and we want to prove for our model
(specification) is as follows:

��The receiver does not accept as authentic any message mi unless mi was actually
sent by the sender��
The above property is expressed based on our specification as three different
invariants:
?INV1: Whenever you receive the three messages rm, m1, m2 i.e.

then m1 originates from the claimed source S.
?INV2: Whenever you receive the three messages m1, m2, m3 i.e.

then m2 originates from the claimed source S.

Verifying TESLA

Formalization of invariant property
?INV3: Whenever you receive the three messages m_n-1, m_n, m_n+1, n >2 i.e.

then mn originates from the claimed source S.

Verifying TESLA

Verification Outline
? Proof by induction on the number of action operators applied (or transition
rules applied).
? Case analyses and lemmas also needed.
? In any case, proof scores are written in CafeOBJ and case analyses is done with
the aid of CafeOBJ system.
? Flexible human �C computer interaction in good balance, i.e humans make proof
plans and machines conduct detailed computations.

Verifying TESLA

Verification Procedure
?Write a CafeOBJ module called INV where is declared the invariants to prove
? Show that the predicate holds at any initial state
? Write a module ISTEP, where two constants t, t�� denoting any state and the
successor state after applying an action in the state, and the invariant to prove in
each inductive case is expressed in CafeOBJ terms
? Write a proof score for each case.
? For our proof we used 29 lemmas that we had to prove for our specification.
? Two invariants that include timing information are:
?inv8: If an original message mn exists in the network in a state T with n >1
and l-sdmn(T) = now(T) then the message has been already received by the
client.
?inv12: If an original message mn exists in the network in a state T with n >1
and it has not yet been received by the client , then u-rcvmn(T) < l-sdmn(T).

Lessons Learned

Algebraic Specification and Verification with
CafeOBJ
P C
R O
O N
S S
Can be difficult and time
Simple underlying theory �C
consuming for
based on equations
inexperienced user

Lessons Learned

Algebraic Specification and Verification with
CafeOBJ
T T
A A
S S
K K
System Description Property Description

Deep understanding of
the protocol/system

Lessons Learned

?Incorrect system��s specifications => unsuccessful verifications => specification
revisions => verification retries which can be time consuming
? In our case many verification retries and specification revisions were performed
due to misunderstanding of protocol��s functions that lead to wrong descriptions
ERROR 1:
? Protocol model without timing constraints, only by packet indexing
ERROR 2
? Wrong expression of the invariant property to prove
ERROR 3
? Less important protocol mis - description
RESULTS
? Counterexamples found during verification for our model

Proposals

? Some level of automation for Timed OTS method can be possible (Cr��me, Toolkit
proof score presenter for OTSs)
? Emacs and/or Eclipse make specification/proof score editing easier
? Library support for reusable similar modules can be useful.
? Combination of model checking and theorem proving can save time.

Thank you!
Petros Stefaneas, NTUA
petros @math.ntua.gr

�ݺ�ߣ

Isola 12 presentation

Recommended

More Related Content

What's hot (20)

Similar to Isola 12 presentation (20)

Isola 12 presentation