@techreport{Cor05a,
	author = {R. Corin and S. Etalle and A. Saptawijaya},
	title = {{PS-LTL} for Constraint-based Security Protocol Analysis},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {to appear},
	month = {Jun},
	year = {2005},
	annote = {group DIES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project PAW},
	annote = {abstract We introduce PS-LTL (pronounced pastel ), a pure-past security linear temporal logic. PSLTL allows the specification of several security properties including data freshness and different notions of authentication and secrecy. We give semantics and further propose a procedure to decide validity of properties for finite (albeit symbolic) execution traces, for a relevant subset (which includes the mentioned properties) of PS-LTL . Our procedure is easily integrated with constraint-based protocol analysis approaches. We also provide a Prolog implementation.}}
@techreport{Eta05a,
	author = {S. Etalle and W. H. Winsborough},
	title = {Integrity Constraints in Trust Management},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {to appear},
	month = {Apr},
	year = {2005},
	url = {http://arxiv.org/abs/cs.CR/0503061},
	annote = {group DIES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Inspired},
	annote = {abstract We introduce the use, monitoring, and enforcement of integrity constraints in trust managementstyle authorization systems. We consider what portions of the policy state must be monitored to detect violations of integrity constraints. Then we address the fact that not all participants in a trust management system can be trusted to assist in such monitoring, and show how many integrity constraints can be monitored in a conservative manner so that trusted participants detect and report if the system enters a policy state from which evolution in unmonitored portions of the policy could lead to a constraint violation.}}
@techreport{Law05b,
	author = {Y. W. Law and P. H. Hartel and S. Etalle and P. J. M. Havinga and R. di Pietro and L. V. Mancini},
	title = {Overview of Security Research in {EYES}},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {TR-CTIT-05-06},
	month = {Feb},
	year = {2005},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/00000120.pdf},
	annote = {group CADTES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Eyes},
	annote = {abstract The security research for the EYES project is mainly carried out by the the Univ. of Rome La Sapienza and the Univ. of Twente. While Rome is primarily interested in key management, Twente has been involved with an assortment of topics such as key management, cryptographic primitives and link-layer security. This document gives an overview of the research output of these two groups for the past 3 years.}}
@inproceedings{2004:CCE+,
	author = {R. Corin and G. Di Caprio and S. Etalle and S. Gnesi and G. Lenzini and C. Moiso},
	title = {Security Analysis of Parlay/{OSA} Framework},
	booktitle = {9th Int. Conf. on Intelligence in service delivery Networks {ICIN}},
	editor = {B. Villain},
	publisher = {IOS Press, Amsterdam},
	address = {Bordeaux, France},
	month = {Oct},
	year = {2004},
	pages = {54-59},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/00000108.pdf},
	annote = {group DIES},
	annote = {isbn not assigned},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project BRICKS},
	annote = {abstract This paper analyzes the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Architectures based on Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, to those network capabilities offered by the network operator. Role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and use the network capabilities features offered. For this reason potential security flaws in its authentication strategy can bring to unauthorized use of network with evident damages to the operator and to the quality of the services. This paper shows how a rigorous formal analysis of TSM underlines serious weaknesses in the model describing its authentication procedure. This usually means that also the original system (i.e., the TSM protocol itself) hides the same flaws. The paper relates about the design activity of the formal model, the tool-aided verification performed and the security flaws discovered. This will allow us to discuss about how the security of the TSM protocol can be generally improved.}}
@inproceedings{Cho04a,
	author = {C. N. Chong and B. Ren and J. M. Doumen and S. Etalle and P. H. Hartel and R. Corin},
	title = {License protection with a tamper-resistant token},
	booktitle = {5th Workshop on Information Security Applications ({WISA})},
	volume = {LNCS 3325},
	editor = {C.-H. Lim and M. Yung},
	publisher = {Springer-Verlag, Berlin},
	address = {Jeju Island, Korea},
	month = {Aug},
	year = {2004},
	pages = {223-237},
	url = {http://dx.doi.org/10.1007/b103174},
	annote = {group DIES},
	annote = {isbn 3-540-24015-2},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract Content protection mechanisms are intended to enforce the usage rights on the content. These usage rights are carried by a license. Sometimes, a license even carries the key that is used to unlock the protected content. Unfortunately, license protection is difficult, yet it is important for digital rights management (DRM). Not many license protection schemes are available, and most if not all are proprietary. We present a license protection scheme, which exploits tamper-resistant cryptographic hardware. The confidentiality and integrity of the license or parts thereof can be assured with our protection scheme. In addition, the keys to unlock the protected content are always protected and stored securely as part of the license. We verify secrecy and authentication aspects of one of our protocols. We implement the scheme in a prototype to assess the performance.}}
@inproceedings{Cor03e,
	author = {R. Corin and J. M. Doumen and S. Etalle},
	title = {Analysing Password Protocol Security Against Off-line Dictionary Attacks},
	booktitle = {2nd Int. Workshop on Security Issues with Petri Nets and other Computational Models ({WISP})},
	volume = {121},
	editor = {N. Busi and R. Gorrieri and F. Martinelli},
	publisher = {Electronic Notes in Theoretical Computer Science (ENTCS), 121},
	address = {Bologna, Italy},
	month = {Jun},
	year = {2004},
	pages = {47-63},
	url = {http://dx.doi.org/10.1016/j.entcs.2004.10.007},
	annote = {group DIES},
	annote = {issn 1571-0661},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract  We study the security of password protocols against off-line dictionary attacks. In addition to the standard adversary abilities, we also consider further cryptographic advantages given to the adversary when considering the password protocol being instantiated with particular encryption schemes. We work with the applied pi-calculus of Abadi and Fournet, in which the (new) adversary abilities are modelled as equations between terms. As case studies, we analyse the Encrypted Password Transmission (EPT) protocol of Halevi and Krawczyk, and the wellknown Encrypted Key (EKE) of Bellovin and Merritt. In the latter, we find an attack that arises when considering the ability of distinguishing ciphertexts from random noise. We propose a modification to EKE that prevents this attack.}}
@inproceedings{Cor04,
	author = {R. Corin and S. Etalle and P. H. Hartel and A. Mader},
	title = {Timed Model Checking of Security Protocols},
	booktitle = {2nd {ACM} Workshop on Formal Methods in Security Engineering: From Specifications to Code ({FMSE})},
	editor = {V. Atluri and M. Backes and D. Basin and M. Waidner},
	publisher = {ACM Press, New York},
	address = {Fairfax, Virginia},
	month = {Oct},
	year = {2004},
	pages = {23-32},
	url = {http://doi.acm.org/10.1145/1029133.1029137},
	annote = {group DIES},
	annote = {isbn 1-58113-971-3},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project BRICKS},
	annote = {abstract We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.}}
@inproceedings{Cor04b,
	author = {R. Corin and S. Etalle and J. I. den Hartog and G. Lenzini and I. Staicu},
	title = {{A} Logic for Auditing Accountability in Decentralized Systems},
	booktitle = {2nd Int. Workshop on Formal Aspect of Security and Trust ({FAST})},
	volume = {IFIP 173},
	editor = {T. Dimitrakos and F. Martinelli},
	publisher = {Springer-Verlag, Berlin},
	address = {Toulouse, France},
	month = {Aug},
	year = {2004},
	pages = {187-202},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000fe.pdf},
	annote = {group DIES},
	annote = {isbn 0-387-24050-0},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Inspired},
	annote = {abstract We propose a language that allows agents to distribute data with usage policies in a decentralized architecture. In our framework, the compliance with usage policies is not enforced. However, agents may be audited by an authority at an arbitrary moment in time. We design a logic that allows audited agents to prove their actions, and to prove their authorization to posses particular data. Accountability is defined in several flavors, including agent accountability and data accountability. Finally, we show the soundness of the logic.}}
@inproceedings{Har04,
	author = {P. H. Hartel and P. van Eck and S. Etalle and R. J. Wieringa},
	title = {Modelling mobility aspects of security policies},
	booktitle = {Construction and Analysis of Safe, Secure and Interoperable Smart cards ({CASSIS})},
	volume = {LNCS 3362},
	editor = {G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean},
	publisher = {Springer-Verlag, Berlin},
	address = {Marseille, France},
	month = {Mar},
	year = {2004},
	pages = {172-191},
	url = {http://dx.doi.org/10.1007/b105030},
	annote = {group IS},
	annote = {isbn 3-540-24287-2},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Inspired},
	annote = {abstract Security policies are rules that constrain the behaviour of a system. Different, largely unrelated sets of rules typically govern the physical and logical worlds. However, increased hardware and software mobility forces us to consider those rules in an integrated fashion. We present SPIN models of four case studies where mobility plays a role. In each case the model captures both the system of interest and its security policy. The model is then formally checked against a property that represents a principle from the problem domain. The model checking activity shows many examples of policies that are too weak to cope with mobility.}}
@inproceedings{Law03a,
	author = {Y. W. Law and C. N. Chong and S. Etalle and P. H. Hartel and R. Corin},
	title = {Licensing Structured Data with Ease},
	booktitle = {2nd {IFIP} {TC6} {WG6.11} Int. Workshop for Technology, Economy, Social and Legal Aspects of Virtual Goods},
	publisher = {Technical Univ. Ilmenau, Germany},
	address = {Ilmenau, Germany},
	month = {May},
	year = {2004},
	pages = {Paper 11},
	url = {http://virtualgoods.tu-ilmenau.de/2004/law04licensing.pdf},
	annote = {group DIES},
	annote = {isbn not assigned},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract In response to the need of a rights expression language (REL), we have proposed LicenseScript, an REL based on multiset rewriting and Prolog. LicenseScript has advantage over existing RELs, in the sense that it has a well-defined semantics. In fact besides semantics, LicenseScript has a lot of other advantages over other RELs. The mission of this paper is twofold: (1) to put a spotlight on these advantages, (2) at the same time justifying some of our design rationales in LicenseScript. We accomplish this by giving examples of licensing models that are greatly facilitated by the use of Prolog as a component of LicenseScript. At the same time showing how LicenseScript makes these non-trivial models viable, we also make LicenseScript a stronger case than it previously might have occurred to be.}}
@techreport{Cor04a,
	author = {R. Corin and S. Etalle},
	title = {{A} simple procedure for finding guessing attacks (Extended Abstract)},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {TR-CTIT-04-23},
	month = {Jun},
	year = {2004},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000fa.pdf},
	annote = {group DIES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {abstract A novel procedure for finding guessing attacks in security protocols is presented. The procedure enjoys a simple and intuitive definition, and is easily implementable.}}
@article{Eta03,
	author = {S. Etalle and S. Mukhopadhyay and A. Roychoudhury (Eds.)},
	title = {Int. Workshop on Software Verification and Validation ({SVV})},
	journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
	volume = {118},
	pages = {1},
	month = {Dec},
	year = {2003},
	url = {http://dx.doi.org/10.1016/j.entcs.2004.10.004},
	annote = {group DIES},
	annote = {issn 1571-0661},
	annote = {topic Security},
	annote = {program ISTRICE}}
@inproceedings{Cho03,
	author = {C. N. Chong and R. Corin and S. Etalle and P. H. Hartel and Y. W. Law},
	title = {{LicenseScript}: {A} Novel Digital Rights Language},
	booktitle = {{IFIP} {TC6} {WG6.11} Int. Workshop for Technology, Economy, Social and Legal Aspects of Virtual Goods},
	editor = {R. Grimm and J. Nitzel},
	publisher = {Technical Univ. Ilmenau, Germany},
	address = {Ilmenau, Germany},
	month = {May},
	year = {2003},
	pages = {104-115},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000ba.pdf},
	annote = {group DIES},
	annote = {isbn not assigned},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract We propose LicenseScript as a new multi-set rewriting/logic based language for expressing dynamic conditions of use of digital assets such as music, video or private data. LicenseScript differs from the other DRM languages in that it caters for the intentional but legal manipulation of data. We believe this feature is the answer to providing the flexibility needed to support emerging usage paradigms of digital data.}}
