Cyber Protocols in the Physical Environment
Abstract
The work included participation in the Kerberos Working Group of The Internet Engineering Task Force (IETF), where our work contributed to the wording of the Kerberos IETF specification. Security protocol analysis literature considers the so-called Dolev–Yao adversary, a powerful adversary which can act as the network, intercept, decompose, compose, and send messages, and can remember as much information as it needs. That is, its memory is unbounded. Scedrov and collaborators proposed a weaker Dolev–Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev–Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where although the total number of sessions is unbounded, there are only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts or an unbounded number of nonces at a time. This led us to the question of whether it is possible to compute an upper-bound on the memory required by the Dolev–Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. Our recent work answers this question negatively. An interesting class of protocols that is receiving attention recently are the so-called cyberphysical protocols. These protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance-Bounding protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. Other examples include Secure Neighbor Discovery, Secure Localization Protocols, Secure Time Synchronization Protocols, and others. Time plays a key role in the design and verification of many of these protocols. In addition, the message transmission medium is not necessarily only the internet but could also be radio wave or ultrasound. A further interesting challenge is whether the protocol participants and the adversary are static or whether they may be moving. Scedrov and collaborators have started investigating the foundational differences from the traditional Dolev-Yao adversary model and their significance for protocol verification in this interesting research area. Scedrov and collaborators have also introduced a multiset rewriting based formal framework for strategic planning. The collaborating organizations or individuals share some information in order to achieve a desired common goal, but they each also need to guard their sensitive information. The decision which pieces of information to share and which pieces to protect is usually based on a number of factors depending on the nature and the context of the collaboration. Different participants can be trusted with different information in different contexts. We have developed decision algorithms for policy compliance checking as well as an initial implementation in the computational tool Maude both of the original collaborative planning framework as well as its timed extension. Scedrov and collaborators are pursuing an application of a timed extension of this framework which arises in pharmacological research, clinical trials of proposed medications on human subjects. A prospective transition being developed would involve a CTA, clinical trials assistant, an automated tool which would use the formal framework discussed in, implemented in Maude, to model clinical trial protocols, as the basis for planning and compliance checking. The proposed research will emphasize: 1) the investigation of threat models appropriate for cyber protocols in the physical environment and 2) continuation, refinement, and extensions of the theoretical investigation of the multiset rewriting based formal framework for strategic planning.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 12, 2016
- Source ID
- N000141512047
Entities
People
- Andre Scedrov
Organizations
- Office of Naval Research
- United States Navy
- University of Pennsylvania