Three Extensions of BAN logic



Three Extensions of BAN logic

Heather Goldsby

Michelle Pirtle

BAN logic remains important because it was the first language to reason about the beliefs of principals involved in a protocol. However, BAN logic is not practical to use to verify the correctness of a protocol since there are several known limitations. 1. BAN provides no way to reason about what a principal does not know 2. There is no process for converting a protocol to idealized form, thus it may be done incorrectly. 3. BAN is unable to represent whether or not a principal is honest. These limitation result in false positives where BAN verifies a protocol as correct when the protocol is actually flawed.

This survey will analyze three belief logics: RV logic, GNY logic, and SG logic. Each logic attempts to improve upon BAN logic by resolving some of the limitations, thus providing an alternate method to verify the protocol correctness. Analysis of the logics will include, how each logic attempts to solve the limitations of BAN logic, whether or not the attempt to solve the limitations was successful, how practical each logic is to use (primarily focusing on tool support), and a comparison of the different logics involved in the survey. In order to provide consistent grounds to compare the logics, each will express the Needham Schroeder protocol and will attempt to find the flaws within it. Also key examples will be provided to highlight the extensions the logic has made to BAN if they are not already exemplified in the Needham Schroeder protocol.

Milestones:

-literature review of papers pertaining to RV logic, GNY logic and SG logic (completed)

-choice of a protocol by which to compare the logics – Needham Schroeder (completed)

-Comparison of the logics, different facets to be examined: (11/18)

-extensions to BAN

-stated goal for the logic

-type of protocols that can be analyzed with the logic

-type of errors in the protocols, which are expected to be found w/

the logic

-practicality of using the logic

-analysis of tool support for each of the logics (11/20)

-SPEAR – BAN and GNY

-RVChecker –RV logic

-SH Verification tool –SG logic

-comparison of tools for the logics (11/22)

-first draft (11/25)

-second draft

-third draft

Tools:

We have previously worked with SPEAR for our BAN presentation, hence it does not present a problems. The probability of getting SH Verification tool is extremely slim since it was developed in Germany and the developers will not allow ftping from their site. However, extensive documentation does exist on SH Verfication tool, which we are hoping will aid in our project. We are still working on obtaining a copy of RVChecker from either Jeanette Wing or Darrell Kindred. We think it was just developed for a thesis and thus is not particularly easy to access a copy of.

Research Background papers bibtex entries:

@inproceedings{ abadisemantics,

author = "Mart{\'\i}n Abadi and Mark Tuttle",

title = "A Semantics for a Logic of Authentication",

pages = "201--216",

url = "citeseer.nj.article/abadi91semantics.html",

filename = "abadi91semantics.pdf",

note = "offers a new approach to logics of beliefs, attempts to give BAN a rigorous semantics" }

@inproceedings{ syverson94unifying,

author = "P. Syverson and P. van Oorschot",

title = "On unifying some cryptographic protocol logics",

booktitle = "Proc. {IEEE} Symposium on Research in Security and Privacy",

pages = "14--28",

year = "1994",

url = "citeseer.nj.syverson94unifying.html",

filename = "syverson94unifying.pdf",

note = "states attempts to improve or expand BAN logic" }

@article{ kailar96accountability,

author = "Rajashekar Kailar",

title = "Accountability in Electronic Commerce Protocols",

journal = "{IEEE} Transactions on Software Engineering",

volume = "22",

number = "5",

year = "1996",

url = "citeseer.nj.kailar96accountability.html",

filename = "kailar96accountability.pdf" }

@inproceedings{ kindred96fast,

author = "Darrell Kindred and Jeannette Wing",

title = "Fast, Automatic Checking of Security Protocols",

pages = "41--52",

year = "1996",

url = "citeseer.nj.kindred96fast.html",

filename = "kindred96fast.pdf",

note = "RVChecker" }

@inproceedings{ mao93towards,

author = "Wenbo Mao and Colin Boyd",

title = "{Towards the Formal Analysis of Security Protocols}",

booktitle = "Proceedings of the Computer Security Foundations Workshop {VI}"

,

publisher = "IEEE Computer Society Press",

pages = "147--158",

year = "1993",

url = "citeseer.nj.mao93towards.html",

filename = "mao93towards.pdf",

note = "Mao and Boyd logic" }

@article{ boyd94limitation,

author = "Colin Boyd and Wenbo Mao",

title = "On a Limitation of {BAN} Logic",

journal = "Lecture Notes in Computer Science",

volume = "765",

pages = "240--??",

year = "1994",

url = "citeseer.nj.boyd93limitation.html",

note = "Mao and Boyd logic" }

@inproceedings{ gong90reasoning,

author = "Li Gong and Roger Needham and Raphael Yahalom",

title = "{Reasoning About Belief in Cryptographic Protocols}",

booktitle = "Proceedings 1990 {IEEE} Symposium on Research in Security and P

rivacy",

publisher = "IEEE Computer Society",

editor = "Deborah Cooper and Teresa Lunt",

pages = "234--248",

year = "1990",

url = "citeseer.nj.gong90reasoning.html",

filename = "gong90reasoning.pdf",

note = "GNY logic" }

@misc{ rgens-sg,

author = "Sigrid Gürgens",

title = "SG Logic - A Formal Analysis Technique for Authentication Protocols",

url = "citeseer.nj.337.html",

filename = "sg-logic-a-formal.pdf",

note = "SG logic" }

@misc{ craigen96using,

author = "D. Craigen and M. Saaltink",

title = "Using EVES to analyze authentication protocols",

text = "D. Craigen and M. Saaltink. Using EVES to analyze authentication protocols.

Technical Report TR96 -5508-05, ORA Canada, 1996.",

year = "1996",

url = "citeseer.nj.craigen96using.html",

filename = "craigen96using.pdf",

note = "A tool with BAN logic embedded" }

Hurdles/Obstacles:

The primary current obstacle we are addressing is the limitations of SG logic. It seems to be a logic specifically designed for E-commerce, thus we are not entirely sure how to integrate it within our comparison. If we can find out a good deal of information about SG logic it will add a new aspect to the comparison and extensions of BAN logic, otherwise we will be forced to select a different belief logic, which is an extension of BAN for the survey. Another obstacle is the lack of information/availability of the tools. This is primarily going to be a concern with SH Verification tool and RVChecker. Ideally we would like to be able to install a copy of both, however, if this proves to be too difficult there is information about the tools upon which we can rely.

Questions the survey will address:

What are the limitations of BAN which need to be fixed?

How do the different belief logics extend BAN?

Are the different belief logics extensions to BAN useful, do they solve a previous limitation?

How practical are each of the logics for industrial use?

What tools are available to support each logic?

How do the belief logics compare to each other?

................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download