اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدEpistemic Temporal Logic for Information Flow Security
161
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.
قيم البحث
اقرأ أيضاً
Logics for social networks have been studied in recent literature. This paper presents a framework based on *dynamic term-modal logic* (DTML), a quantified variant of dynamic epistemic logic (DEL). In contrast with DEL where it is commonly known to w
hom agent names refer, DTML can represent dynamics with uncertainty about agent identity. We exemplify dynamics where such uncertainty and de re/de dicto distinctions are key to social network epistemics. Technically, we show that DTML semantics can represent a popular class of hybrid logic epistemic social network models. We also show that DTML can encode previously discussed dynamics for which finding a complete logic was left open. As complete reduction axioms systems exist for DTML, this yields a complete system for the dynamics in question.
The ISO 21434 is a new standard that has been proposed to address the future challenges of automotive cybersecurity. This white paper takes a closer look at the ISO 21434 helping engineers to understand the ISO 21434 parts, the key activities to be c
arried out and the main artefacts that shall be produced. As any certification, obtaining the ISO 21434 certification can be daunting at first sight. Engineers have to deploy processes that include several security risk assessment methods to produce security arguments and evidence supporting item security claims. In this white paper, we propose a security engineering approach that can ease this process by relying on Rigorous Security Assessments and Incremental Assessment Maintenance methods supported by automation. We demonstrate by example that the proposed approach can greatly increase the quality of the produced artefacts, the efficiency to produce them, as well as enable continuous security assessment. Finally, we point out some key research directions that we are investigating to fully realize the proposed approach.
We describe and implement a policy language. In our system, agents can distribute data along with usage policies in a decentralized architecture. Our language supports the specification of conditions and obligations, and also the possibility to refin
e policies. In our framework, the compliance with usage policies is not actively enforced. However, agents are accountable for their actions, and may be audited by an authority requiring justifications.
We propose a new simple emph{trace} logic that can be used to specify emph{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 fo
rmal 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 protocol TMN.
Where information grows abundant, attention becomes a scarce resource. As a result, agents must plan wisely how to allocate their attention in order to achieve epistemic efficiency. Here, we present a framework for multi-agent epistemic planning with
attention, based on Dynamic Epistemic Logic (DEL, a powerful formalism for epistemic planning). We identify the framework as a fragment of standard DEL, and consider its plan existence problem. While in the general case undecidable, we show that when attention is required for learning, all instances of the problem are decidable.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
