ss2

Network Security ArchitecturesPart 2 Formalization and TestingSummer School on Software Security Theory to Practice: 

Network Security Architectures Part 2 Formalization and Testing Summer School on Software Security Theory to Practice Carl A. Gunter University of Pennsylvania Summer 2004

End-to-End Security and Mandatory Tunnels: 

End-to-End Security and Mandatory Tunnels Security Gateway Client Server Examples: WTLS, cdma2000, L2TP, Palm VII

Goals for a Security Protocol : 

Goals for a Security Protocol If client C receives content from server S, then this is authorized by the policies of S and all of the security gateways between C and S If C receives content from S, then this content is encrypted and authenticated from end-to-end between C and S Simple setup and low-overhead enforcement

IPSec Strategy: 

IPSec Strategy

Encapsulation: 

Encapsulation AH headers for authentication and authorization of traversal. Use tunnel mode. ESP header for authentication and confidentiality of end-to-end communication. Use transport mode.

Drawbacks to IPSec Solution: 

Drawbacks to IPSec Solution

IP SEC Header Overheads for 576 Byte Packets: 

IP SEC Header Overheads for 576 Byte Packets Security overhead = (4.50 + 7.61t) (60.8 – 5.25t)

Evidence of Problems: 

Evidence of Problems Experimental: FreeBSD IPSec showed an overhead of 46% with two gateways Standards activity: secure L2TP overheads were so severe a standard was developed specifically to reduce them. Default security with one gatekeeper yielded this: ESP IP L2TP UDP IP PPP TCP ESP Payload ESP ESP A Goodloe, C Gunter, T Hiller, P McCann, M McDougall

Case Study: Layer 3 Accounting (L3A): 

Case Study: Layer 3 Accounting (L3A) Motivating problem from wireless security Solution by composing secure tunnels Maude model Problems Future work A Goodloe, C Gunter, MO Stehr

Wireless Security: 

Wireless Security Why is wireless security any different from wired security? Resource constraints Increased risk to confidentiality Value of the network link

Wireless Security Efforts: 

Wireless Security Efforts Layer 1 (Physical) Spread spectrum Layer 2 (Link) 802.11x – 802.11(b) WEP, 802.11(g) CDMA 2000 GPRS

802.11/WEP: 

802.11/WEP SSL WEP Router/NAT

Network Layer Wireless Security: 

Network Layer Wireless Security We propose that security be addressed at the network layer Advantages Independent of underlying link layer Overcomes many of the problems of layer 2 solutions Leverages extensive experience, s/w, and h/w support from Ipsec for VPNs Disadvantage Need set up protocols

Protocols for Tunnel Composition: 

Protocols for Tunnel Composition We have been investigating protocols for composing IPSec security tunnels Given a scenario we ask: What tunnels should we establish? What properties should these tunnels have? Develop protocols that compose these tunnels into a satisfactory solution Lots of messy details to consider in order to get the composition to work

Toward Layer 3 Security: 

Toward Layer 3 Security Suppose we have three parties: client, server, network access server (NAS) The client wishes to securely access the server We will assume that the client has a relationship with the NAS and the server, but the NAS does not have a relationship to the server The Client will have to authenticate itself to both the NAS and the server

Network Layer Wireless Security: 

Network Layer Wireless Security

Problem: 

Problem Similar problem as before The NAS does not protect the client from attacking incoming traffic Being forced to pay for service you never used is worse than denial of service

How About a Firewall?: 

How About a Firewall?

Why Not a Firewall: 

Why Not a Firewall A stateful firewall can be programmed to allow only traffic from the address to which a connection has been made The firewall can not see the contents of the Ipsec traffic and cannot guarantee origin of any traffic.

L3A Protocol Principles: 

L3A Protocol Principles The user’s traffic should travel in DOS resistant IPSec tunnels These IPSec tunnels should be set up using DOS resistant protocols The NAS should ensure that when the accounting system logs traffic as being from a user it is actually from that user: viz. it must authenticate incoming traffic

