Automatic verification of temporal-epistemic properties of cryptographic protocols. (English) Zbl 1186.68105
Summary: We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and rewrite CAPSL goals as temporal-epistemic specifications. We present a compiler that implements this translation. The compiler links to the symbolic model checker MCMAS. We evaluate the technique on protocols in the Clark-Jacobs library and in the SPORE repository against custom secrecy and authentication requirements.
MSC:
| 68N20 | Theory of compilers and interpreters |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 94A60 | Cryptography |
| 94A62 | Authentication, digital signatures and secret sharing |
| 68P25 | Data encryption (aspects in computer science) |
References:
| [1] | Abadi M., Proceedings of the 10th annual ACM symposium on Principles of distributed computing (PODC’91) pp 201– |
| [2] | Armando A., Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05) 3576 pp 281– |
| [3] | AVISPA-project, AVISS – Deliverable D.6.1: List of selected problems (2005) |
| [4] | DOI: 10.1007/s10207-004-0055-7 · doi:10.1007/s10207-004-0055-7 |
| [5] | DOI: 10.1109/SECPRI.2004.1301317 · doi:10.1109/SECPRI.2004.1301317 |
| [6] | Boreale M., Proceedings of the 28th International Colloquium of Automata, Languages and Programming (ICALP’01) 2076 pp 667– · doi:10.1007/3-540-48224-5_55 |
| [7] | Boureanu I., Protocol Descriptions to Interpreted Systems, version 0.90 (2009) |
| [8] | Burrows M., A Logic of Authentication (1990) |
| [9] | DOI: 10.1007/BF00206326 · Zbl 0654.94012 · doi:10.1007/BF00206326 |
| [10] | Clark J., A Survey of Authentication Protocol Literature (1997) |
| [11] | Clark J., Clark-Jacobs library in CAPSL (1999) |
| [12] | Clarke E., Model Checking (1999) |
| [13] | Cohen M., Proceedings of the 22nd Symposium on Logic in Computer Science (LICS’07) pp 77– |
| [14] | Corin R., Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P’06) pp 155– |
| [15] | Denker G., Proceedings of DARPA Information Survivability Conference (DISCEX’00) pp 207– |
| [16] | DOI: 10.1109/TIT.1983.1056650 · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650 |
| [17] | Fagin R., Reasoning about Knowledge (1995) |
| [18] | Halpern J., Proceedings of the Workshop on Formal Aspects of Security (FASec’02) 2629 pp 115– · doi:10.1007/978-3-540-40981-6_11 |
| [19] | DOI: 10.3233/JCS-2003-11405 · doi:10.3233/JCS-2003-11405 |
| [20] | DOI: 10.3233/JCS-2003-11204 · doi:10.3233/JCS-2003-11204 |
| [21] | Kacprzak M., Fundamenta Informaticae 72 (1) pp 215– (2006) |
| [22] | Kacprzak M., Fundamenta Informaticae 85 (1) pp 313– (2008) |
| [23] | DOI: 10.1145/142854.142872 · doi:10.1145/142854.142872 |
| [24] | Laboratoire Spécification et Vérification ENS Cachan, SPORE: Security Protocols Open Repository (2003) |
| [25] | Lomuscio A., Fundamenta Informaticae 85 pp 359– (2008) |
| [26] | Lomuscio A., Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09) 5643 pp 682– |
| [27] | Lomuscio A., Fundamenta Informaticae 79 (3) pp 473– (2007) |
| [28] | Lowe G., Proceedings of the 9th IEEE workshop on Computer Security Foundations (CSFW’96) pp 162– |
| [29] | DOI: 10.3233/JCS-1998-61-204 · doi:10.3233/JCS-1998-61-204 |
| [30] | DOI: 10.1016/0743-1066(95)00095-X · Zbl 0871.68052 · doi:10.1016/0743-1066(95)00095-X |
| [31] | Meyden R., Proceedings of 16th International Conference on Computer Aided Verification (CAV’04) 3114 pp 479– |
| [32] | Meyden R., Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW’04) pp 280– |
| [33] | Millen J., Common Authentification Protocol Specification Language (2001) |
| [34] | DOI: 10.1145/359657.359659 · Zbl 0387.68003 · doi:10.1145/359657.359659 |
| [35] | v. Oheimb D., Proceedings of International Summer School On Applied Semantics (APPSEM’05) |
| [36] | DOI: 10.1007/3-540-15648-8_21 · doi:10.1007/3-540-15648-8_21 |
| [37] | Paulson L., Proceeding of the IEEE Symposium on Logic in Computer Science (LICS’99) 1999 pp 370– |
| [38] | Pucella R., Proceedings of the 15th Computer Security Foundations Workshop (CSFW’02) pp 282– |
| [39] | Ramanujam R., Proceedings of theWorkshop on Issues in the Theory of Security (WITS’03) pp 11– |
| [40] | Ramanujam R., Undecidability of secrecy for security protocols (2003) |
| [41] | Rusinowitch M., Proceedings of the 14th IEEE Workshop on Computer Security Foundations (CSFW’01) pp 174– |
| [42] | Syverson P., Proceedings of the International School on Foundations of Security Analysis and Design (FOSAD’00) 2170 pp 63– |
| [43] | Syverson P., Proceedings of the Wold Congress on Formal Methods (FM’99) in the Development of Computing Systems pp 814– |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