@inproceedings{Cho03a,
	author = {C. N. Chong and R. Corin and S. Etalle and P. H. Hartel and W. Jonker and Y. W. Law},
	title = {{LicenseScript}: {A} Novel Digital Rights Language and its Semantics},
	booktitle = {3rd Int. Conf. on Web Delivering of Music ({WEDELMUSIC})},
	editor = {K. Ng and C. Busch and P. Nesi},
	publisher = {IEEE Computer Society Press, Los Alamitos, California},
	address = {Leeds, UK},
	month = {Sep},
	year = {2003},
	pages = {122-129},
	url = {http://doi.ieeecomputersociety.org/10.1109/WDM.2003.1233885},
	annote = {group DB},
	annote = {isbn 0-7695-1935-0},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract We propose LicenseScript as a new multiset rewriting/ logic based language for expressing dynamic conditions of use of digital assets such as music, video or private data. LicenseScript differs from other DRM languages in that it caters for the intentional but legal manipulation of data. We believe this feature is the answer to providing the flexibility needed to support emerging usage paradigms of digital data. We provide the language with a simple semantics based on traces.}}
@inproceedings{Cho03c,
	author = {C. N. Chong and S. Etalle and P. H. Hartel},
	title = {Comparing Logic-based and {XML-based} Rights Expression Languages},
	booktitle = {Confederated Int. Workshops: On The Move to Meaningful {Internet} Systems ({OTM})},
	volume = {LNCS 2889},
	editor = {R. Meersman and Z. Tari},
	publisher = {Springer-Verlag, Berlin},
	address = {Catania, Sicily, Italy},
	month = {Nov},
	year = {2003},
	pages = {779-792},
	url = {http://www.springerlink.com/link.asp?id=fptbu7l1xtwpl6ae},
	annote = {group DIES},
	annote = {isbn 3-540-20494-6},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract Several rights expression languages (RELs) have been proposed to describe licenses governing the terms and conditions of content access. In this field XrML and ODRL play a prominent role. Both languages are powerful yet complex. We propose a way of analysing RELs and we apply it to ODRL, XrML and to LicenseScript, a REL we propose. In addition, we test these languages against a number of example scenarios. These examples bring new insights, and shed new light on some of the limits of XrML and ODRL.}}
@inproceedings{Cho03d,
	author = {C. N. Chong and S. Etalle and P. H. Hartel and Y. W. Law},
	title = {Approximating Fair Use in {LicenseScript}},
	booktitle = {6th Int. Conf. of Asian Digital Libraries ({ICADL})},
	volume = {LNCS 2911},
	editor = {M. T. Tengku and H. B. Sembok and H. Zaman},
	publisher = {Springer-Verlag, Berlin},
	address = {Kuala Lumpur, Malaysia},
	month = {Dec},
	year = {2003},
	pages = {432-443},
	url = {http://dx.doi.org/10.1007/b94517},
	annote = {group DIES},
	annote = {isbn 3-540-20608-6},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract Current rights management systems are not able to enforce copyright laws because of both legal and technological reasons. The contract rights granted by a copyright owner typically restrict the users' statutory rights that are endorsed by copyright laws. In particular, Fair Use allows these `unauthorized but not illegal' rights. Two technological reasons why fair use cannot be upheld: (1) the current XML-based rights expression language (REL) cannot capture user's statutory rights; and (2) the underlying architectures cannot support copyright enforcement. This paper focuses on the first problem and introduces a two-pronged approach: (1) rights assertion, to allow a user assert new rights to the license, i.e. freely express her rights under fair use; and (2) audit logging, to record the asserted rights and keep track of the copies rendered and distributed under fair use. We apply this approach in LicenseScript (a logic-based REL) to demonstrate how LicenseScript can approximate fair use easily.}}
@inproceedings{Cor03,
	author = {R. Corin and S. Malladi and J. Alves-Foss and S. Etalle},
	title = {Guess what? Here is a new tool that finds some new guessing attacks (Extended Abstract)},
	booktitle = {{IFIP} {WG} 1.7 and {ACM} {SIGPLAN} Workshop on Issues in the Theory of Security ({WITS})},
	editor = {R. Gorrieri and R. Lucchi},
	publisher = {Dipartamento di Scienze dell'Informazione Universita di Bologna, Italy},
	address = {Warsaw, Poland},
	month = {Apr},
	year = {2003},
	pages = {62-71},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000b2.pdf},
	annote = {group DIES},
	annote = {isbn not assigned},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript}}
@inproceedings{Cor03a,
	author = {R. Corin and A. Durante and S. Etalle and P. H. Hartel},
	title = {{A} Trace Logic for Local Security Properties},
	booktitle = {Int. Workshop on Software Verification and Validation ({SVV})},
	volume = {118},
	publisher = {Electronic Notes in Theoretical Computer Science (ENTCS), 118},
	address = {Mumbai, India},
	month = {Dec},
	year = {2003},
	pages = {129-143},
	url = {http://dx.doi.org/10.1016/j.entcs.2004.12.019},
	annote = {group DIES},
	annote = {issn 1571-0661},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Account},
	annote = {abstract We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specification. Our technique allows a protocol designer to provide a formal specification of the desired security properties, and integrate it naturally into the design process of cryptographic protocols. Furthermore, the logic can be used for formal verification. We illustrate the utility of our technique by exposing new attacks on the well studied TMN protocol.}}
@inproceedings{Eta03a,
	author = {S. Etalle and S. Mukhopadhyay and A. Roychoudhury},
	title = {Preface},
	booktitle = {Int. Workshop on Software Verification and Validation ({SVV})},
	volume = {118},
	publisher = {Electronic Notes in Theoretical Computer Science (ENTCS), 118},
	address = {Mumbai, India},
	month = {Dec},
	year = {2003},
	pages = {1},
	url = {http://dx.doi.org/10.1016/j.entcs.2004.10.004},
	annote = {group DIES},
	annote = {issn 1571-0661},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Account}}
@inproceedings{Law02a,
	author = {Y. W. Law and S. Etalle and P. H. Hartel},
	title = {Assessing {Security-Critical} {Energy-Efficient} Sensor Networks},
	booktitle = {18th {IFIP} {TC11} Int. Conf. on Information Security and Privacy in the Age of Uncertainty ({SEC})},
	editor = {D. Gritzalis and S. De Capitani di Vimercati and P. Samarati and S. K. Katsikas},
	publisher = {Kluwer Academic Publishers, Boston, Massachusetts},
	address = {Athens, Greece},
	month = {May},
	year = {2003},
	pages = {459-463},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/00000087.pdf},
	annote = {group DIES},
	annote = {isbn 1-4020-7449-2},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Eyes},
	annote = {abstract In the EYES project, we are investigating self-organizing, collaborative, energy-efficient sensor networks. This study is devoted to the security aspects of the project. Our contribution is three-fold: firstly, we present a survey, where we discuss the dominant issues of energy-security trade-off in the network protocol and key management design space. From there we set out future research directions for our security framework. Secondly, we propose an assessment framework based on system profile, with which we have managed to carve out manageable design spaces from the seemingly infinite possibilities of ad hoc mobile wireless networks. Finally, we have benchmarked some well-known cryptographic algorithms in search for the best compromise in security and energy-efficiency, on a typical sensor node. Our preliminary investigations also cover an important parameter in the design space: the resource requirements of the symmetric key algorithms RC5 and TEA.}}
