Transcript NPG Workshop - Stanford University

Protocol analysis, wireless
networking, and mobility
John Mitchell
Stanford University
Many security Protocols
Challenge-response
• ISO 9798-1,2,3; Needham-Schroeder, …
Authentication
• Kerberos
Key Exchange
• SSL handshake, IKE, JFK, IKEv2,
Wireless and mobile computing
• Mobile IP, WEP, 802.11i
Electronic commerce
• Contract signing, SET, electronic cash, …
Mobile IPv6 Architecture
Mobile Node (MN)
IPv6
Direct connection via
binding update
Corresponding Node (CN)
Home Agent (HA)
 Authentication is a
requirement
 Early proposals weak
802.11i Wireless Authentication
TLS protocol layer over TCP/IP
http
telnet
ftp
Application
SSL/TLS
Transport
Internet
(TCP)
(IP)
Network interface
Physical layer
nntp
SSL/TLS
ClientHello
ServerHello,
[Certificate],
[ServerKeyExchange],
[CertificateRequest],
ServerHelloDone
C
[Certificate],
ClientKeyExchange,
[CertificateVerify]
switch to negotiated cipher
Finished
switch to negotiated cipher
Finished
S
Handshake Protocol
ClientHello
CS
C, VerC, SuiteC, NC
ServerHello
SC
VerS, SuiteS, NS, signCA{ S, KS }
ClientVerify
CS
signCA{ C, VC }
{ VerC, SecretC } K
S
signC { Hash( Master(NC, NS, SecretC) + Pad2 +
Hash(Msgs + C + Master(NC, NS, SecretC) + Pad1)) }
(Change to negotiated cipher)
ServerFinished S  C { Hash( Master(NC, NS, SecretC) + Pad2 +
Hash( Msgs + S + Master(NC, NS, SecretC) + Pad1))
} Master(NC, NS, SecretC)
ClientFinished C  S
{ Hash( Master(NC, NS, SecretC) + Pad2 +
Hash( Msgs + C + Master(NC, NS, SecretC) + Pad1))
} Master(NC, NS, SecretC)
IKE subprotocol from IPSEC
m1
A, (ga mod p)
A
B, (gb mod p), signB(m1,m2)
m2
signA(m1,m2)
Result: A and B share secret gab mod p
Analysis involves probability, modular exponentiation,
complexity, digital signatures, communication networks
B
Explicit Intruder Method
Informal
Protocol
Description
Formal
Protocol
Find error
Intruder
Model
Analysis
Tool
Run of protocol
Initiate
A
Respond
B
Attacker
C
D
Correct if no security violation in any run
Automated Finite-State Analysis
Define finite-state system
• Bound on number of steps
• Finite number of participants
• Nondeterministic adversary with finite options
Pose correctness condition
• Can be simple: authentication and secrecy
• Can be complex: contract signing
Exhaustive search using “verification” tool
• Error in finite approximation  Error in protocol
• No error in finite approximation  ???
Murj
[Dill et al.]
Describe finite-state system
• State variables with initial values
• Transition rules
• Communication by shared variables
Scalable: choose system size parameters
Automatic exhaustive state enumeration
• Space limit: hash table to avoid repeating states
Research and industrial protocol verification
Applying Murj to security protocols
Formulate protocol
• Assume finite participants
– Example: 2 clients, 2 servers
• Assume finite message space
– Represent random numbers by r1, r2, r3, …
– Do not allow unbounded encrypt(encrypt(encrypt(…)))
Add adversary
• Control over “network”
• Possible actions
(shared variables)
– Intercept any message
– Remember parts of messages
– Generate new messages, using observed data and
initial knowledge (e.g. public keys)
Needham-Schroeder in Murj (1)
const
NumInitiators: 1;
NumResponders: 1;
NumIntruders:
1;
NetworkSize:
1;
MaxKnowledge: 10;
type
InitiatorId:
ResponderId:
IntruderId:
AgentId:
------
number of initiators
number of responders
number of intruders
max. outstanding msgs in network
number msgs intruder can remember
scalarset (NumInitiators);
scalarset (NumResponders);
scalarset (NumIntruders);
union {InitiatorId, ResponderId, IntruderId};
Needham-Schroeder in Murj (2)
MessageType : enum {
M_NonceAddress,
M_NonceNonce,
M_Nonce
};
Message : record
source:
AgentId;
dest:
AgentId;
key:
AgentId;
mType:
MessageType;
nonce1:
AgentId;
nonce2:
AgentId;
end;
-- types of messages
-- {Na, A}Kb nonce and addr
-- {Na,Nb}Ka two nonces
-- {Nb}Kb
one nonce
-------
source of message
intended destination of msg
key used for encryption
type of message
nonce1
nonce2 OR sender id OR empty
Needham-Schroeder in Murj (3)
-- intruder i sends recorded message
ruleset i: IntruderId do
-- arbitrary choice of
choose j: int[i].messages do
-- recorded message
ruleset k: AgentId do
-- destination
rule "intruder sends recorded message"
!ismember(k, IntruderId) &
-- not to intruders
multisetcount (l:net, true) < NetworkSize
==>
var outM: Message;
begin
outM
:= int[i].messages[j];
outM.source := i;
outM.dest
:= k;
multisetadd (outM,net);
end; end; end; end;
Run of Needham-Schroeder
Find error after 1.7 seconds exploration
Output: trace leading to error state
example
Murj
times after correcting error:
number of
ini. res. int.
1
1
1
1
1
1
2
1
1
2
2
1
size of
network
1
2
1
1
states
time
1706
3.1s
40207
82.2s
17277
43.1s
514550 5761.1s
State Reduction on N-S Protocol
1000000
514550
155709
100000
17277
6981
10000
1000
100
1706
980
3263
222
58
10
1
1 init
1 resp
2 init
2 init
1 resp 2 resp
Base: hand
optimization
of model
CSFW:
eliminate
net, max
knowledge
Merge
intrud send,
princ reply
Security Protocols in Murj
Standard “benchmark” protocols
• Needham-Schroeder, TMN, …
• Kerberos
Study of Secure Sockets Layer (SSL)
• Versions 2.0 and 3.0 of handshake protocol
• Include protocol resumption
Tool optimization
Additional protocols
• Contract-signing
• Wireless networking
… ADD YOUR PRODUCT HERE …
CS259 Term Projects
iKP protocol family
Electronic voting
XML Security
IEEE 802.11i wireless
handshake protocol
Onion Routing
Electronic Voting
Secure Ad-Hoc
Distance Vector
Routing
An Anonymous Fair
Exchange
E-commerce Protocol
Secure Internet Live
Conferencing
Windows file-sharing
protocols
Key Infrastructure
Wireless Threats
Changhua He
 Passive Eavesdropping/Traffic Analysis