L3A Protocol Components: 

L3A Protocol Components L3A protocol sets up three bidirectional tunnels SIKE Key Exchange protocol (X509 + DoS protection) Very simple: does not use two party key generation No guarantee of perfect forward secrecy. Assumes existence of public key infrastructure

L3A Architecture: 

L3A Architecture

Methodology : 

Methodology An English language description resembling an IETF RFC is produced A formal specification is written in Maude Systems are modeled using membership equational logic and rewriting logic Symbolic simulation has been our main debugging aid We feel the design is now relatively stable

IPSec SA & SPD: 

IPSec SA & SPD Security Associations define a set of cryptographic transformations that are applied to each packet. Authentication w/ HMAC. Encrypt w/3DES. SAD Security Policies filter traffic and define what SAs apply to what traffic. CS goes into tunnels CS and CN SPD

SIKE: 

SIKE A B rA, SPI(n,0) rA,rB, SPI(n,m), certB, cookieA certA,cookieA, DA, Ps(a,DA) Where DA = [rA, IPB, SPI(n,m)] Where CookieA = VersionSecret | Hash([rA,rB,IPA, SPI(n,m)],Secret) DB, Ps(b,DB) Where DB = [rB, IPA, rA, SPI(n,m), Pe(A, K)] Update SADB/SPD AB Update SADB/SPD BA Update SADB/SPD BA Update SADB/SPD AB

L3A Protocol Overview: 

L3A Protocol Overview Client NAS Server Req(cred) Ack(cred) Fin SPD CS:(CN) SPD C->S:(C->N) SPD SC:(SN) SPD:SC:(SN)

Abstractions: 

Abstractions Getting the right level of abstraction Modeled the various components and layers IP, IPSec, L3A, ….. We found that we didn’t need to model details of IPSec authentication and encryption since we are interested in the set up of tunnels We discovered that our model of IP send/receive was too abstract. Introduced messy concurrency problems

Overview of Module Interaction: 

Overview of Module Interaction L3A PKI SIKE Ipsec IP setkey

Slide29: 

Security Assoc State Message Ipsec Security Policy SIKE PKI L3A Abstract L3A L3A Test Abstract L3A Test Concrete SIKE Test IP Routing Table IP Message Setkey

Modeling Uncovered Problems: 

Modeling Uncovered Problems Problems arose from interactions among the components Numerous iterations were required to resolve problems resulting from when the Ipsec databases are updated Maude search feature was of great help here When things are not done right packets can slip into partially set up tunnels

We Didn’t Model: 

We Didn’t Model Timers Lost Messages Periodic updates to the secret used to generate the cookie Fragmentation Can be the source of DOS attacks UDP layer: Ports not mentioned at all in the model

Implementation: 

Implementation Under development at this moment Platform. X86 running FreeBSD w/ IPSec. C with Open SSL crypto libraries Radius server to be used for accounting Will demonstrate that our protocol can be implemented using available technology Hope to get some useful benchmarks A Goodloe, C Gunter, M Jacobs, G Shah

Future Work: 

Future Work Continue work on verifying composition of security tunnels We are currently thinking about attacks Do such compositions introduce new vulnerabilities? Add the capability to reuse tunnels Seemed easy at first, but may require some major restructuring of the design Figure out what theorems need to be proven

Simulators: 

Simulators Maude “logical simulations” Exhaustive breath first search. Model checking. Must abstract things like packet size. Not good with timers. Not really useful for performance modeling. OPNET, NS-2 discrete event simulation. Good at modeling details (time, etc). Often used to estimate network performance Not good at finding the extreme cases Probably wouldn’t have found several of our concurrency problems

Summary: 

Summary Complex problems arise when composing high-level security protocols such as Ipsec tunnels Wireless networks pose some new challenges but can leverage general solutions Symbolic simulation can provide a powerful tool for the design of network security protocols