AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
There has been substantial research on other proof methods for security protocols. While many of those proof methods have focused on predicates on behaviors, others have addressed equivalences between systems

Automated verification of selected equivalences for security protocols

The Journal of Logic and Algebraic Programming, no. 1 (2008): 331-340

Cited by: 456|Views114
EI WOS

Abstract

In the analysis of security protocols, methods and tools for reasoning about protocol behaviors have been quite effective. We aim to expand the scope of those methods and tools. We focus on proving equivalences P ≈ Q in which P and  Q are two processes that differ only in the choice of some terms. These equivalences arise often in applica...More

Code:

Data:

0
Introduction
  • Many security properties can be expressed as predicates on system behaviors. These properties include some kinds of secrecy properties (for instance, “the system never broadcasts the key k”).
  • Many security properties can be expressed as predicates on system behaviors
  • These properties include some kinds of secrecy properties.
  • The authors aim to apply them to important security properties that have been hard to prove and that cannot be phrased as predicates on system behaviors.
  • Many such properties can be written as equivalences.
  • A priori, P ≈ Q is not a simple predicate on the behaviors of P or Q
Highlights
  • Many security properties can be expressed as predicates on system behaviors
  • Such predicates on system behaviors are the focus of many successful methods for security analysis
  • We have proved that four variants of Encrypted Key Exchange [9, 10] are resistant to off-line guessing attacks
  • There has been substantial research on other proof methods for security protocols. While many of those proof methods have focused on predicates on behaviors, others have addressed equivalences between systems (e.g., [1, 4,5,6, 14,15,16,17,18,19,20,21, 24])
  • We show how to derive equivalences by reasoning about behaviors— by reasoning about behaviors of applied pi calculus biprocesses
Conclusion
  • There has been substantial research on other proof methods for security protocols.
  • Much of this research is concerned with obtaining sound and complete proof systems, often via sophisticated bisimulations, and eventually decision algorithms for restricted cases.
  • In the opinion, these are important goals, and the results to date are significant.
  • The authors demonstrate the usefulness of the method through automated analyses of interesting, infinite-state systems
Funding
  • Martın Abadi’s work was partly done at Microsoft Research, Silicon Valley, and also partly supported by the National Science Foundation under Grants CCR-0204162 and CCR-0208800
Reference
  • M. Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749–786, Sept. 1999.
    Google ScholarLocate open access versionFindings
  • M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102–146, Jan. 2005.
    Google ScholarLocate open access versionFindings
  • M. Abadi, B. Blanchet, and C. Fournet. Just Fast Keying in the Pi Calculus. In ESOP’04, volume 2986 of LNCS, pages 340–354. Springer, Mar. 2004.
    Google ScholarLocate open access versionFindings
  • M. Abadi and C. Fournet. Mobile Values, New Names, and Secure Communication. In POPL’01, pages 104–115. ACM Press, Jan. 2001.
    Google ScholarLocate open access versionFindings
  • M. Abadi and A. D. Gordon. A Bisimulation Method for Cryptographic Protocols. Nordic Journal of Computing, 5(4):267–303, Winter 1998.
    Google ScholarLocate open access versionFindings
  • M. Abadi and A. D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation, 148(1):1–70, Jan. 1999.
    Google ScholarLocate open access versionFindings
  • W. Aiello, S. M. Bellovin, M. Blaze, R. Canetti, J. Ioannidis, K. Keromytis, and O. Reingold. Just Fast Keying: Key Agreement in a Hostile Internet. ACM TISSEC, 7(2):242– 273, May 2004.
    Google ScholarLocate open access versionFindings
  • X. Allamigeon and B. Blanchet. Reconstruction of Attacks against Cryptographic Protocols. In CSFW-18, June 2005.
    Google ScholarLocate open access versionFindings
  • S. M. Bellovin and M. Merritt. Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks. In Security and Privacy, pages 72–84, May 1992.
    Google ScholarLocate open access versionFindings
  • S. M. Bellovin and M. Merritt. Augmented Encrypted Key Exchange: a Password-Based Protocol Secure Against Dictionary Attacks and Password File Compromise. In CCS’93, pages 244–250, Nov. 1993.
    Google ScholarLocate open access versionFindings
  • B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In CSFW-14, pages 82–96, June 2001. Springer, Sept. 2002.
    Google ScholarLocate open access versionFindings
  • [13] B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In Security and Privacy, pages 86–100, May 2004.
    Google ScholarLocate open access versionFindings
  • [14] M. Boreale, R. De Nicola, and R. Pugliese. Proof Techniques for Cryptographic Processes. SIAM Journal on Computing, 31(3):947–986, 2002.
    Google ScholarLocate open access versionFindings
  • [15] J. Borgstrom, S. Briais, and U. Nestmann. Symbolic Bisimulation in the Spi Calculus. In CONCUR 2004, volume 3170 of LNCS, pages 161–176. Springer, Aug. 2004.
    Google ScholarLocate open access versionFindings
  • [16] J. Borgstrom and U. Nestmann. On Bisimulations for the Spi Calculus. In AMAST 2002, volume 2422 of LNCS, pages 287–303.
    Google ScholarLocate open access versionFindings
  • [17] V. Cortier. Verification Automatique des Protocoles Cryptographiques. PhD thesis, ENS de Cachan, Mar. 2003.
    Google ScholarFindings
  • [18] L. Durante, R. Sisto, and A. Valenzano. Automatic Testing Equivalence Verification of Spi Calculus Specifications. ACM TOSEM, 12(2):222–284, Apr. 2003.
    Google ScholarLocate open access versionFindings
  • [19] R. Focardi and R. Gorrieri. The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering, 23(9):550–571, Sept. 1997.
    Google ScholarLocate open access versionFindings
  • [20] H. Huttel. Deciding Framed Bisimilarity. In INFINITY’02, pages 1–20, Aug. 2002.
    Google ScholarLocate open access versionFindings
  • [21] P. D. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic Polynomial-time Equivalence and Security Protocols. In FM’99, volume 1708 of LNCS, pages 776–793. Springer, Sept. 1999.
    Google ScholarLocate open access versionFindings
  • [22] F. Pottier. A Simple View of Type-Secure Information Flow in the π-Calculus. In CSFW-15, pages 320–330, June 2002.
    Google ScholarLocate open access versionFindings
  • [23] F. Pottier and V. Simonet. Information Flow Inference for ML. In POPL’02, pages 319–330, Jan. 2002.
    Google ScholarLocate open access versionFindings
  • [24] A. Ramanathan, J. Mitchell, A. Scedrov, and V. Teague. Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols. In FOSSACS 2004, volume 2987 of LNCS, pages 468–483.
    Google ScholarLocate open access versionFindings
Author
Bruno Blanchet
Bruno Blanchet
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科