Completeness and counter-example generations of a basic protocol logic: (Extended abstract)

Koji Hasebe, Mitsuhiro Okada

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a "trace" any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.

Original languageEnglish
Pages (from-to)73-92
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Volume147
Issue number1
DOIs
Publication statusPublished - 2006 Jan 31

Fingerprint

Counterexample
Completeness
Query
Logic
Network protocols
Formal Semantics
Inference Rules
Trace
Semantics
Proof Search
Computability and decidability
Predicate Logic
Security Protocols
Deduction
First-order Logic
Decidability
Search Methods
Axioms
Immediately
Correctness

Keywords

  • Agreement properties
  • First-order predicate logic
  • Proof-search method
  • Security protocol analysis

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Completeness and counter-example generations of a basic protocol logic : (Extended abstract). / Hasebe, Koji; Okada, Mitsuhiro.

In: Electronic Notes in Theoretical Computer Science, Vol. 147, No. 1, 31.01.2006, p. 73-92.

Research output: Contribution to journalArticle

@article{939b30a329934ec096781cb6f138c01f,
title = "Completeness and counter-example generations of a basic protocol logic: (Extended abstract)",
abstract = "We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a {"}trace{"} any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.",
keywords = "Agreement properties, First-order predicate logic, Proof-search method, Security protocol analysis",
author = "Koji Hasebe and Mitsuhiro Okada",
year = "2006",
month = "1",
day = "31",
doi = "10.1016/j.entcs.2005.06.038",
language = "English",
volume = "147",
pages = "73--92",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Completeness and counter-example generations of a basic protocol logic

T2 - (Extended abstract)

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2006/1/31

Y1 - 2006/1/31

N2 - We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a "trace" any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.

AB - We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a "trace" any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.

KW - Agreement properties

KW - First-order predicate logic

KW - Proof-search method

KW - Security protocol analysis

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

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

U2 - 10.1016/j.entcs.2005.06.038

DO - 10.1016/j.entcs.2005.06.038

M3 - Article

AN - SCOPUS:30844435683

VL - 147

SP - 73

EP - 92

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -