
arXiv: 0910.4053
Model checking is an automatic verification technique to verify hardware and software systems. However it suffers from state-space explosion problem. In this paper we address this problem in the context of cryptographic protocols by proposing a security property-dependent heuristic. The heuristic weights the state space by exploiting the security formulae; the weights may then be used to explore the state space when searching for attacks.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Cryptography and Security, Computer Science - Programming Languages, QA75.5-76.95, Logic in Computer Science (cs.LO), Electronic computers. Computer science, QA1-939, Cryptography and Security (cs.CR), Mathematics, Programming Languages (cs.PL)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Cryptography and Security, Computer Science - Programming Languages, QA75.5-76.95, Logic in Computer Science (cs.LO), Electronic computers. Computer science, QA1-939, Cryptography and Security (cs.CR), Mathematics, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
