M. Plath and M. D. Ryan. Feature Integration using a Feature Construct. Science of Computer Programming. 41(1), pp.53-84, 2001. Code to support the paper.
Narrative. A
feature is a post-hoc addition
made to a software system, in order to add new functionality. The
paper is the first to make formal and rigorous the idea of a feature
construct for programming and specification languages, and it enabled
industrially-relevant verification of featured telephony systems to
take place in conjunction with BT.
The research was sponsored by BT and EPSRC (GR/R02214
evaluated as outstanding).
The methods developed in the paper previously won first prize in the
open
competition at International Workshop in Feature Interaction, 2000, and
led to Ryan's 2005 co-chairship of the International
Conference on Feature Interaction.
((Not part of commentary: together with
background
conference papers, the work has had 105 citations (Google scholar).))
Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking Access Control Policies. Seventh Information Security Conference (ISC'04). Lecture Notes in Computer Science volume 3225, Springer-Verlag, 2004. 16 pages.
Narrative. Access
control systems in web-based workflow systems can become very
complicated, and it can be hard to determine whether a configuration
really denies or permits access in the intended way. This is the first
paper to bring automatic model checking techniques to the verification
of access
control policies. The paper is supported by freely downloadable tool,
and we
have used it to find flaws in access
control policies for web-based workflow systems. The work has
led to a fruitful collaboration with IBM and Ryan has received a
prestigious "IBM Faculty Award" of GBP 18,000 to carry it
forward.
((Not part of commentary: 25
citations in Google scholar.))
Nan
Zhang, Dimitar P. Guelev, and Mark Ryan. Synthesising
Verified Access
Control Systems through Model Checking. Journal of Computer
Security (in print), 2007. 58 pages.
Narrative. Access
control systems in web-based workflow systems can become very
complicated, and it can be hard to determine whether a configuration
really denies or permits access in the intended way. An
earlier conference version was the first
paper to bring automatic model checking techniques to the verification
of access
control policies. The paper is supported by freely downloadable tool,
and we
have used it to find flaws in access
control policies for web-based workflow systems. Work has
led to a fruitful collaboration with IBM and Ryan has received a
prestigious "IBM Faculty Award" of GBP 18,000 to carry it
forward.
((Not part of commentary: Conference papers of which this paper is
the culmination have 45
citations.))
Steve Kremer and Mark D. Ryan. Analysis
of an Electronic Voting Protocol in the Applied Pi Calculus. In
Proceedings of the European Symposium on Programming (ESOP'05),
Lecture Notes in Computer Science volume 3444,
pages 186-200. Springer Verlag, 2005.
Narrative. Governments
the world over are exploring systems for electronic voting. This is the
first
paper to apply formal verification techniques to verification of
electronic voting systems. The paper analysed a classical and
established electronic
voting protocol [FOO'02], and proved several properties such as vote
privacy, voter eligibility, and fairness. The paper led to the
successful EPSRC
proposal Verifying properties in
Electronic Voting Protocols (EP/E029833) to further develop this
seminal work, to Ryan's invitation to the Dagstuhl seminar Frontiers of Electronic Voting and
membership of the programme committee of Workshop on Trustworthy Elections
2006, 2007.
Narrative.Multi-party contract signing protocols provide a method for n participants to send messages to each other in order to be simultaneously bound by a contract, so as to guarantee fairness (that is, no-one is bound unless everyone is bound). Protocols for achieving this are important for e-commerce and p2p systems, but have proved notoriously difficult to obtain. We show that a 1999 protocol revised in 2004 is still flawed. In a follow-up paper, we propose a new protocol and prove it correct in a rigorous mathematical framework. Our work resolved a question which was open for 8 years.
Narrative.
Multi-party contract signing protocols provide a method for n
participants to send messages to each other in order to be
simultaneously bound by a contract, so as to guarantee
fairness (that is, no-one is bound unless everyone is bound). Protocols
for achieving this are important for e-commerce and p2p systems, but
have proved notoriously difficult to obtain. We showed that a 1999
protocol revised in 2004 is flawed. We
propose a new protocol, and prove it correct in a rigorous mathematical
framework. Our work
resolved a question which was open for 8 years.