Se connecter

Se connecter avec OpenID

A progress report on using Maude to verify protocol

Progress Report on Java Based Protocol
Presented by
Stephen W. Mancini, 1Lt, USAF/AFIT
Robert P. Graham, MAJ, USAF/AFIT
Presentation date: 09 Feb 04
• Understand a Java based Protocol
Analysis Tool built for recognizing
Authentication Tests in any Protocol
Research goals
Introduction into Java tool
Perform demo of Java tool
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
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
– 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
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
• Introduction into Java tool
• Performed demo of Java tool on several
• Summary
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.
Без категории
Taille du fichier
260 Кб