@inproceedings{Law03,
	author = {Y. W. Law and R. Corin and S. Etalle and P. H. Hartel},
	title = {{A} Formally Verified Decentralized Key Management Architecture for Wireless Sensor Networks},
	booktitle = {4th {IFIP} {TC6}/{WG6.8} Int. Conf on Personal Wireless Communications ({PWC})},
	volume = {LNCS 2775},
	editor = {M. Conti and S. Giordano and E. Gregori and S. Olariu},
	publisher = {Springer-Verlag, Berlin},
	address = {Venice, Italy},
	month = {Sep},
	year = {2003},
	pages = {27-39},
	url = {http://www.springerlink.com/link.asp?id=tp55mu4ltw9wkvy7},
	annote = {group DIES},
	annote = {isbn 3-540-20123-8},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Eyes},
	annote = {abstract We present a decentralized key management architecture for wireless sensor networks (WSNs), covering the aspects of key deployment, key refreshment and key establishment. Our architecture is based on a clear set of assumptions and guidelines. Key deployment uses minimal key storage while key refreshment is based on the well studied scheme of Abdalla et al. The keying protocols involved uses only symmetric cryptography and have all been verified with our constraint solving-based protocol verification tool CoProVe.}}
@inproceedings{Pie03,
	author = {R. Di Pietro and L. V. Mancini and Y. W. Law and S. Etalle and P. J. M. Havinga},
	title = {{LKHW}: {A} Directed {Diffusion-Based} Secure Multicast Scheme for Wireless Sensor Networks},
	booktitle = {32nd Int. Conf. on Parallel Processing Workshops ({ICPP})},
	editor = {C.-H. Huang and J. Ramanujam},
	publisher = {IEEE Computer Society Press, Los Alamitos, California},
	address = {Kaohsiung, Taiwan},
	month = {Oct},
	year = {2003},
	pages = {397-406},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000cc.pdf},
	annote = {group CADTES},
	annote = {isbn 0-7695-2018-9},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Eyes},
	annote = {abstract We present a mechanism for securing group communications in Wireless Sensor Networks (WSN). First, we derive an extension of Logical Key Hierarchy (LKH). Then we merge the extension with Directed Diffusion (DD). The resulting protocol, LKHW, combines the advantages of both LKH and DD. In particular, LKHW enforces both backward and forward secrecy, while incurring only limited overhead in terms of the number of messages required. This is the first security protocol that leverages DD, and it shows that such a paradigm is also viable for other applications than routing. Finally, a few new research directions that originate from this paper are discussed.}}
@misc{Cho03b,
	author = {C. N. Chong and R. Corin and Y. W. Law and S. Etalle},
	title = {License Interpreter, Manager and Interface for {LicenseScript}},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	month = {Jul},
	year = {2003},
	url = {http://wwwes.cs.utwente.nl/licensescript/tools/},
	annote = {group DIES},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript}}
@techreport{Bri03,
	author = {R. Brinkman and L. Feng and S. Etalle and P. H. Hartel and W. Jonker},
	title = {Experimenting with linear search in encrypted data},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {TR-CTIT-03-43},
	month = {Sep},
	year = {2003},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000d9.pdf},
	annote = {group DB},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project SecureMetaData},
	annote = {abstract Song, Wagner and Perrig have published a theoretical paper about keyword search on encrypted textual data. We describe a prototype implementing their theory. Tests are carried out with this prototype to analyse efficiency and timing aspects. As expected encryption and search times are linear in the size of the database. More interestingly they also depend on the parameters used in the protocol.}}
@techreport{Cor03b,
	author = {R. Corin and C. N. Chong and S. Etalle and P. H. Hartel},
	title = {How to pay in {LicenseScript}},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {TR-CTIT-03-31},
	month = {Aug},
	year = {2003},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000ce.pdf},
	annote = {group DIES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project LicenseScript},
	annote = {abstract Current DRM systems do not provide flexible payment methods, requiring the user to handle the payment by hand. For instance, when the user needs to pay for watching a movie, she needs to decide which available payment method is the most optimal and suitable. This is a rather cumbersome process for the user that can be avoided by the specification of payment policies. A payment policy automates the payment process of each content usage, choosing the best alternative among the possible payment methods. We show how LicenseScript is able to model payment policies, allowing the user to precisely specify how a payment of content usage should be performed.}}
