From qualitative to quantitative proofs of security properties using first-order conditional logic 1

Abstract

A first-order conditional logic is considered, with semantics given by a variant of ϵ-semantics where $φ \to ψ$ means that $Pr (ψ | φ)$ approaches 1 super-polynomially – faster than any inverse polynomial. This type of convergence is needed for reasoning about security protocols. A complete axiomatization is provided for this semantics, and it is shown how a qualitative proof of the correctness of a security protocol can be automatically converted to a quantitative proof appropriate for reasoning about concrete security.

Keywords

Qualitative security quantitative security conditional logic epsilon semantics

Get full access to this article

View all access options for this article.

References

Abadi and

Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), in: Proc. IFIP International Conference on Theoretical Computer Science (TCS’00), Lecture Notes in Computer Science, Vol. 1872, Springer-Verlag, 2000, pp. 3–22.

Adams, The Logic of Conditionals. Reidel, Dordrecht, Netherlands, 1975. doi:10.1007/978-94-015-7622-2.

Atserias and

J.L.

Balcázar, Entailment among probabilistic relations, in: Proc. 30th IEEE Symposium on Logic in Computer Science, 2015, pp. 621–632.

Bana,

Hasebe and

Okada, Computationally complete symbolic attacker and key exchange, in: Proc. 13th ACM SIGSAC Conference on Computer and Communications Security (CCS ’13), 2013, pp. 1231–1246.

Barthe,

Grégoire,

Heraud and

Zanella-Béguelin, Computer-aided security proofs for the working cryptographer, in: Advances in Cryptology (CRYPTO 2011),

Rogaway, ed., Lecture Notes in Computer Science, Vol. 6841, 2011, pp. 71–90. doi:10.1007/978-3-642-22792-9_5.

Barthe,

Grégoire and

Zanella-Béguelin, Formal certification of code-based cryptographic proofs, SIGPLAN Notices 44(1) (2009), 90–101. doi:10.1145/1594834.1480894.

Bella and

L.C.

Paulson, Kerberos version IV: Inductive analysis of the secrecy goals, in: Proc. 5th European Symposium on Research in Computer Security,

J.-J.

Quisquater, ed., LNCS, Vol. 1485, Springer-Verlag, 1998, pp. 361–375.

Bellare,

Canetti and

Krawczyk, A modular approach to the design and analysis of authentication and key exchange protocols, in: Proc. 30th Annual Symposium on the Theory of Computing, 1998, pp. 419–428.

Blanchet, A computationally sound mechanized prover for security protocols, in: IEEE Symposium on Security and Privacy, 2006, pp. 140–154.

10.

Borisov,

Goldberg and

Wagner, Intercepting mobile communications: The insecurity of 802.11, in: Proc. 7th Annual International Conference on Mobile Computing and Networking, 2001, pp. 180–189.

11.

Burgess, Quick completeness proofs for some logics of conditionals, Notre Dame Journal of Formal Logic 22 (1981), 76–84. doi:10.1305/ndjfl/1093883341.

12.

Datta,

Derek,

J.C.

Mitchell and

Roy, Protocol composition logic (PCL), Electronic Notes Theoretical Computer Science 172 (2007), 311–358. doi:10.1016/j.entcs.2007.02.012.

13.

Datta,

Derek,

J.C.

Mitchell,

Shmatikov and

Turuani, Probabilistic polynomial-time semantics for a protocol security logic, in: 32nd International Colloquium on Automata, Languages, and Programming (ICALP), 2005, pp. 16–29. doi:10.1007/11523468_2.

14.

Datta,

J.Y.

Halpern,

J.C.

Mitchell,

Roy and

Sen, A symbolic logic with concrete bounds for cryptographic protocols, 2015, Available at: http://arxiv.org/abs/1511.07536.

15.

H.B.

Enderton, A Mathematical Introduction to Logic, Academic Press, New York, 1972.

16.

Friedman and

J.Y.

Halpern, Plausibility measures and default reasoning, Journal of the ACM 48(4) (2001), 648–685. doi:10.1145/502090.502092.

17.

Friedman,

J.Y.

Halpern and

Koller, First-order conditional logic for default reasoning revisited, ACM Trans. on Computational Logic 1(2) (2000), 175–207. doi:10.1145/359496.359500.

18.

Geffner, High probabilities, model preference and default arguments, Mind and Machines 2 (1992), 51–70.

19.

Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001.

20.

Goldszmidt,

Morris and

Pearl, A maximum entropy approach to nonmonotonic reasoning, IEEE Transactions of Pattern Analysis and Machine Intelligence 15(3) (1993), 220–232. doi:10.1109/34.204904.

21.

Goldszmidt and

Pearl, Rank-based systems: A simple approach to belief revision, belief update and reasoning about evidence and actions, in: Principles of Knowledge Representation and Reasoning: Proc. Third International Conference (KR ’92), 1992, pp. 661–672.

22.

Kraus,

Lehmann and

Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artificial Intelligence 44 (1990), 167–207. doi:10.1016/0004-3702(90)90101-5.

23.

Mitchell,

Mitchell and

Stern, Automated analysis of cryptographic protocols using Murφ, in: Proc. 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1997, pp. 141–151. doi:10.1109/SECPRI.1997.601329.

24.

J.C.

Mitchell,

Shmatikov and

Stern, Finite-state analysis of SSL 3.0, in: Proc. Seventh USENIX Security Symposium, 1998, pp. 201–216.

25.

L.C.

Paulson, Isabelle, a Generic Theorem Prover, Lecture Notes in Computer Science, Vol. 828, Springer-Verlag, 1994.

26.

Wagner and

Schneier, Analysis of the SSL 3.0 protocol, in: Proc. 2nd USENIX Workshop on Electronic Commerce, 1996, pp. 29–40.