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

Koji Hasebe, Mitsuhiro Okada

研究成果: Article査読

2 被引用数 (Scopus)


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.

ジャーナルElectronic Notes in Theoretical Computer Science
出版ステータスPublished - 2006 1 31

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)


「Completeness and counter-example generations of a basic protocol logic: (Extended abstract)」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。