Transcript m - CSE - University of South Carolina

CSCE 715:
Network Systems Security
Chin-Tser Huang
[email protected]
University of South Carolina
What Can Go Wrong…

…when your computer y receive or is
waiting for a message m?
?
m
Internet
x
08/27/2013
y
2
Message Loss

Adversary A can discard m in its transit
A
m
x
08/27/2013
y
3
Message Interception

Adversary A can get a copy of m when
m passes by
A
m
x
08/27/2013
m
m
y
4
Message Modification

Adversary A can arbitrarily modify the
content of m to become m’
A
m
x
08/27/2013
m’
y
5
Message Insertion

Adversary A can arbitrarily fabricate a
message m, pretending that m was sent by x
src: x
dst: y
A
m
x
08/27/2013
y
6
Message Replay

Adversary A can replay a message m that has
been sent earlier by x and received by y
m
A
m
x
08/27/2013
y
7
Denial-of-Service Attack

Adversary A can send huge amount of
messages to y to block m from arriving at y

In the case of botnet attack, the adversary
instructs many bots to send messages to y
simultaneously
A
m
?????
x
08/27/2013
…
…
…
…
…
…
y
8
More Scenarios

In one case, x wants y to be able to verify
message m is sent by a legitimate party but
not able to determine identity of x
src: ?
dst: y
m
Internet
x
08/27/2013
y
9
More Scenarios

In another case, y wants to be able to prove
to third party z that y receives message m
from x
z
x sent
m
m
to y
Internet
x
08/27/2013
y
10
Network Security Is Great…




Protect messages from interception in
their transit
Provide desired level of privacy for user
or data
Detect and discard messages that are
modified, inserted, or replayed
Disallow unauthorized access to local
system resource and sensitive data
08/27/2013
11
…But Hard To Achieve





Many layers in network architecture
Many different media of network
connection
Adversary’s location hard to determine
New attacks keep emerging
Cryptographic overhead
08/27/2013
12
Attacks, Mechanisms, and Services




Security attack: any action that compromises
security of information owned by an organization
Security mechanism: a mechanism designed to
detect, prevent, or recover from a security attack
Security service: a service that enhances security
of data processing systems and information transfers
of an organization
Security service uses one or more security
mechanisms to counter security attack
08/27/2013
13
Type of Attacks

Passive attacks


Message interception
Traffic analysis

Active attacks





08/27/2013
Message loss
Message modification
Message insertion
Message replay
Denial-of-Service
attack
14
Network Security Services

Confidentiality
Integrity
Authentication
Anti-replay

…



08/27/2013




Availability
Access control
Non-repudiation
Anonymity
15
Confidentiality


Keep message known only to the
receiver and remain secret to anyone
else
To counter message interception
08/27/2013
16
Integrity


When receiver receives message m,
receiver can verify that m is intact after
sent by sender
To counter message modification
08/27/2013
17
Authentication


When receiver receives message m,
receiver can verify that m is indeed sent
by the sender recorded in m
To counter message insertion
08/27/2013
18
Anti-replay


When receiver receives message m,
receiver can verify m is not a message
that was sent and received before
To counter message replay
08/27/2013
19
Availability


Property of a system or a resource
being accessible and usable upon
demand by an authorized entity
To counter denial-of-service attack
08/27/2013
20
Access Control



Mechanism to enforce access rights to
resources and data
Users can access resources and data to
which they have access rights
Users cannot access resources and data
to which they don’t have access rights
08/27/2013
21
Non-repudiation


Sender non-repudiation: When
receiver receives message m, receiver
gets proof that sender of m ever sent m
Receiver of m can show proof to thirdparty so that sender of m cannot
repudiate
08/27/2013
22
Non-repudiation


Receiver non-repudiation: When
receiver receives message m, sender
gets proof that receiver of m ever
receives m
Sender of m can show proof to thirdparty so that receiver of m cannot
repudiate
08/27/2013
23
Anonymity


Identity of sender is hidden from
receiver
When receiver receives message m,
receiver has no clue about sender of m
08/27/2013
24
Network Protocols

Abstractions of communication between two
processes over a network




Define message formats
Define legitimate sequence of messages
Take care of physical details of different
network hardware and machines
Separate tasks in complex communication
networks

For example, FTP and ARP
08/27/2013
25
Example: IP Header
08/27/2013
26
Protocol Layering



Many problems need to be solved in a
communication network
These problems can be divided into
smaller sets and different protocols are
designed for each set of problem
Protocols can be organized into layers
to keep them easy to manage
08/27/2013
27
Properties of Protocol Layer

Functions of each layer are independent
of functions of other layers


Thus each layer is like a module and can
be developed independently
Each layer builds on services provided
by lower layers

Thus no need to worry about details of
lower layers -- transparent to this layer
08/27/2013
28
Protocol Stack: OSI Model
Application
Presentation
Session
Transport
Network
Data link
Physical
08/27/2013
29
Communicating End Hosts
Host
Host
Application
Application
Presentation
Presentation
Session
Session
Transport
Router
Transport
Network
Network
Network
Data link
Data link
Data link
Physical
Physical
Physical
08/27/2013
30
Verification of Network Protocols



