A logical verification method for security protocols based on linear logic and BAN logic

Koji Hasebe, Mitsuhiro Okada

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov [4], while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham [2]) is used as an evaluation semantics on security-properties for processes. By this method, we can get rid of the so called "idealization" step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting. We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.

Original languageEnglish
Pages (from-to)417-440
Number of pages24
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2609
Publication statusPublished - 2003

Fingerprint

Linear Logic
Security Protocols
Logic
Network protocols
Semantics
Syntactics
Evaluation
Concretes
Formal Proof
Multiset
Expressive Power
Rewriting
Fragment
Classify
Evaluate

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

@article{0f90a4e5ac7841ffb591b8a1264e8363,
title = "A logical verification method for security protocols based on linear logic and BAN logic",
abstract = "A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov [4], while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham [2]) is used as an evaluation semantics on security-properties for processes. By this method, we can get rid of the so called {"}idealization{"} step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting. We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.",
author = "Koji Hasebe and Mitsuhiro Okada",
year = "2003",
language = "English",
volume = "2609",
pages = "417--440",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - A logical verification method for security protocols based on linear logic and BAN logic

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2003

Y1 - 2003

N2 - A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov [4], while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham [2]) is used as an evaluation semantics on security-properties for processes. By this method, we can get rid of the so called "idealization" step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting. We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.

AB - A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov [4], while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham [2]) is used as an evaluation semantics on security-properties for processes. By this method, we can get rid of the so called "idealization" step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting. We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.

UR - http://www.scopus.com/inward/record.url?scp=35048859061&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048859061&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:35048859061

VL - 2609

SP - 417

EP - 440

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -