Name
Abstract | ||
|---|---|---|
Meadows has shown how availability issues involving security protocols may be treated by analyzing the time-consuming internal actions of agents with respect to failstop criteria that are cost dependent.In this paper we present a technique which combines Paulson's inductive approach to protocol analysis with Interval Logic in order to create a verification tool that supports analysis of the kind Meadows proposes.Based on a novel notion of packets and a redefined notion of external events we develop theoretical extensions that enable the inductive analysis method to distinguish active attacks . To supplement the global traces of external events we define an inductive theory of (untimed) local traces of internal actions. Notions of timed global traces and timed local traces are introduced and used to develop a method that allows natural modelling of real-time (cost) properties of security protocols.Proof support for the theory developed here is achieved via encoding in Isabelle/ LSILHOL, an Isabelle/HOL environment for (labelled) interval logics. Some small examples of protocols are treated and properties are shown via interactive theorem proving. |
Year | Venue | Keywords |
|---|---|---|
2003 | Nord. J. Comput. | external event,inductive theory,protocol analysis,inductive analysis method,internal action,global trace,local trace,security protocol,inductive approach,Interval Logic,availability property |
Field | DocType | Volume |
HOL,Discrete mathematics,Programming language,Protocol analysis,Cryptographic protocol,Interval temporal logic,Computer science,Network packet,Theoretical computer science,Encoding (memory),Proof assistant | Journal | 10 |
Issue | Citations | PageRank |
4 | 2 | 0.39 |
References | Authors | |
11 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| henrik pilegaard | 1 | 100 | 7.73 |
| Michael r. Hansen | 2 | 543 | 43.29 |
| r t sharp | 3 | 33 | 3.65 |