• Easy, most wireless NICs have promiscuous mode
 Message Injection/Active Eavesdropping
• Easy, some techniques to gen. any packet with common NIC
 Message Deletion and Interception
• Possible, interfere packet reception with directional antennas
 Masquerading and Malicious AP
• Easy, MAC address forgeable and s/w available (HostAP)
 Session Hijacking
 Man-in-the-Middle
 Denial-of-Service: cost related evaluation
Wireless Security Evolution
 802.11 (Wired Equivalent Protocol)
•
•
•
•
Authentication: Open system (SSID) and Shared Key
Authorization: some vendor use MAC address filtering
Confidentiality/Integrity: RC4 + CRC
Completely insecure
 WPA: Wi-Fi Protected Access
• Authentication: 802.1X
• Confidentiality/Integrity: TKIP
• Reuse the legacy hardware, still problematic
 IEEE 802.11i (Ratified on June 24, 2004 )
•
•
•
•
Mutual authentication
Data confidentiality and integrity: CCMP
Key management
Availability
RSNA Conversations
Supplicant
UnAuth/UnAssoc
Auth/Assoc
802.1X UnBlocked
Blocked
No Key
MSK
PMK
New
PTK/GTK
GTK
Authenticator
UnAuth/UnAssoc
Auth/Assoc
802.1X UnBlocked
Blocked
No Key
PMK
New
PTK/GTK
GTK
Authentication Server
(RADIUS)
MSK
No
Key
802.11 Association
EAP/802.1X/RADIUS Authentication
MSK
4-Way Handshake
Group Key Handshake
Data Communication
Security Level Rollback Attack
Supplicant
RSNA enabled
Pre-RSNA enabled
Authenticator
RSNA enabled
Pre-RSNA enabled
Bogus Beacon (Pre-RSNA only)
Beacon + AA RSN IE
Probe Request
Bogus Probe Response (Pre-RSNA only)
Probe Response + AA RSN IE
802.11 Authentication Request
802.11 Authentication Response
Bogus Association Request (Pre-RSNA only)
Association Request + SPA RSN IE
802.11 Association Response
Pre-RSNA Connections
Solutions
Security Level Rollback Attack
• Similar to general version rollback attack
• Destroy security since WEP is insecure
• Not vulnerability of 802.11i standard, but an
implementation problem
Solutions
• Allow only RSNA connections: secure, but too
strict for common networks, where Transient
Security Network is more convenient
• Deploy both, but
– Supplicant manually choose to deny or accept
– Authenticator limit pre-RSNA connections to only
insensitive data
Reflection Attack
Adversary
Impersonates
Communicating
Peers
Legitimate Devices
Authenticator and
Supplicant
{A1, Nonce1, sn, msg1}
{A2, Nonce1, sn, msg1}
{A1, Nonce2, RSN IE, sn, msg2, MIC}
{A2, Nonce2, RSN IE, sn, msg2, MIC}
{A1, Nonce1, RSN IE, GTK, sn+1, msg3, MIC}
{A2, Nonce1, RSN IE, GTK, sn+1, msg3, MIC}
{A1, sn+1, msg4, MIC}
{SPA, sn+1, msg4, MIC}
Bogus Authentication
Peers Authenticated
Reflection Solutions
Possible in ad hoc networks
Violates mutual authentication
Solutions:
• Restrict each entity to single role
– Access point is not wireless station
• Allow one entity to have two roles
– But require different pairwise master keys (PMK)
802.11i Availability
 Not an original design objective
 Physical Layer DoS attacks
• Inevitable but detectable, not our focus
 Network and upper Layer DoS attack
• Depend on protocols, not our focus
 Link Layer attack
•
•
•
•
•
•
Flooding attack: Lots of traffic and power req’d
Some Known DoS attacks in 802.11 networks
DoS attack on Michael algorithm in TKIP
RSN IE Poisoning/Spoofing
4-Way Handshake Blocking
Failure Recovery
4-Way Handshake Blocking
Supplicant
Auth/Assoc
802.1X Blocked
PMK
Authenticator
Auth/Assoc
802.1X Blocked
PMK
AA, ANonce, sn, msg1
PTK Derived
SPA, SNonce, SPA RSN IE, sn, msg2, MIC
AA, ANonce, sn, msg1
PTK Derived
Random GTK
AA, ANonce, AA RSN IE, GTK, sn+1, msg3, MIC
SPA, sn+1, msg4, MIC
AA, ANonce, sn, msg1
PTK and GTK
802.1X Unblocked
PTK and GTK
802.1X Unblocked
Countermeasures
 Random-Drop Queue
• Randomly drop a stored entry if the queue is full
• Not so effective
 Authenticate Message 1
• Use the share PMK; must modify the packet format
 Reuse supplicant nonce
• Reuse SNonce, derive correct PTK from Message 3
• Performance degradation, more computation in supplicant
 Combined solution
•
•
•
•
•
Supplicant reuses SNonce
Store one entry of ANonce and PTK for the first Message 1
If nonce in Message 3 matches the entry, use PTK directly
Eliminate memory DoS, only minor change to algorithm
Adopted by TGi
Failure Recovery
 Failure recovery is important
• Can reduce but not eliminate DoS vulnerabilities
 Current 802.11i method
• When failure, restart everything: inefficient
 A better failure approach
• If 802.1X does not finish, restart everything
• Otherwise restart from nearest completed subprotocol
• Channel scanning time is significantly larger than the
protocol execution time
Improved 802.11i
Stage 1: Network and Security Capability Discovery
Stage 2: 802.1X authentication
(mutual authentication, shared secret, cipher suite)
802.1X Failure
Stage 3: Secure Association (management frames protected)
Association Failure
Stage 4: 4-Way Handshake
(PMK confirmation, PTK derivation, and GTK distribution)
4-Way Handshake Timout
Stage 5: Group Key Handshake
Group Key Handshake Timout
Stage 6: Secure Data Communications
Michael MIC Failure or Other Security Failures
Summary of larger study
ATTACKS
SOLUTIONS
security rollback
supplicant manually choose security; authenticator
restrict pre-RSNA to only insensitive data.
reflection attack
each participant plays the role of either authenticator or supplicant; if both, use different PMKs.
attack on Michael
countermeasures
cease connections for a specific time instead of
re-key and deauthentication; update TSC before
MIC and after FCS, ICV are validated.
RSN IE poisoning
Authenticate Beacon and Probe Response frame;
Confirm RSN IE in an earlier stage;
Relax the condition of RSN IE confirmation.
4-way handshake
blocking
adopt random-drop queue, not so effective;
authenticate Message 1, packet format modified;
re-use supplicant nonce, eliminate memory DoS.
802.11i correctness proof in PCL
 EAP-TLS
