Abstract | ||
---|---|---|
In this paper we present by a case study an approach to the verification of security protocols based on Abductive Logic Programming. We start from the perspective of open multi-agent systems, where the internal architecture of the individual system's components may not be completely specified, but it is important to infer and prove properties about the overall system behaviour. We take a formal approach based on Computational Logic, to address verification at two orthogonal levels: ‘static' verification of protocol properties (which can guarantee, at design time, that some properties are a logical consequence of the protocol), and ‘dynamic' verification of compliance of agent communication (which checks, at runtime, that the agents do actually follow the protocol). In order to explain the approach, we adopt as a running example the well-known Needham-Schroeder protocol. We first show how the protocol can be specified in our previously developed SOCS-SI framework, and then demonstrate the two types of verification. We also demonstrate the use of the SOCS-SI framework for the static verification of the NetBill e-commerce protocol. |
Year | DOI | Venue |
---|---|---|
2005 | 10.1007/11759683_7 | ESAW |
Keywords | Field | DocType |
abductive logic programming,individual system,computational logic,protocol property,well-known needham-schroeder protocol,socs-si framework,static verification,netbill e-commerce protocol,security protocol,formal approach,case study,security protocols verification | Functional verification,Programming language,Cryptographic protocol,Intelligent verification,Computer science,Runtime verification,Abductive logic programming,Artificial intelligence,Formal methods,High-level verification,Software verification | Conference |
Volume | ISSN | ISBN |
3963 | 0302-9743 | 3-540-34451-9 |
Citations | PageRank | References |
10 | 0.57 | 23 |
Authors | ||
6 |
Name | Order | Citations | PageRank |
---|---|---|---|
marco alberti | 1 | 467 | 30.93 |
federico chesani | 2 | 801 | 46.41 |
Marco Gavanelli | 3 | 596 | 48.07 |
Evelina Lamma | 4 | 1268 | 109.21 |
Paola Mello | 5 | 444 | 21.33 |
Paolo Torroni | 6 | 1167 | 80.57 |