Transcript yang-10-16 - Computer Science and Engineering

Using State Space Exploration and a Natural
Deduction Style Message Derivation Engine to
Verify Security Protocols
By E. M. Clarke, et al.
Presented by Zhenxiao Yang
1
Outline




Introduction
Model Architecture
Evaluation of the Model
References
2 of 27
Introduction

What are network protocols


Why are we using FM to reason about
protocols?



principals + messages
Subtlety
Criticality
Main FM approaches being used


Belief logics and automated deduction process
Rigorous mathematical proof
3 of 27
Introduction – cont’d

Comparison between this paper and the
paper Ali presented


This paper focuses on the model itself,
versus the specification logic
This paper focuses on common security
protocols, versus e-commerce protocols
4 of 27
Model Architecture
5 of 27
Assumptions

Perfect Encryption Assumption


Atomic Key Assumption


Crypto-techniques are unbreakable
Keys are atomic messages
Open Network Assumption

The adversary controls the network
6 of 27
Interesting Security Properties

Secrecy


Secret messages should never be exposed
to the adversary
Correspondence



iff X event is preceded by a Y event
Scenario:
if A has successfully finished a
authentication protocol run with B, then B
has at least started the protocols run.
7 of 27
Interesting Security Properties – cont’d

Correspondence – cont’d

A way to check correspondence:


in the event sequence, the number of X should
never exceed the number of Y
Use a counter to indicate violation of
correspondence property
8 of 27
Messages

Atomic Messages




Keys
Principal names
Nonce’s
Data
9 of 27
Messages – cont’d

Message Composition



Concatenation m1  m2
Encryption – decryption mk
Formal Representation
*A is the space of atomic messages
*M is the set of all messages
10 of 27
Messages – cont’d

Message Derivation Rules
*
I
is initial set of information
11 of 27
State Machines



Model of honest principals
Model of the adversary
Model of global states
12 of 27
Honest Agents

Each honest agent is modeled as a triple
<N, p, B>



N is the name of the principal
P is a process
B : vars ( N )  M is a set of bindings
13 of 27
The adversary

The adversary is modeled as a pair <Z, I>

Z is the name of the adversary

I  M is the knowledge of the adversary

I is a set of messages
{m1 , m2 , m3 ,, mn }
14 of 27
Global State Model

The global state is a triple <Π, C, S>



 is the product of honest agents and adversary
C is a set of counters
S  M is a set of messages that are considered secrets
15 of 27
Search Algorithms

What to search?


When to search


Search for secrets in the set of messages the
intruder can generate (secrecy)
After each SEND action of an honest agent
(secrecy)
How to Search

Message derivations
16 of 27
Message Derivation

Derivation rules for messages
m1 m2
I
m1  m2
m1  m2
 E1
m1
m k
 {}k I
{m}k
m
k 1
m
m1  m2
 E2
m2
 {}k E
17 of 27
Message Derivation – cont’d

Concepts




minor premise: a key in a inference rule
major premise: any other premise
maximum message: conclusion of the
introduction rule, or major premise of the
elimination rules
normalized derivation tree: a derivation
tree that contains no maximum message
18 of 27
Example Derivation Trees
Example Derivation Tree of
19 of 27
Theorems



Theorem 1: Any derivation tree T for m depending
on assumptions A can be transformed into a
normalized derivation tree T’ for m depending on the
same assumptions A
Theorem 2: No introduction rule appears above an
elimination rule in a normalized derivation tree
Theorem 3: m can be derived from I iff m can be
derived from I*



I is the knowledge of the adversary
I* is the closure of I under all elimination rules
Proves the correctness and decidability of the algorithm
20 of 27
Algorithm Implementation
add(I,m)
i = enumerate(I)
m is x.y
Y
i is {x}y and m is
decryption key
return add(add(I,x),y)
N
Y
add(I,x)
m is {x}y && decryption
key is in I
N
Y
y in I
N
Y
y in I
Y
I=I-i
N
return add(I,x)
N
m is atomic
N
return add(I+m,x)
Y
return I + m
return I + m
21 of 27
Algorithm Implementation – cont’d
Augmenting the adversary’s knowledge
22 of 27
Algorithm Implementation – cont’d
Searching the adversary’s knowledge
23 of 27
The Model is Finite

A run of the a protocol




is some interleaving actions from a set of
participants and from the adversary.
The length of each run is finite
we only consider a small number of runs.
A trace



is the interleaving of one or more runs.
Each trace is finite as well.
We only consider a finite number of traces
24 of 27
Model Evaluation




The model is intuitive and practical
The model is finite and correct
Translation process is tedious
Efficiency is also a problem
25 of 27
References


[1]E. Clarke, S. Jha, and W. Marrero. Using state
space exploration and a natural deduction style
message derivation engine to verify security
protocols. In Proceedings of the IFIP Working
Conference on Programming Concepts and Methods
(PROCOMET), 1998.
[2]Michael Burrows, Martin Abadi, and Roger
Needham. A logic of authentica- tion, from
proceedings of the royal society, volume 426, number
1871, 1989. In William Stallings, editor, Practical
Cryptography for Data Internetworks. IEEE Computer
Society Press, 1996.
26 of 27
Questions and Answers

Why use FM to reason about security
protocols, what are the major methods used?


Structure of the model, why is it finite and
correct?




See slide #3
Model structure: slide #5
Finiteness: slide #24
Correctness: slide #20
Strengths and weaknesses

See slide #25
27 of 27