Many complex protocols perform
multiple functions with multiple
messages
It is desirable to verify that a protocol
can correctly perform functions that it
was designed for
Particularly important for security
protocols
08/27/2013
31
Traditional Ways of
Network Protocol Specification

Plain English

Time charts

Programming languages
08/27/2013
32
Shortcomings of Plain English

Ambiguity


Different words can have similar meanings
process p sends message m to process q
process p transmits message m to process q
process p forwards message m to process q
process p delivers message m to process q
Same word can have different meanings
process p sends message m to process q
process p sends file f to process q
08/27/2013
33
Shortcoming of Time Chart

Not scalable


Many legitimate sequences of messages
Cannot list all possible legitimate sequences when
the number of sequences grows exponentially
08/27/2013
34
Shortcoming of Using
Programming Language


Hard to prove correctness of protocol
specification
For example, protocol specified in C language
may involve overlap, and may involve
transmission delay
08/27/2013
35
Formal Ways of
Network Protocol Specification

BAN logic

Abstract Protocol Notation
08/27/2013
36
BAN Logic


Invented by Burrows, Abadi, and
Needham
Use logical constructs and
postulates to analyze authentication
protocols and uncover various protocol
weaknesses
08/27/2013
37
Logical Constructs








Assume P and Q are network agents, X is a message, and K is
an encryption key
P believes X: P acts as if X is true, and may assert X in other
messages
P has jurisdiction over X: P 's beliefs about X should be
trusted
P said X: At one time, P transmitted (and believed) message X,
although P might no longer believe X
P sees X: P receives message X, and can read and repeat X
{X}K: X is encrypted with key K
fresh(X): X was sent recently
key(K, P<->Q): P and Q may communicate with shared key K
08/27/2013
38
Examples of Postulates




If P believes key(K, P<->Q), and P sees {X}K,
then P believes (Q said X)
If P believes (Q said X) and P believes
fresh(X), then P believes (Q believes X)
If P believes (Q has jurisdiction over X) and P
believes (Q believes X), then P believes X
If P believes that Q said <X, Y>, the
concatenation of X and Y, then P believes
that Q said X, and P also believes that Q said
Y
08/27/2013
39
Shortcomings of BAN Logic



High level of abstraction
Need for a protocol idealization step, in
which the user is required to transform
each message in a protocol into
formulas
Can only verify a round every time
08/27/2013
40
Abstract Protocol Notation

Presented by Mohamed Gouda in the book
Elements of Network Protocol Design


Formal and scalable
Proof of correctness of protocol specification
can be easily done using state transition
diagram
08/27/2013
41
Communication Model

A network of processes and two unbounded
FIFO channels between every two processes
Set of messages
process p
…
08/27/2013
-------
process q
…
42
Process Specification

Each process in a protocol is specified as follows
process px
inp <name of
…
<name of
var <name of
…
<name of
begin
<action>
[]
<action>
…
[]
<action>
end
08/27/2013
input>
:
<type of input>
input> :
variable> :
<type of input>
<type of variable>
variable> :
<type of variable>
43
Action Execution


Specified as <guard>  <statement>
Satisfy three conditions



Atomic: actions in the whole protocol are
executed one at a time; one action cannot start
while another action execution is in progress
Non-deterministic: an action is enabled when
its guard is true; any action that is enabled at a
state can be selected for execution at that state
Fair: if guard of an action is continuously true,
then the action is eventually executed
08/27/2013
44
State Transition Diagram



Define semantic of a protocol
State is defined by a value for each variable
in protocol and by a message set for each
channel in protocol
Transition is movement from current state to
next state triggered by an action execution
08/27/2013
45
An Example Protocol
process p
var ready: boolean
{init. ready=true}
txt, t : integer
begin
ready 
txt := any;
send rqst(txt) to q;
ready := false
process q
var t
: integer
begin
rcv rqst(t) from p 
t := any;
send rply(t) to p
end
[] rcv rply(t) from q 
{use text t in received
message}
ready := true
end
08/27/2013
46
State Transition Diagram of Example
Protocol
T.0
T.1
T.0 :
ready 
ch.p.q = < > 
ch.q.p = < >
T.1 :
~ready 
ch.p.q = <rqst(txt)>
ch.q.p = < >
T.2 :
~ready 
ch.p.q = < > 
ch.q.p = <rply(t.q)>
T.2
08/27/2013
47
Adversary Model

Adversary can change contents of protocol channels
by executing the following actions a finite number of
times




Message loss: lose an original message
Message modification: modify the field of an original
message to cause a modified message
Message replay: replace an original message by another
original message to cause a replayed message
Message insertion: add to a channel a finite number of
arbitrary messages
08/27/2013
48
Prove Correctness of Secure Protocol


Execution of adversary actions may lead the
protocol to a bad state
Protocol is said to be correct if it converges to
its good cycle in a finite number of steps after
adversary finishes executing its actions
08/27/2013
49
Next Class



Network security tools to counter the
effects of adversary actions
Cryptography backgrounds of network
security tools
Read Ch. 2
08/27/2013
50