@inproceedings{Cor02,
	author = {R. Corin and S. Etalle},
	title = {An Improved Constraint-based system for the verification of security protocols},
	booktitle = {9th Int. Static Analysis Symp. ({SAS})},
	volume = {LNCS 2477},
	editor = {M. V. Hermenegildo and G. Puebla},
	publisher = {Springer-Verlag, Berlin},
	address = {Madrid, Spain},
	month = {Sep},
	year = {2002},
	pages = {326-341},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/00000096.pdf},
	annote = {group DIES},
	annote = {isbn 3-540-44235-9},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Account},
	annote = {abstract We propose a constraint-based system for the verification of security protocols that improves upon the one developed by Millen and Shmatikov. Our system features (1) a significantly more efficient implementation, (2) a monotonic behavior, which also allows to detect aws associated to partial runs and (3) a more expressive syntax, in which a principal may also perform explicit checks. We also show why these improvements yield a more effective and practical system.}}
@misc{Cor02b,
	author = {R. Corin and S. Etalle},
	title = {{CoProVe} -- {A} {Constraint-Based} System for the Verification of Security Protocols},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	month = {Sep},
	year = {2002},
	url = {http://wwwes.cs.utwente.nl/24cqet/coprove.html},
	annote = {group DIES},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Account}}
@techreport{Law02b,
	author = {Y. W. Law and S. Etalle and P. H. Hartel},
	title = {Key Management with {Group-Wise} {Pre-Deployed} Keying and Secret Sharing {Pre-Deployed} Keying},
	institution = {Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands},
	type = {Technical report},
	number = {TR-CTIT-02-25},
	month = {Jul},
	year = {2002},
	url = {http://www.ub.utwente.nl/webdocs/ctit/1/00000094.pdf},
	annote = {group DIES},
	annote = {issn 1381-3625},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Eyes},
	annote = {abstract In wireless sensor networks, the key deployment problem has received little attention, whereas it is in fact fundamental, heavily involving crucial (scarce) resources of ad-hoc networks, such as memory and energy availability. We first briefly survey the state-of-the art of key deployment strategies that are amenable to ad-hoc network. Then we proposed two possible methods and we shortly investigate their space and computational complexity.}}
@inproceedings{DE02,
	author = {G. Delzanno and S. Etalle},
	title = {Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols},
	booktitle = {11th Int. Logic Based Program Synthesis and Transformation ({LOPSTR})},
	volume = {LNCS 2372},
	editor = {A. Pettorossi},
	publisher = {Springer-Verlag, Berlin},
	address = {Paphos, Greece},
	month = {Nov},
	year = {2001},
	pages = {76-90},
	url = {http://www.cs.utwente.nl/~etalle/papers/de02lopstr.pdf},
	annote = {group DIES},
	annote = {isbn 3-540-43915-3},
	annote = {issn 0302-9743},
	annote = {topic Security},
	annote = {program ISTRICE},
	annote = {project Account},
	annote = {abstract We define a sequent calculus to formally specify, simulate, debug and verify security protocols. In our sequents we distinguish between the current knowledge of principals and the current global state of the session. Hereby, we can describe the operational semantics of principals and of an intruder in a simple and modular way. Furthermore, using proof theoretic tools like the analysis of permutability of rules, we are able to find efficient proof strategies that we prove complete for special classes of security protocols including Needham-Schroeder. Based on the results of this preliminary analysis, we have implemented a Prolog meta-interpreter which allows for rapid prototyping and for checking safety properties of security protocols, and we have applied it for finding error traces and proving correctness of practical examples.}}