Reverse Engineering
#1

[attachment=7282]
[attachment=366]

Presented by:Rajesh M K
Reverse Engineering



Abstract
Cryptographic protocol is a precisely defined sequence of communication and computa¬tion steps that use cryptographic mechanisms such as message encryption and decryption. But even when strong encryption algorithms are used, information is not safe and flaws have been found in protocols considered to be secure. So it becomes necessary to verify the protocol. A number of methods and tools exist for verifying the protocols, which includes the using automata theory, spi caculus, logic programming etc. Two methods, using concept of strand spaces and using proof theory, for verifying the protocols by logic programing is studied.

Introduction
1.1 What is an Reverse Engineering Network
1.2 Verification using logic programing

• it helps to determine the minimum number of messages to achieve a certain set of beliefs;
• useless or erroneous message exchanges can be spotted easily;
• subtle differences between similar protocols come to the surface.
Despite their many merits, they also have their limitations:
• most logics are based on assumptions that are not written explicitly; for instance, many assume that the concatenation of expressions is commutative and that the sender can recognize its own messages; moreover, they assume that the integrity of encrypted (or signed) messages is always preserved (i.e. they withstand message-splicing attacks),
• many require an 'idealization' process, or at least the addition of extra annotations; this 'process', which need to be done prior to the analysis, is not fully automated, and therefore error-prone; often, the analyser uses a cumbersome syntax, which makes it harder to non¬experts to understand the 'subtleties' of the protocol.
In this project the chosen logic constrained first order logic ,or can be easily sepcified as prolog. The two methods studied for first order verification are
• Using concept of strand spaces .The strand space approach is based on the Dolev-Yao intruder model. It is a graph-based method that is used to to prove properties of arbitrary combinations of protocols running at the same time.
• Proof theortic approach.This is a knowledge - state ,based method. Described later
Since the concept of strand spaces were found conceivably difficult and too much formal the proof theoretic method is adopted.
2 Security Requirements
2.1 The core of the method
2.1.1 Assumptions
In routing the primary security service is authorization. There is two types of autorization,
1. Import authorization :- when a routing update is received from the outside, the router needs to decide whether to modify its local routing information base accordingly. It means that the ultimate authority about routing messages regarding a certain destination node is that node itself. Therefore, we will only authorize route information in our routing table if that route information concerns the node that is sending the information. In this way, if a malicious node lies about it, the only thing it will cause is that others will not be able to route packets to the malicious node. 2. Export authorization :- Router carry out export authorization whenever it receives a request for routing information.
Import authorization is the critical service. In traditional routing systems, authorization is a matter of policy. For example, gated, a commonly used routing program, allows the administrator of a router to set policies about whether and how much to trust routing updates from other routers. In mobile ad hoc networks, such static policies are not sufficient.
Authorization may require other security services such as authentication and integrity. Tech¬niques like digital signatures and message authentication codes are used to provide these ser¬vices. 3. Source authentication:- We need to be able to verify that the node is the one it claims to be. 4 Integrity:- we need to be able to verify that the routing information that it is being sent to us has arrived unaltered. The two last security services combined build data authentication, and they are requirements derived from import authorization requirement.

2.1.2 Strategy
2.2 Outline of the method
• Specify formally a cryptographic protocol by writing simple prolog rules defining it.
• Define the goals of a protocol and verify if they are reachable. Similarly it can be checked that unwanted situations are not reachable.
• Define the goals of an intruder, and therefore check the protocol for flaws, by verifying whether they are reachable.
3 Constructing the verifier
The construction of a verifier program for Needham Schroeder Public Key (NSPK) protocol is described.

3.1 Protocol description

A^t B B -)> A A^f B

{A,NA}KB
{Na,Nb}Ka {Nb}Kb


Goal of the protocol is the confidential exchange of two nonces, Na and Nb, which are re¬spectively created by Alice (A) and Bob (B) and encrypted using keys Ka and Kb.

3.2 Primitive facts and rules involved in the program
3.2.1 Messages
Messages contain keys and nonces, which are both integers. Time stamps can also be viewed as nonces. Message contain a list of objects.

Keys : K := Integer
Nonce : N := Integer
Objects : O := K\N%Key or Nonce
MessageContent : M := [] | [OjM] | enc(K, M) %K is either public or private key
Message : msg(M)

Facts for creation of nonces and keys

create_key(Z) :- random(Z). create_nonce(Z) :- random(Z).

3.2.2 Principals
Principal has a unique id, and the protocol step it is at (in the bove case either 1, 2 or 3.
Step: S:= Integer
Agent id: Id:=String % like alice, bob, trudy etc.
Agent state: agent(Id,S) %who is at what step


3.2.3 Knowledge
knowledge is stored by facts or objects like key(kl), nonce(n), or my_nonce(N) where kl,n etc are objects. Knowledge is stored in the knowledge base in facts of the form knows(Id,S,D) containing id of the agent that posses it, and the step S at which the knowledge was acquired.
3.2.4 States
a state is a list containing agent states and/or messages .

3.3 Specifying the protocol
The protocol's translation is fully specified by two prolog clauses : expect and compose. The first is for specifying the behavior of the receiving principal and the second is specifies the behavior of the sending principal. The methods are specified below.

3.3.1 Method expect /4
expect(Id, Step, Message, Knowledge) % first three are the given input arguments ,while the last one is the output .The method succeeds when principal Id at step Step can receive message Message and Knowledge is the facts agents learns during the transaction.

3.3.2 Method compose /5
compose(Id, Step, Nonce, Message, Knowledge) %first three are the input arguments and last two are the output. Variable Nonce is added because sometimes we require a Nonce to be passed to the rule for composing message. The method succeeds when agent ID at step Step can produce message Message, possibly using the nonce Nonce, and Knowledge is the list of facts the principal learns during the transaction.

3.4 Specification of Needham Schroeder protocol
3.4.1 First Transaction
A B : {A, Na}Kb

Bob's Role

expect (bob, 1,M,Info) :-
M = msg ([enc(key (Pkb),[key (Pka),nonce(Na)])]),
knows(bob,keypar(_,Pkb)),
knows(bob,key (Pka)),
Info = [other _nonce(Na),other _key (Pka)].

Alice's Role

compose(alice,l,Nonce,M,Info) :-
knows(alice,keypar(_,Pka)),
knows(alice,key(Pkb)),
M = msg([enc(key(Pkb),[key(Pka), nonce(Nonce)])]), Info = [my_nonce(Nonce), other_key(Pkb)].
3.4.2 Second Transaction B A : {NIL Nb}Ka

Alice's Role expect(alice,2,M,Info) :-
M = msg([enc(key(Pka),[nonce(Na),nonce(Nb)])]), knows(alice,keypar(_,Pka)), knows(alice,my_nonce(Na)), Info = [other_nonce(Nb)].

Bob's Role

compose(bob,2,Nb,M,Info) :-
knows(bob,other _nonce(Na)), knows(bob,other _key(Pka)), Info = [my_nonce(Nb)],
M = msg([enc(key(Pka),[nonce(Na),nonce(Nb)])]).

3.4.3 Third Transaction
A B : {Nb}Kb


Bob's Role

expect(bob,3,M,Info) :-
M = msg([enc(key(Pkb),[nonce(Nb)])]), knows(bob,keypar(_,Pkb)), knows(bob,my_nonce(Nb)), Info = [].

Alice's Role

compose(alice,3,_,M,Info) :-
knows(alice,other_nonce(Nb)), knows(alice,other_key(Pkb)), Info = [],
M = msg([enc(key(Pkb),[nonce(Nb)])]).


3.4.4 Specifying the Initial Knowledge and State
It is also required to specify the initial knowledge of the agents, and the initial state. This is done by adding to the specification the definition for initial_state(State) and initial_knowledge(List of facts).
Rules for specifying initial state and knowledge

initial_state ([agent (alice, 1), agent (bob, 1) ]).
initiaLtheory([knows(alice,0,keypar(SKA,PKA),knows(bob,0,key(PKA)),knows(bob,0,keypar(SKB,PKB),
knows(alice,0,key(PKB))]):- create_keys([PKA,SKA,PKB,SKB]).

3.4.5 Specifying the Final Knowledge and States
Specifying the final state of the protocol is straightforward. This is done by checking that both alice and bob are in state 4.
Rule for checking final state
fmal_state(S):-substate([agent(alice,4),agent(bob,4)],S). Fact for checking final knowledge
Suppose that we want to prove that alice and bob eventually exchange nonces, then we do this by adding the rule:
final-knowledge :- knows(bob,_, other_nonce(NA)), knows(bob,_, my_nonce(NB)), knows(alice,_, other_nonce(NA)), knows(alice,_, my_nonce(NB)).


Reply

Important Note..!

If you are not satisfied with above reply ,..Please

ASK HERE

So that we will collect data for you and will made reply to the request....OR try below "QUICK REPLY" box to add a reply to this page
Popular Searches: reverse engineeringrreverse engineering, reverse eng, reverse power protection of an alternator by wikipedia, reverse power protection of alternater project details, seminar topics on reverse engineering with ppt mechanical, seminar topics based on reverse engineering, reverse engineering download,

[-]
Quick Reply
Message
Type your reply to this message here.

Image Verification
Please enter the text contained within the image into the text box below it. This process is used to prevent automated spam bots.
Image Verification
(case insensitive)

Possibly Related Threads...
Thread Author Replies Views Last Post
  Particle Swarm Optimization Algorithm and Its Application in Engineering Design Optim computer science crazy 3 5,473 03-05-2013, 10:28 AM
Last Post: computer topic
  mini Project Ideas & Seminar Topics for CS & IT Engineering computer science crazy 9 34,025 13-03-2012, 09:59 AM
Last Post: seminar paper
  Reverse Engineering: A Roadmap seminar class 1 1,379 07-02-2012, 10:43 AM
Last Post: seminar addict
  REVERSE ENGINEERING INVESTIGATING THE NANOSCALE computer science technology 1 1,549 07-02-2012, 10:43 AM
Last Post: seminar addict
  Reverse Engineering seminar surveyer 1 2,204 07-02-2012, 10:42 AM
Last Post: seminar addict
  computer science projects for engineering students kasarla vinitha 0 961 28-01-2012, 06:32 PM
Last Post: kasarla vinitha
  Genetic engineering computer science crazy 2 3,167 20-06-2011, 12:21 PM
Last Post: smart paper boy
  Client Server Software Engineering Full Download Seminar Report and Paper Presentatio computer science crazy 1 3,483 24-12-2010, 12:24 PM
Last Post: seminar surveyer
Tongue Security Engineering Electrical Fan 0 1,184 10-09-2009, 05:16 PM
Last Post: Electrical Fan
  Software Engineering for Embedded Systems: Design and Evaluation Electrical Fan 0 1,272 03-09-2009, 02:02 AM
Last Post: Electrical Fan

Forum Jump: