close

Se connecter

Se connecter avec OpenID

A progress report on using Maude to verify protocol

IntégréTéléchargement
Progress Report on Java Based Protocol
Analysis
Presented by
Stephen W. Mancini, 1Lt, USAF/AFIT
Robert P. Graham, MAJ, USAF/AFIT
Presentation date: 09 Feb 04
Objectives
• Understand a Java based Protocol
Analysis Tool built for recognizing
Authentication Tests in any Protocol
Overview
•
•
•
•
Research goals
Introduction into Java tool
Perform demo of Java tool
Summary
Research Goals
• Automate Guttman’s Authentication Tests
• Analyze numerous Protocols
– Originally this was limited to a few protocols
but since analysis is easy, numerous
protocols are examined
• Search for alternative way to model
penetrator activity
– Still not there!
Java Based Analysis
• Initially developed to be used as a prototype for
final Maude tool
• Most model checkers work in a similar fashion
so try something different
• Why use Java language?
– Input files in Java much easier to develop
– Rules would be much easier to understand
– Coding experience in Java reduced time necessary to
develop the tool
• Big learning curve with Maude!
Java Based Analysis
• Input files in Java much easier to develop
– The following shows Needham-Schroeder
input file for Java tool:
A -> B : {*Na1 A}Kb
B -> A : {Na1 *Nb1}Ka
A -> B : {Nb1}Kb
* Marks the first time a nonce is generated
Java Based Analysis
•
The parser breaks down each message into instances of that particular class
–
For example: A -> B : A B {A *Na1}Kb
Protocol
From: A
To: B
Text: A
Message: A B {A *Na1}Kb
Text: B
Encryption: {A *Na1}Kb
Term: {A *Na1}
Text: A
Text: *Na1
Key: Kb
Java Based Analysis
• The tool instantiates individual classes
where sender and receiver roles are
expressed
– This instance will contain all relevant
information pertaining to that principal
•
For example: Components they send, nonce’s they generate, nonce’s they’ve seen and other
properties particular for each participant in the run of the protocol
• The tool also keeps track of all messages
sent in order to allow principals to check
for duplication/spoofs or other errors
regarding any message sent
Java Based Analysis
•
Order of operations:
1. Run through protocol and grab all messages
1. Check for duplicates and store in vectors
2. Check for malformed messages (give errors)
2. Create instance for each Principal
3. Restart evaluation of protocol with above gained
knowledge
4. Analyze each message
1. Populate sender/receiver with relevant information from the
current message being evaluated
2. Depending on sender/receiver check for presence of
authentication test in a particular message
3. Repeat 1 and 2
NS Output using Java Tool
Parsing from file 'NSPublic.txt'
File Contents:
A -> B : {*Na1 A}Kb
B -> A : {Na1 *Nb1}Ka
A -> B : {Nb1}Kb
<Parties> : <Message> >> A -> B : {*Na1 A}Kb
Encrypted term(s) < *Na1 A > with key Kb is readable by recipient only.
Sender may be attempting to initiate an outgoing test by transmitting Na1 in encrypted form.
Unsolicited test for B because of nonce Na1 within test component < {Na1 A}Kb >
<Parties> : <Message> >> B -> A : {Na1 *Nb1}Ka
Encrypted term(s) < Na1 *Nb1 > with key Ka is readable by recipient only.
The encrypted/fresh nonce Na1 has been received back in component: {Na1 Nb1}Ka
Outgoing/Incoming test for A because fresh term Na1 was sent out earlier in < {Na1 A}Kb >
Pseudo-unsolicited test for A because Nb1 is a newly received fresh nonce, but A has sent items to B previously
Sender may be attempting to initiate an outgoing test by transmitting Nb1 in encrypted form.
<Parties> : <Message> >> A -> B : {Nb1}Kb
Encrypted term(s) < Nb1 > with key Kb is readable by recipient only.
The encrypted/fresh nonce Nb1 has been received back in component: {Nb1}Kb
Outgoing/Incoming test for B because fresh term Nb1 was sent out earlier in < {Na1 Nb1}Ka
Live Demo of Java Based Protocol
Analyzer
Summary
• Introduction into Java tool
• Performed demo of Java tool on several
protocols
• Summary
Bibliography
1. Cervesato, Iliano and others. A Comparison
between Strand Spaces and Multiset Rewriting
for Security Protocol Analysis. July 2000.
2. Guttman, Joshua and F. J. Thayer Fabrega.
Authentication Tests. March 2000.
3. Song, Dawn. Athena: A New Efficient
Automatic Checker for Security Protocol
Analysis. June 1999.
4. Clavel, Manuel and others. Maude 2.0 Manual:
version 1. June 2003.
5. http://cliki.tunes.org/Maude.
Auteur
Документ
Catégorie
Без категории
Affichages
4
Taille du fichier
260 Кб
Étiquettes
1/--Pages
signaler