Transcript The Theory of Secure Design (Jim Alves-Foss)

Network Authentication Protocol
Studies (NAPS):
The Theory of Secure Design
Jim Alves-Foss
Gurdeep Sing Hura
University of Idaho
Moscow, Idaho
Focus of This Research

Enhance the design and analysis techniques
used for modern security protocols


Current protocols are often successfully attacked,
Why?
Present an implementation technique that will
ensure protocols are secure against attacks.

Assuming certain security properties of underlying
crypto, key management software, operating system
and hardware
August 20, 2002
DARPA, OASIS PI Meeting
2
Status

Timetable



Research team


New project, started mid June 2002
Terminates December 2003
2 Faculty, 2/3 students
Commenced with initial tasks, exploring some relevant
issues discussed here



Extension of a formal model of protocols, codifying in ACL2
theorem prover
Evaluating sample protocols and attack space mapping into
formalism
Exploration into a “semantic gap” issues
August 20, 2002
DARPA, OASIS PI Meeting
3
What is a Security Protocol?

A set of messages designed to establish a
desired security property between
communicating agents, (players).



Authentication, privacy, integrity, non-repudiation
May wish to provide key distribution, establishment of
secure communication channel, proof of liveness,
Used in banking, e-commerce, distributed
systems, mobile communications, etc.
August 20, 2002
DARPA, OASIS PI Meeting
4
Cryptographic Protocol
Notation

Encryption




{…}KAB – Uses private key shared between A and B
{…}KA – Uses public part of A’s public key
{…}KA-1 – Uses private part of A’s public key
Other Terms


M.N – Concatenation of M followed by N
RA - random value generated by A

August 20, 2002
for use as a nonce or part of a Diffie-Hellman style keygeneration
DARPA, OASIS PI Meeting
5
Example “Secure” Protocol
A.B.{RA}KB
Ann
B.A.{RA,RB }KA
Bob
A.B.{RB}KB
“A mutual authentication protocol”
Adapted From: Needham Schroeder, “Using Encryption for Authentication in Large Networks of Computers”,
Communications of the ACM, 21(12), December 1978, pg. 993-999.
August 20, 2002
DARPA, OASIS PI Meeting
6
Sample Attack: Replay

When the attacker takes a message
generated by a communicating party and
inserts it into the communication stream of
an executing protocol in order to spoof a
user of the protocol.



earlier component from current protocol run
earlier component from previous protocol run
component from concurrent protocol run
August 20, 2002
DARPA, OASIS PI Meeting
7
Attack on NS Protocol
A.E.{RA}KE
E(A).B.{RA}KB
E.A.{RA,RB }KA
Ann
A.E.{RB}KE
E
V
E
B.E(A).{RA,RB }KA
Bob
E(A).B.{RB}KB
“An attack on the mutual authentication protocol”
Adapted From: Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR,”,
Proc. TACAS, 1996, pp. 147-166.
August 20, 2002
DARPA, OASIS PI Meeting
8
Other Problems


Numerous Attacks have been published against
protocols that don’t use correct labeling
Recent: Catherine Meadows, FCS June 2002

Discovered an attack on a draft group multicast
protocol, GDOI, where a dishonest participant could
force a signature, generating a fake new group key.


This occurred when a signature key was used to sign two
different messages in the protocol, where the messages
were not well labeled.
Developed formalism for defining and detecting
probabilities of “type confusion” between sets of
generated messages.
August 20, 2002
DARPA, OASIS PI Meeting
9
What Happened?

We used cryptography, it should be
secure!!

Designers/analysts must correctly interpret
the semantics of cryptographic services
and how they are used.
August 20, 2002
DARPA, OASIS PI Meeting
10
What Really Happens in
Protocol Message Exchange?
M1
Mysterious
Beyond
Ann’s Protocol
M2
Ann needs to determine what happened in the “Mysterious Beyond”
between the transmission of message M1 and the receipt of Message M2
August 20, 2002
DARPA, OASIS PI Meeting
11
Semantic Assumptions

Proof carrying assumptions

Receiver can tell if a message is correctly decrypted
(sender used correct protocol and key)


Receiver can determine partial ordering on messages


easy when crypto algorithm includes encrypted checksums
Easy if initial message included a new/unique number (nonce) and
response also includes that number where number must have been
cryptographically “handled”
Receiver can tell if a message is well-formed and well-typed


August 20, 2002
Not easy if there exists a collision in the type labels (if they even
exist) of different messages.
Why? Because the bad guys can cheat, and good guys make
mistakes or do their own thing.
DARPA, OASIS PI Meeting
12
Semantics of Crypto Services

Crypto Semantics (Axioms assumed of Crypto
Services)

Handling – creation or reading of specific message
contents (not relaying, but content handling)




{…}KAB – A or B was last player to handle message and A or
B will be next player to handle message
{…}KA – A is next subject to handle message
{…}KA-1 – A was last subject to handle message
The semantics are not Context-Sensitive

