NDLI: Strand spaces with choice via a process algebra semantics

Please wait, while we are loading the content...

Testing of concurrent and imperative software using CLP

Challenges in compiling Coq

Description and evaluation of a generic design to integrate CLP and tabled execution

Higher-order logic programming: an expressive language for representing qualitative preferences

A framework for easing the development of applications embedding answer set programming

Proving inductive validity of constrained inequalities

Analysis of access control policy updates through narrowing

Strand spaces with choice via a process algebra semantics

Reducing the overhead of assertion run-time checks via static analysis

Exploration of language specifications by compilation to first-order logic

Actors may synchronize, safely!

Iterated process analysis over lattice-valued regular expressions

Typechecking protocols with Mungo and StMungo

Unification of program expressions with recursive bindings

The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value

Effect-dependent transformations for concurrent programs

Towards a framework for algorithm recognition in binary code

Language-integrated provenance

Demand-driven incremental object queries

Strand spaces with choice via a process algebra semantics

Content Provider	ACM Digital Library
Author	Meadows, Catherine Escobar, Santiago Santiago, Sonia Meseguer, José Yang, Fan
Abstract	Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool. To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e. the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an (explicit) if-then-else choice, i.e. one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e. execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper. Our main theoretical results are two bisimulation results: one proving that the formal semantics of our process algebra is bisimilar to the forwards execution semantics of its associated strands, and another showing that it is also bisimilar with respect to the symbolic backwards semantics of the strands such as that supported by Maude-NPA. At the practical level, we present a prototype implementation of our process algebra in Maude-NPA, illustrate its expressive power and naturalness with various examples, and show how it can be effectively used in formal analysis.
Starting Page	76
Ending Page	89
Page Count	14
File Format	PDF
ISBN	9781450341486
DOI	10.1145/2967973.2968609
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-09-05
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Process algebra Cryptographic protocol analysis Narrowing-based reachability analysis Rewriting-based model checking
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in