TY - GEN

T1 - Computational semantics for first-order logical analysis of cryptographic protocols

AU - Bana, Gergei

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2009/7/16

Y1 - 2009/7/16

N2 - This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.

AB - This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.

KW - Computational semantics

KW - Cryptographic protocols

KW - First order logic

KW - Formal methods

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

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

U2 - 10.1007/978-3-642-02002-5_3

DO - 10.1007/978-3-642-02002-5_3

M3 - Conference contribution

AN - SCOPUS:67650269836

SN - 9783642020018

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 33

EP - 56

BT - Formal to Practical Security

ER -