August 20, 2002
Cryptography provides no requirement that the sender is
operating within the same context as the receiver. We must
add additional semantic constraints at a higher level
DARPA, OASIS PI Meeting
13
Semantic Layering
Application
Semantic
Gap
Protocol
Crypto Engine
TCP/IP Stack
August 20, 2002
Want: Privacy, Integrity,
Authentication, Non-repudiation
Authentication? Key
Distribution? Privacy? NonRepudiation? Integrity?
Liveness? Freshness?
Handling Semantics; Can
Determine Last/Next Handler
Reliable End-To-End Transport
DARPA, OASIS PI Meeting
14
How Do We Prevent Replay
Attacks?

Uniquely identify each encrypted component of
every message transmitted. This requires:





Session ID, established prior to protocol run; unique
for every run of the protocol
Component ID, established at protocol design time.
IDs are encrypted within each message.
These ideas are similar to those already in literature
but have unique properties.
Does this prevent the bad guys from cheating?
August 20, 2002
DARPA, OASIS PI Meeting
15
Does labeling ever work?

Yes, if we can guarantee disjoint encryption



Sufficient - to prevent cryptographic replays
Necessary – we believe so, needs proof
Possible if:

Every protocol uses the same rules and encoding


–or– Keys are enforceably bound to specific PROTOCOLS (we
know users are willing to manage many keys)


we know vendors/designers will agree ;-)
this means you need a key for each version/implementation of each
crypto protocol on your system (expensive for certified public keys)
–or– Crypto engines provide “context sensitive” encryption
services
August 20, 2002
DARPA, OASIS PI Meeting
16
PAPI

Proposed solution:
Protocol Services
Layer


forces unique
labeling.
Implementation:
Protocol
Application
Programmers
Interface (PAPI)
August 20, 2002
Application Layer
Security Services
Provider
CDSA, MS
CryptoAPI,
JCE,
Entrust
DARPA, OASIS PI Meeting
Protocol Services Layer
SSL,
IPSE
C,
PAPI
TCP/IP,
Sockets
Network Services Layer
17
Tasks of this Project
1.
Expand Existing Formal Analysis Model


2.
3.
4.
Reason about wider classes of attacks
Validate with existing protocols/attacks
Develop Software Engineering Methodology for
Secure Protocol Development
Demonstrate Feasibility on Simple Protocols
Demonstrate Feasibility on Fault Tolerant
Survivable Network Management System
August 20, 2002
DARPA, OASIS PI Meeting
18
Formal Model

Use Strand Space Model


Developed by Fábrega, Herzog & Guttman
Model Defines:





August 20, 2002
Facts: messages, plain-text and encrypted (we add labels
(tags) to our messages to uniquely identify cryptographic
components)
Strands: consist of transmissions and receptions of facts
Bundles: consist of interactions between strands
Honest Strand: Define behavior of “good guys”
Intruder Strand: fits a model of behavior that has control over
network messages; we add replaying to allow for runexternal attacks
DARPA, OASIS PI Meeting
19
Proofs

We Prove



If there exists a successful attack against a protocol
implemented using our tagging scheme, then there
must exist an equivalent attack against the protocol
that does not use replays.
Therefore, no replay attacks exist under our tagging
scheme.
Following example is for an attack against
authentication
August 20, 2002
DARPA, OASIS PI Meeting
20
Proof Details

Initially

We assume honest players tag correctly and
do not accept ill-tagged facts.


May either ignore ill-tagged messages or abort
protocol run
We define a retagging method () that takes
facts of one bundle and correctly tags them
according to our scheme.

August 20, 2002
This is fair to do, since ill-tagged facts will be
discarded by honest players.
DARPA, OASIS PI Meeting
21
More proof details




Assume there exists an attack against the tagged bundle
C; where no secret keys are compromised.
Assume there exists a strand of minimal height that
represent acceptance of authentication; but no
corresponding honest sender
We then take the bundle and retag it with () to get C’;
which is secure against replays since all messages are
well-tagged, and honest players will not accept ill-tagged
messages
We prove that the re-tagged attack still works., there fore
the crucial portion of the attack was not dependent upon
replays.
August 20, 2002
DARPA, OASIS PI Meeting
22
Next Steps
Continue with extending strand space model to
address new attacks and engineering
approaches
1.



Replay attacks
Guessing and probabilistic attacks
Fault Tolerant Design Issues
Formalize Semantic Gap
2.


Is disjoint encryption necessary?
Under what assumptions is disjoint encryption
possible.
August 20, 2002
DARPA, OASIS PI Meeting
23
Further Steps
3.
4.
Once we resolve model and semantic
issues, map these into software
engineering methodology.
Start applying model and methodology to
existing protocols
August 20, 2002
DARPA, OASIS PI Meeting
24
Thank you.
August 20, 2002
DARPA, OASIS PI Meeting
25
Security Service
Requirements




Always invoked
Non-bypassable
Tamperproof
Evaluatable
August 20, 2002
DARPA, OASIS PI Meeting
26