• Between Supplicant and Authentication Server
• Authorizes supplicant and establishes access key (PMK)
 4-Way Handshake
• Between Access Point and Supplicant
• Checks authorization, establish key (PTK) for data
transfer
 Group Key Protocol
• AP distributes group key (GTK) using KEK to supplicants
 AES based data protection using established keys
Our proof covers subprotocols 1, 2, 3 alone and in various combinations
SSL/TLS
ClientHello
ServerHello,
[Certificate],
[ServerKeyExchange],
[CertificateRequest],
ServerHelloDone
C
[Certificate],
ClientKeyExchange,
[CertificateVerify]
switch to negotiated cipher
Finished
switch to negotiated cipher
Finished
S
TLS Protocol: Client
The TLS Server actions also defined by a straight-line sequential process (cord)
TLS Properties
Authentication: client and the server agree on
•
•
•
•
Master secret
Protocol version and crypto suite
Each other’s identities
Protocol completion status
Secrecy
• The master secret must not be known to any other
principal
Theorems: Agreement and Secrecy
Client is guaranteed:
• there exists a session
of the intended server
• this server session
agrees on the values of
all messages
• all actions viewed in
same order by client
and server
• there exists exactly
one such server session
Similar specification for server
Invariants required by TLS
Server Side Recommendation: If the server reuses Public Key in a
protocol different from TLS, then it should not send decryptions of
incoming messages
4-Way handshake: Authenticator
Supplicant actions also defined by a straight-line sequential process (cord)
4-Way Handshake properties
The pairwise key (PTK) is fresh and
correctly generated from the PMK
Messages 2 and 4 assure authenticator
that supplicant messages are current (not
replay)
Message 3 assures supplicant that
authenticator messages are current (not
replay)
Pairwise key PTK derivation produces
shared secret between supplicant and
authenticator
4-way Handshake Properties
Similar specification for server
4-Way : Relating invariants to deployment
Recommendation: One Principal should not act as both
authenticator and supplicant ! Otherwise, reflection attack.
Consider careful deployment in Sensor Network scenarios
Group-Key Protocol
Group key handshake
 Authenticator guarantee: If principal has
the group key, then it must have a shared
PTK with the authenticator
Supplicant guarantee: the GTK received was
transmitted by the Access Point, and
correctly supersedes any GTK from earlier
handshakes (4-Way or Group Key)
Observation: For assurance of GTK freshness, important that the
first handshake uses 4-Way protocol; one principal should not be
authenticator and supplicant, as in the 4-way handshake.
Composition
 All necessary invariants are satisfied
by basic blocks of all the subprotocols
 The postconditions of TLS imply the
preconditions of the 4-Way
handshake
The postconditions of 4-Way
handshake imply the preconditions of
the Group Key protocol
Complex Control Flows
Simple Flow
Complex Flow
And what about mobility … ?
Arnab Roy
IPv4: Triangle routing
• All traffic routed through home agent
IPv6: Binding update
• Mobile node sends new “care-of address”
• Many risks
– Attacker can subvert existing connection
• Announce false care-of address
– Also, can send lots of packets to target
• Announce that target is new care-of address for
many connections
Representative protocol
Corresponding node
1 X, Y, H
Y
2 Y, X, n
2
2
2 Y, H, m, X
4 X, Y,
hash(m, n, H, X)
1
X
4
Mobile node
3
3 H, X, m, Y
H
Home agent
Current situation
Under strong assumptions
• Assume limited read access to messages
• Can prove that CN receives a good
address
Under more realistic assumptions
• Have found many attacks
Conclusions
Protocol analysis methods
• Model checking is fairly easy to apply
• Ready for industrial use
Wireless 802.11i
• Automated study led to improved standard
• Deployment recommendations also
Mobile networking
• Partial analysis so far
• No clear guarantees without key infrastructure