A first-order conditional logic is considered, with semantics given by a variant of ϵ-semantics where means that 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.
M.Abadi and P.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.
2.
E.Adams, The Logic of Conditionals. Reidel, Dordrecht, Netherlands, 1975. doi:10.1007/978-94-015-7622-2.
3.
A.Atserias and J.L.Balcázar, Entailment among probabilistic relations, in: Proc. 30th IEEE Symposium on Logic in Computer Science, 2015, pp. 621–632.
4.
G.Bana, K.Hasebe and M.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.
5.
G.Barthe, B.Grégoire, S.Heraud and S.Zanella-Béguelin, Computer-aided security proofs for the working cryptographer, in: Advances in Cryptology (CRYPTO 2011), P.Rogaway, ed., Lecture Notes in Computer Science, Vol. 6841, 2011, pp. 71–90. doi:10.1007/978-3-642-22792-9_5.
6.
G.Barthe, B.Grégoire and S.Zanella-Béguelin, Formal certification of code-based cryptographic proofs, SIGPLAN Notices44(1) (2009), 90–101. doi:10.1145/1594834.1480894.
7.
G.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.
8.
M.Bellare, R.Canetti and H.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.
9.
B.Blanchet, A computationally sound mechanized prover for security protocols, in: IEEE Symposium on Security and Privacy, 2006, pp. 140–154.
10.
N.Borisov, I.Goldberg and D.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.
J.Burgess, Quick completeness proofs for some logics of conditionals, Notre Dame Journal of Formal Logic22 (1981), 76–84. doi:10.1305/ndjfl/1093883341.
A.Datta, A.Derek, J.C.Mitchell, V.Shmatikov and M.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.
A.Datta, J.Y.Halpern, J.C.Mitchell, A.Roy and S.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.
N.Friedman and J.Y.Halpern, Plausibility measures and default reasoning, Journal of the ACM48(4) (2001), 648–685. doi:10.1145/502090.502092.
17.
N.Friedman, J.Y.Halpern and D.Koller, First-order conditional logic for default reasoning revisited, ACM Trans. on Computational Logic1(2) (2000), 175–207. doi:10.1145/359496.359500.
18.
H.Geffner, High probabilities, model preference and default arguments, Mind and Machines2 (1992), 51–70.
19.
O.Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001.
20.
M.Goldszmidt, P.Morris and J.Pearl, A maximum entropy approach to nonmonotonic reasoning, IEEE Transactions of Pattern Analysis and Machine Intelligence15(3) (1993), 220–232. doi:10.1109/34.204904.
21.
M.Goldszmidt and J.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.
S.Kraus, D.Lehmann and M.Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artificial Intelligence44 (1990), 167–207. doi:10.1016/0004-3702(90)90101-5.
23.
J.Mitchell, M.Mitchell and U.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, V.Shmatikov and U.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.
D.Wagner and B.Schneier, Analysis of the SSL 3.0 protocol, in: Proc. 2nd USENIX Workshop on Electronic Commerce, 1996, pp. 29–40.
