You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Edinburgh » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Edinburgh

Return to search Previous output Next output

Output 0 of 0 in the submission

Output title

Modular verification of security protocol code by typing

Type

E - Conference contribution

DOI

10.1145/1706299.1706350

Name of conference/published proceedings

Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Volume number

Issue number

First page of article

445

ISSN of proceedings

Year of publication

2010

URL

http://dl.acm.org/citation.cfm?doid=1706299.1706350

Number of additional authors

Additional information

<10> Originality: Paper introduces modular technique of invariants for cryptographic structures for verifying cryptographic code.

Significance: Analyzes richer range of cryptographic primitives (including hybrid encryption) than previous work with F7, hence allowing F7 to beat close competitor in area (fs2pv plus ProVerif). Associated software, download site, and users:

F7 (version 2.0)

http://research.microsoft.com/en-us/downloads/c0c4ed53-cfd8-4b9c-b780-74946bd1337e/

1120 downloads (version 2.0)

Rigour: The paper includes formal correctness proofs, and also evaluation of the method on over 5000 LOC, and shows an order of magnitude performance improvement over closest competitor. Acceptance rate of POPL 2010 is 19%.

Interdisciplinary

Cross-referral requested

Research group

F - Laboratory for Foundations of Computer Science

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract